adjust test

src/Init/Data/Int/DivMod/Bootstrap.lean

@@ -23,11 +23,11 @@ namespace Int
 
 protected theorem dvd_def (a b : Int) : (a ∣ b) = Exists (fun c => b = a * c) := rfl
 
-@[simp] protected theorem dvd_zero (n : Int) : n ∣ 0 := ⟨0, (Int.mul_zero _).symm⟩
+@[simp, grind] protected theorem dvd_zero (n : Int) : n ∣ 0 := ⟨0, (Int.mul_zero _).symm⟩
 
-@[simp] protected theorem dvd_refl (n : Int) : n ∣ n := ⟨1, (Int.mul_one _).symm⟩
+@[simp, grind] protected theorem dvd_refl (n : Int) : n ∣ n := ⟨1, (Int.mul_one _).symm⟩
 
-@[simp] protected theorem one_dvd (n : Int) : 1 ∣ n := ⟨n, (Int.one_mul n).symm⟩
+@[simp, grind] protected theorem one_dvd (n : Int) : 1 ∣ n := ⟨n, (Int.one_mul n).symm⟩
 
 protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
   | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => Exists.intro (d * e) (by rw [Int.mul_assoc])
@@ -42,23 +42,27 @@ protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
   | .inr h => match a, eq_ofNat_of_zero_le h with
     | _, ⟨k, rfl⟩ => exact ⟨k, Int.ofNat.inj ae⟩
 
-@[simp] protected theorem zero_dvd {n : Int} : 0 ∣ n ↔ n = 0 :=
+@[simp, grind =] protected theorem zero_dvd {n : Int} : 0 ∣ n ↔ n = 0 :=
   Iff.intro (fun ⟨k, e⟩ => by rw [e, Int.zero_mul])
             (fun h => h.symm ▸ Int.dvd_refl _)
 
 @[simp] protected theorem dvd_mul_right (a b : Int) : a ∣ a * b := ⟨_, rfl⟩
 
+grind_pattern Int.dvd_mul_right => b ∣ a * b
+
 @[simp] protected theorem dvd_mul_left (a b : Int) : b ∣ a * b := ⟨_, Int.mul_comm ..⟩
 
-@[simp] protected theorem neg_dvd {a b : Int} : -a ∣ b ↔ a ∣ b := by
+grind_pattern Int.dvd_mul_left => a ∣ a * b
+
+@[simp, grind =] protected theorem neg_dvd {a b : Int} : -a ∣ b ↔ a ∣ b := by
   constructor <;> exact fun ⟨k, e⟩ =>
     ⟨-k, by simp [e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
 
-@[simp] protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
+@[simp, grind =] protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
   constructor <;> exact fun ⟨k, e⟩ =>
     ⟨-k, by simp [← e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
 
-@[simp] theorem natAbs_dvd_natAbs {a b : Int} : natAbs a ∣ natAbs b ↔ a ∣ b := by
+@[simp, grind =] theorem natAbs_dvd_natAbs {a b : Int} : natAbs a ∣ natAbs b ↔ a ∣ b := by
   refine ⟨fun ⟨k, hk⟩ => ?_, fun ⟨k, hk⟩ => ⟨natAbs k, hk.symm ▸ natAbs_mul a k⟩⟩
   rw [← natAbs_natCast k, ← natAbs_mul, natAbs_eq_natAbs_iff] at hk
   cases hk <;> subst b
@@ -70,19 +74,19 @@ theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natA
 
 /-! ### ediv zero  -/
 
-@[simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
+@[simp, grind =] theorem zero_ediv : ∀ b : Int, 0 / b = 0
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => show -ofNat _ = _ by simp
 
-@[simp] protected theorem ediv_zero : ∀ a : Int, a / 0 = 0
+@[simp, grind =] protected theorem ediv_zero : ∀ a : Int, a / 0 = 0
   | ofNat _ => show ofNat _ = _ by simp
   | -[_+1] => rfl
 
 /-! ### emod zero -/
 
-@[simp] theorem zero_emod (b : Int) : 0 % b = 0 := rfl
+@[simp, grind =] theorem zero_emod (b : Int) : 0 % b = 0 := rfl
 
-@[simp] theorem emod_zero : ∀ a : Int, a % 0 = a
+@[simp, grind =] theorem emod_zero : ∀ a : Int, a % 0 = a
   | ofNat _ => congrArg ofNat <| Nat.mod_zero _
   | -[_+1]  => congrArg negSucc <| Nat.mod_zero _
 
@@ -125,7 +129,7 @@ theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
 
 /-! ### `/` ediv -/
 
-@[simp] theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
+@[simp, grind =] theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
   | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
   | ofNat _, -[_+1] => (Int.neg_neg _).symm
   | ofNat _, succ _ | -[_+1], 0 | -[_+1], succ _ | -[_+1], -[_+1] => rfl
@@ -162,6 +166,7 @@ theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c
       apply congrArg negSucc
       rw [Nat.mul_comm, Nat.sub_mul_div_of_le]; rwa [Nat.mul_comm]
 
+@[grind =]
 theorem add_mul_ediv_left (a : Int) {b : Int}
     (c : Int) (H : b ≠ 0) : (a + b * c) / b = a / b + c :=
   Int.mul_comm .. ▸ Int.add_mul_ediv_right _ _ H
@@ -175,13 +180,14 @@ theorem add_ediv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b) / c = a / c
 theorem add_ediv_of_dvd_left {a b c : Int} (H : c ∣ a) : (a + b) / c = a / c + b / c := by
   rw [Int.add_comm, Int.add_ediv_of_dvd_right H, Int.add_comm]
 
-@[simp] theorem mul_ediv_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b) / b = a := by
+@[simp, grind =] theorem mul_ediv_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b) / b = a := by
   have := Int.add_mul_ediv_right 0 a H
   rwa [Int.zero_add, Int.zero_ediv, Int.zero_add] at this
 
-@[simp] theorem mul_ediv_cancel_left (b : Int) (H : a ≠ 0) : (a * b) / a = b :=
+@[simp, grind =] theorem mul_ediv_cancel_left (b : Int) (H : a ≠ 0) : (a * b) / a = b :=
   Int.mul_comm .. ▸ Int.mul_ediv_cancel _ H
 
+@[grind =]
 theorem ediv_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : 0 ≤ a / b ↔ 0 ≤ a := by
   rw [Int.div_def]
   match b, h with
@@ -202,31 +208,31 @@ theorem emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b :=
   | ofNat _, _, ⟨_, rfl⟩ => ofNat_lt.2 (Nat.mod_lt _ (Nat.succ_pos _))
   | -[_+1], _, ⟨_, rfl⟩ => Int.sub_lt_self _ (ofNat_lt.2 <| Nat.succ_pos _)
 
-@[simp] theorem add_mul_emod_self_right (a b c : Int) : (a + b * c) % c = a % c :=
+@[simp, grind =] theorem add_mul_emod_self_right (a b c : Int) : (a + b * c) % c = a % c :=
   if cz : c = 0 then by
     rw [cz, Int.mul_zero, Int.add_zero]
   else by
     rw [Int.emod_def, Int.emod_def, Int.add_mul_ediv_right _ _ cz, Int.add_comm _ b,
       Int.mul_add, Int.mul_comm, ← Int.sub_sub, Int.add_sub_cancel]
 
-@[simp] theorem add_mul_emod_self_left (a b c : Int) : (a + b * c) % b = a % b := by
+@[simp, grind =] theorem add_mul_emod_self_left (a b c : Int) : (a + b * c) % b = a % b := by
   rw [Int.mul_comm, add_mul_emod_self_right]
 
-@[simp] theorem mul_add_emod_self_right (a b c : Int) : (a * b + c) % b = c % b := by
+@[simp, grind =] theorem mul_add_emod_self_right (a b c : Int) : (a * b + c) % b = c % b := by
   rw [Int.add_comm, add_mul_emod_self_right]
 
-@[simp] theorem mul_add_emod_self_left (a b c : Int) : (a * b + c) % a = c % a := by
+@[simp, grind =] theorem mul_add_emod_self_left (a b c : Int) : (a * b + c) % a = c % a := by
   rw [Int.add_comm, add_mul_emod_self_left]
 
 @[deprecated add_mul_emod_self_right (since := "2025-04-11")]
 theorem add_mul_emod_self {a b c : Int} : (a + b * c) % c = a % c :=
   add_mul_emod_self_right ..
 
-@[simp] theorem emod_add_emod (m n k : Int) : (m % n + k) % n = (m + k) % n := by
+@[simp, grind =] theorem emod_add_emod (m n k : Int) : (m % n + k) % n = (m + k) % n := by
   have := (add_mul_emod_self_left (m % n + k) n (m / n)).symm
   rwa [Int.add_right_comm, emod_add_ediv] at this
 
-@[simp] theorem add_emod_emod (m n k : Int) : (m + n % k) % k = (m + n) % k := by
+@[simp, grind =] theorem add_emod_emod (m n k : Int) : (m + n % k) % k = (m + n) % k := by
   rw [Int.add_comm, emod_add_emod, Int.add_comm]
 
 theorem add_emod (a b n : Int) : (a + b) % n = (a % n + b % n) % n := by
@@ -242,22 +248,22 @@ theorem emod_add_cancel_right {m n k : Int} (i) : (m + i) % n = (k + i) % n ↔
     rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this,
   add_emod_eq_add_emod_right _⟩
 
-@[simp] theorem mul_emod_left (a b : Int) : (a * b) % b = 0 := by
+@[simp, grind =] theorem mul_emod_left (a b : Int) : (a * b) % b = 0 := by
   rw [← Int.zero_add (a * b), add_mul_emod_self_right, Int.zero_emod]
 
-@[simp] theorem mul_emod_right (a b : Int) : (a * b) % a = 0 := by
+@[simp, grind =] theorem mul_emod_right (a b : Int) : (a * b) % a = 0 := by
   rw [Int.mul_comm, mul_emod_left]
 
-theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
+theorem mul_emod (a b n : Int) : (a * b) % n = ((a % n) * (b % n)) % n := by
   conv => lhs; rw [
     ← emod_add_ediv a n, ← emod_add_ediv' b n, Int.add_mul, Int.mul_add, Int.mul_add,
     Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_emod_self_left,
     ← Int.mul_assoc, add_mul_emod_self_right]
 
-@[simp] theorem emod_self {a : Int} : a % a = 0 := by
+@[simp, grind =] theorem emod_self {a : Int} : a % a = 0 := by
   have := mul_emod_left 1 a; rwa [Int.one_mul] at this
 
-@[simp] theorem emod_emod_of_dvd (n : Int) {m k : Int}
+@[simp, grind =] theorem emod_emod_of_dvd (n : Int) {m k : Int}
     (h : m ∣ k) : (n % k) % m = n % m := by
   conv => rhs; rw [← emod_add_ediv n k]
   match k, h with
@@ -310,9 +316,15 @@ theorem sub_ediv_of_dvd (a : Int) {b c : Int}
 protected theorem ediv_mul_cancel {a b : Int} (H : b ∣ a) : a / b * b = a :=
   ediv_mul_cancel_of_emod_eq_zero (emod_eq_zero_of_dvd H)
 
+-- We only trigger this lemma if we've already seen `b | a`.
+grind_pattern Int.ediv_mul_cancel => a / b * b, b ∣ a
+
 protected theorem mul_ediv_cancel' {a b : Int} (H : a ∣ b) : a * (b / a) = b := by
   rw [Int.mul_comm, Int.ediv_mul_cancel H]
 
+-- We only trigger this lemma if we've already seen `a | b`.
+grind_pattern Int.mul_ediv_cancel' => a * (b / a), a ∣ b
+
 theorem emod_pos_of_not_dvd {a b : Int} (h : ¬ a ∣ b) : a = 0 ∨ 0 < b % a := by
   rw [dvd_iff_emod_eq_zero] at h
   by_cases w : a = 0
@@ -333,7 +345,7 @@ theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
 
 /-! ### bmod -/
 
-@[simp] theorem bmod_emod : bmod x m % m = x % m := by
+@[simp, grind =] theorem bmod_emod : bmod x m % m = x % m := by
   dsimp [bmod]
   split <;> simp [Int.sub_emod]
 

src/Init/Data/Nat/Dvd.lean

@@ -11,13 +11,18 @@ import Init.Meta
 
 namespace Nat
 
-@[simp] protected theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩
+@[simp, grind] protected theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩
 
-@[simp] protected theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩
+@[simp, grind] protected theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩
 
 protected theorem dvd_mul_left (a b : Nat) : a ∣ b * a := ⟨b, Nat.mul_comm b a⟩
+
+grind_pattern Nat.dvd_mul_left => a ∣ b * a
+
 protected theorem dvd_mul_right (a b : Nat) : a ∣ a * b := ⟨b, rfl⟩
 
+grind_pattern Nat.dvd_mul_right => a ∣ a * b
+
 protected theorem dvd_trans {a b c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
   match h₁, h₂ with
   | ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ =>
@@ -32,7 +37,7 @@ protected theorem dvd_mul_right_of_dvd {a b : Nat} (h : a ∣ b) (c : Nat) : a
 protected theorem eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) : a = 0 :=
   let ⟨c, H'⟩ := h; H'.trans c.zero_mul
 
-@[simp] protected theorem zero_dvd {n : Nat} : 0 ∣ n ↔ n = 0 :=
+@[simp, grind =] protected theorem zero_dvd {n : Nat} : 0 ∣ n ↔ n = 0 :=
   ⟨Nat.eq_zero_of_zero_dvd, fun h => h.symm ▸ Nat.dvd_zero 0⟩
 
 protected theorem dvd_add {a b c : Nat} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
@@ -47,6 +52,7 @@ protected theorem dvd_add_iff_right {k m n : Nat} (h : k ∣ m) : k ∣ n ↔ k
 protected theorem dvd_add_iff_left {k m n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n := by
   rw [Nat.add_comm]; exact Nat.dvd_add_iff_right h
 
+@[grind =]
 theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m := by
   have := Nat.dvd_add_iff_left (m := m % n) <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n)
   rwa [mod_add_div] at this
@@ -70,7 +76,7 @@ protected theorem dvd_antisymm : ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
 theorem pos_of_dvd_of_pos {m n : Nat} (H1 : m ∣ n) (H2 : 0 < n) : 0 < m :=
   Nat.pos_of_ne_zero fun m0 => Nat.ne_of_gt H2 <| Nat.eq_zero_of_zero_dvd (m0 ▸ H1)
 
-@[simp] protected theorem one_dvd (n : Nat) : 1 ∣ n := ⟨n, n.one_mul.symm⟩
+@[simp, grind] protected theorem one_dvd (n : Nat) : 1 ∣ n := ⟨n, n.one_mul.symm⟩
 
 theorem eq_one_of_dvd_one {n : Nat} (H : n ∣ 1) : n = 1 := Nat.dvd_antisymm H n.one_dvd
 
@@ -96,10 +102,16 @@ protected theorem mul_div_cancel' {n m : Nat} (H : n ∣ m) : n * (m / n) = m :=
   have := mod_add_div m n
   rwa [mod_eq_zero_of_dvd H, Nat.zero_add] at this
 
+-- We only trigger this lemma if we've already seen `n | m`.
+grind_pattern Nat.mul_div_cancel' => n * (m / n), n ∣ m
+
 protected theorem div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m := by
   rw [Nat.mul_comm, Nat.mul_div_cancel' H]
 
-@[simp] theorem mod_mod_of_dvd (a : Nat) (h : c ∣ b) : a % b % c = a % c := by
+-- We only trigger this lemma if we've already seen `n | m`.
+grind_pattern Nat.div_mul_cancel => m / n * n, n ∣ m
+
+@[simp, grind =] theorem mod_mod_of_dvd (a : Nat) (h : c ∣ b) : a % b % c = a % c := by
   rw (occs := [2]) [← mod_add_div a b]
   have ⟨x, h⟩ := h
   subst h
@@ -145,7 +157,7 @@ protected theorem mul_dvd_mul_left (a : Nat) (h : b ∣ c) : a * b ∣ a * c :=
 protected theorem mul_dvd_mul_right (h: a ∣ b) (c : Nat) : a * c ∣ b * c :=
   Nat.mul_dvd_mul h (Nat.dvd_refl c)
 
-@[simp] theorem dvd_one {n : Nat} : n ∣ 1 ↔ n = 1 :=
+@[simp, grind =] theorem dvd_one {n : Nat} : n ∣ 1 ↔ n = 1 :=
   ⟨eq_one_of_dvd_one, fun h => h.symm ▸ Nat.dvd_refl _⟩
 
 protected theorem mul_div_assoc (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k) := by

src/Init/Data/Nat/Gcd.lean

@@ -36,7 +36,7 @@ def gcd (m n : @& Nat) : Nat :=
   termination_by m
   decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
 
-@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y := by
+@[simp, grind =] theorem gcd_zero_left (y : Nat) : gcd 0 y = y := by
   rw [gcd]; rfl
 
 theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := by
@@ -48,11 +48,11 @@ theorem gcd_add_one (x y : Nat) : gcd (x + 1) y = gcd (y % (x + 1)) (x + 1) := b
 theorem gcd_def (x y : Nat) : gcd x y = if x = 0 then y else gcd (y % x) x := by
   cases x <;> simp [Nat.gcd_add_one]
 
-@[simp] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by
+@[simp, grind =] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by
   rw [gcd_succ, mod_one]
   rfl
 
-@[simp] theorem gcd_zero_right (n : Nat) : gcd n 0 = n := by
+@[simp, grind =] theorem gcd_zero_right (n : Nat) : gcd n 0 = n := by
   cases n with
   | zero => simp [gcd_succ]
   | succ n =>
@@ -63,7 +63,7 @@ instance : Std.LawfulIdentity gcd 0 where
   left_id := gcd_zero_left
   right_id := gcd_zero_right
 
-@[simp] theorem gcd_self (n : Nat) : gcd n n = n := by
+@[simp, grind =] theorem gcd_self (n : Nat) : gcd n n = n := by
   cases n <;> simp [gcd_succ]
 instance : Std.IdempotentOp gcd := ⟨gcd_self⟩
 
@@ -87,8 +87,12 @@ theorem gcd_dvd (m n : Nat) : (gcd m n ∣ m) ∧ (gcd m n ∣ n) := by
 
 theorem gcd_dvd_left (m n : Nat) : gcd m n ∣ m := (gcd_dvd m n).left
 
+grind_pattern gcd_dvd_left => gcd m n
+
 theorem gcd_dvd_right (m n : Nat) : gcd m n ∣ n := (gcd_dvd m n).right
 
+grind_pattern gcd_dvd_right => gcd m n
+
 theorem gcd_le_left (n) (h : 0 < m) : gcd m n ≤ m := le_of_dvd h <| gcd_dvd_left m n
 
 theorem gcd_le_right (m) (h : 0 < n) : gcd m n ≤ n := le_of_dvd h <| gcd_dvd_right m n
@@ -98,10 +102,12 @@ theorem dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n := by
   | H0 n => rw [gcd_zero_left]; exact kn
   | H1 n m _ IH => rw [gcd_rec]; exact IH ((dvd_mod_iff km).2 kn) km
 
+@[grind =]
 theorem dvd_gcd_iff : k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n :=
   ⟨fun h => let ⟨h₁, h₂⟩ := gcd_dvd m n; ⟨Nat.dvd_trans h h₁, Nat.dvd_trans h h₂⟩,
    fun ⟨h₁, h₂⟩ => dvd_gcd h₁ h₂⟩
 
+@[grind =]
 theorem gcd_comm (m n : Nat) : gcd m n = gcd n m :=
   Nat.dvd_antisymm
     (dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n))
@@ -115,6 +121,7 @@ theorem gcd_eq_left_iff_dvd : gcd m n = m ↔ m ∣ n :=
 theorem gcd_eq_right_iff_dvd : gcd n m = m ↔ m ∣ n := by
   rw [gcd_comm]; exact gcd_eq_left_iff_dvd
 
+@[grind _=_]
 theorem gcd_assoc (m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k) :=
   Nat.dvd_antisymm
     (dvd_gcd
@@ -127,13 +134,15 @@ theorem gcd_assoc (m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k) :=
       (Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
 instance : Std.Associative gcd := ⟨gcd_assoc⟩
 
-@[simp] theorem gcd_one_right (n : Nat) : gcd n 1 = 1 := (gcd_comm n 1).trans (gcd_one_left n)
+@[simp, grind =] theorem gcd_one_right (n : Nat) : gcd n 1 = 1 := (gcd_comm n 1).trans (gcd_one_left n)
 
+@[grind =]
 theorem gcd_mul_left (m n k : Nat) : gcd (m * n) (m * k) = m * gcd n k := by
   induction n, k using gcd.induction with
   | H0 k => simp
   | H1 n k _ IH => rwa [← mul_mod_mul_left, ← gcd_rec, ← gcd_rec] at IH
 
+@[grind =]
 theorem gcd_mul_right (m n k : Nat) : gcd (m * n) (k * n) = gcd m k * n := by
   rw [Nat.mul_comm m n, Nat.mul_comm k n, Nat.mul_comm (gcd m k) n, gcd_mul_left]
 
@@ -162,6 +171,7 @@ theorem gcd_ne_zero_left : m ≠ 0 → gcd m n ≠ 0 := mt eq_zero_of_gcd_eq_zer
 
 theorem gcd_ne_zero_right : n ≠ 0 → gcd m n ≠ 0 := mt eq_zero_of_gcd_eq_zero_right
 
+@[grind =]
 theorem gcd_div {m n k : Nat} (H1 : k ∣ m) (H2 : k ∣ n) :
     gcd (m / k) (n / k) = gcd m n / k :=
   match eq_zero_or_pos k with
@@ -171,12 +181,15 @@ theorem gcd_div {m n k : Nat} (H1 : k ∣ m) (H2 : k ∣ n) :
     rw [Nat.div_mul_cancel (dvd_gcd H1 H2), ← gcd_mul_right,
         Nat.div_mul_cancel H1, Nat.div_mul_cancel H2]
 
+@[grind]
 theorem gcd_dvd_gcd_of_dvd_left {m k : Nat} (n : Nat) (H : m ∣ k) : gcd m n ∣ gcd k n :=
   dvd_gcd (Nat.dvd_trans (gcd_dvd_left m n) H) (gcd_dvd_right m n)
 
+@[grind]
 theorem gcd_dvd_gcd_of_dvd_right {m k : Nat} (n : Nat) (H : m ∣ k) : gcd n m ∣ gcd n k :=
   dvd_gcd (gcd_dvd_left n m) (Nat.dvd_trans (gcd_dvd_right n m) H)
 
+@[grind]
 theorem gcd_dvd_gcd_mul_left_left (m n k : Nat) : gcd m n ∣ gcd (k * m) n :=
   gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_left _ _)
 
@@ -184,6 +197,7 @@ theorem gcd_dvd_gcd_mul_left_left (m n k : Nat) : gcd m n ∣ gcd (k * m) n :=
 theorem gcd_dvd_gcd_mul_left (m n k : Nat) : gcd m n ∣ gcd (k * m) n :=
   gcd_dvd_gcd_mul_left_left m n k
 
+@[grind]
 theorem gcd_dvd_gcd_mul_right_left (m n k : Nat) : gcd m n ∣ gcd (m * k) n :=
   gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_right _ _)
 
@@ -191,9 +205,11 @@ theorem gcd_dvd_gcd_mul_right_left (m n k : Nat) : gcd m n ∣ gcd (m * k) n :=
 theorem gcd_dvd_gcd_mul_right (m n k : Nat) : gcd m n ∣ gcd (m * k) n :=
   gcd_dvd_gcd_mul_right_left m n k
 
+@[grind]
 theorem gcd_dvd_gcd_mul_left_right (m n k : Nat) : gcd m n ∣ gcd m (k * n) :=
   gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_left _ _)
 
+@[grind]
 theorem gcd_dvd_gcd_mul_right_right (m n k : Nat) : gcd m n ∣ gcd m (n * k) :=
   gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_right _ _)
 
@@ -213,68 +229,68 @@ theorem gcd_right_eq_iff {m n n' : Nat} : gcd m n = gcd m n' ↔ ∀ k, k ∣ m
 theorem gcd_left_eq_iff {m m' n : Nat} : gcd m n = gcd m' n ↔ ∀ k, k ∣ n → (k ∣ m ↔ k ∣ m') := by
   rw [gcd_comm m n, gcd_comm m' n, gcd_right_eq_iff]
 
-@[simp] theorem gcd_mul_left_left (m n : Nat) : gcd (m * n) n = n :=
+@[simp, grind =] theorem gcd_mul_left_left (m n : Nat) : gcd (m * n) n = n :=
   Nat.dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (Nat.dvd_mul_left _ _) (Nat.dvd_refl _))
 
-@[simp] theorem gcd_mul_left_right (m n : Nat) : gcd n (m * n) = n := by
+@[simp, grind =] theorem gcd_mul_left_right (m n : Nat) : gcd n (m * n) = n := by
   rw [gcd_comm, gcd_mul_left_left]
 
-@[simp] theorem gcd_mul_right_left (m n : Nat) : gcd (n * m) n = n := by
+@[simp, grind =] theorem gcd_mul_right_left (m n : Nat) : gcd (n * m) n = n := by
   rw [Nat.mul_comm, gcd_mul_left_left]
 
-@[simp] theorem gcd_mul_right_right (m n : Nat) : gcd n (n * m) = n := by
+@[simp, grind =] theorem gcd_mul_right_right (m n : Nat) : gcd n (n * m) = n := by
   rw [gcd_comm, gcd_mul_right_left]
 
-@[simp] theorem gcd_gcd_self_right_left (m n : Nat) : gcd m (gcd m n) = gcd m n :=
+@[simp, grind =] theorem gcd_gcd_self_right_left (m n : Nat) : gcd m (gcd m n) = gcd m n :=
   Nat.dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (gcd_dvd_left _ _) (Nat.dvd_refl _))
 
-@[simp] theorem gcd_gcd_self_right_right (m n : Nat) : gcd m (gcd n m) = gcd n m := by
+@[simp, grind =] theorem gcd_gcd_self_right_right (m n : Nat) : gcd m (gcd n m) = gcd n m := by
   rw [gcd_comm n m, gcd_gcd_self_right_left]
 
-@[simp] theorem gcd_gcd_self_left_right (m n : Nat) : gcd (gcd n m) m = gcd n m := by
+@[simp, grind =] theorem gcd_gcd_self_left_right (m n : Nat) : gcd (gcd n m) m = gcd n m := by
   rw [gcd_comm, gcd_gcd_self_right_right]
 
-@[simp] theorem gcd_gcd_self_left_left (m n : Nat) : gcd (gcd m n) m = gcd m n := by
+@[simp, grind =] theorem gcd_gcd_self_left_left (m n : Nat) : gcd (gcd m n) m = gcd m n := by
   rw [gcd_comm m n, gcd_gcd_self_left_right]
 
-@[simp] theorem gcd_add_mul_right_right (m n k : Nat) : gcd m (n + k * m) = gcd m n := by
+@[simp, grind =] theorem gcd_add_mul_right_right (m n k : Nat) : gcd m (n + k * m) = gcd m n := by
   simp [gcd_rec m (n + k * m), gcd_rec m n]
 
 @[deprecated gcd_add_mul_right_right (since := "2025-03-31")]
 theorem gcd_add_mul_self (m n k : Nat) : gcd m (n + k * m) = gcd m n :=
   gcd_add_mul_right_right _ _ _
 
-@[simp] theorem gcd_add_mul_left_right (m n k : Nat) : gcd m (n + m * k) = gcd m n := by
+@[simp, grind =] theorem gcd_add_mul_left_right (m n k : Nat) : gcd m (n + m * k) = gcd m n := by
   rw [Nat.mul_comm, gcd_add_mul_right_right]
 
-@[simp] theorem gcd_mul_right_add_right (m n k : Nat) : gcd m (k * m + n) = gcd m n := by
+@[simp, grind =] theorem gcd_mul_right_add_right (m n k : Nat) : gcd m (k * m + n) = gcd m n := by
   rw [Nat.add_comm, gcd_add_mul_right_right]
 
-@[simp] theorem gcd_mul_left_add_right (m n k : Nat) : gcd m (m * k + n) = gcd m n := by
+@[simp, grind =] theorem gcd_mul_left_add_right (m n k : Nat) : gcd m (m * k + n) = gcd m n := by
   rw [Nat.add_comm, gcd_add_mul_left_right]
 
-@[simp] theorem gcd_add_mul_right_left (m n k : Nat) : gcd (n + k * m) m = gcd n m := by
+@[simp, grind =] theorem gcd_add_mul_right_left (m n k : Nat) : gcd (n + k * m) m = gcd n m := by
   rw [gcd_comm, gcd_add_mul_right_right, gcd_comm]
 
-@[simp] theorem gcd_add_mul_left_left (m n k : Nat) : gcd (n + m * k) m = gcd n m := by
+@[simp, grind =] theorem gcd_add_mul_left_left (m n k : Nat) : gcd (n + m * k) m = gcd n m := by
   rw [Nat.mul_comm, gcd_add_mul_right_left]
 
-@[simp] theorem gcd_mul_right_add_left (m n k : Nat) : gcd (k * m + n) m = gcd n m := by
+@[simp, grind =] theorem gcd_mul_right_add_left (m n k : Nat) : gcd (k * m + n) m = gcd n m := by
   rw [Nat.add_comm, gcd_add_mul_right_left]
 
-@[simp] theorem gcd_mul_left_add_left (m n k : Nat) : gcd (m * k + n) m = gcd n m := by
+@[simp, grind =] theorem gcd_mul_left_add_left (m n k : Nat) : gcd (m * k + n) m = gcd n m := by
   rw [Nat.add_comm, gcd_add_mul_left_left]
 
-@[simp] theorem gcd_add_self_right (m n : Nat) : gcd m (n + m) = gcd m n := by
+@[simp, grind =] theorem gcd_add_self_right (m n : Nat) : gcd m (n + m) = gcd m n := by
   simpa using gcd_add_mul_right_right _ _ 1
 
-@[simp] theorem gcd_self_add_right (m n : Nat) : gcd m (m + n) = gcd m n := by
+@[simp, grind =] theorem gcd_self_add_right (m n : Nat) : gcd m (m + n) = gcd m n := by
   simpa using gcd_mul_right_add_right _ _ 1
 
-@[simp] theorem gcd_add_self_left (m n : Nat) : gcd (n + m) m = gcd n m := by
+@[simp, grind =] theorem gcd_add_self_left (m n : Nat) : gcd (n + m) m = gcd n m := by
   simpa using gcd_add_mul_right_left _ _ 1
 
-@[simp] theorem gcd_self_add_left (m n : Nat) : gcd (m + n) m = gcd n m := by
+@[simp, grind =] theorem gcd_self_add_left (m n : Nat) : gcd (m + n) m = gcd n m := by
   simpa using gcd_mul_right_add_left _ _ 1
 
 @[simp] theorem gcd_add_left_left_of_dvd {m k : Nat} (n : Nat) :
@@ -293,48 +309,48 @@ theorem gcd_add_mul_self (m n k : Nat) : gcd m (n + k * m) = gcd m n :=
     n ∣ k → gcd n (m + k) = gcd n m := by
   rintro ⟨l, rfl⟩; exact gcd_add_mul_left_right n m l
 
-@[simp] theorem gcd_sub_mul_right_right {m n k : Nat} (h : k * m ≤ n) :
+@[simp, grind =] theorem gcd_sub_mul_right_right {m n k : Nat} (h : k * m ≤ n) :
     gcd m (n - k * m) = gcd m n := by
   rw [← gcd_add_mul_right_right m (n - k * m) k, Nat.sub_add_cancel h]
 
-@[simp] theorem gcd_sub_mul_left_right {m n k : Nat} (h : m * k ≤ n) :
+@[simp, grind =] theorem gcd_sub_mul_left_right {m n k : Nat} (h : m * k ≤ n) :
     gcd m (n - m * k) = gcd m n := by
   rw [← gcd_add_mul_left_right m (n - m * k) k, Nat.sub_add_cancel h]
 
-@[simp] theorem gcd_mul_right_sub_right {m n k : Nat} (h : n ≤ k * m) :
+@[simp, grind =] theorem gcd_mul_right_sub_right {m n k : Nat} (h : n ≤ k * m) :
     gcd m (k * m - n) = gcd m n :=
   gcd_right_eq_iff.2 fun _ hl => dvd_sub_iff_right h (Nat.dvd_mul_left_of_dvd hl _)
 
-@[simp] theorem gcd_mul_left_sub_right {m n k : Nat} (h : n ≤ m * k) :
+@[simp, grind =] theorem gcd_mul_left_sub_right {m n k : Nat} (h : n ≤ m * k) :
     gcd m (m * k - n) = gcd m n := by
   rw [Nat.mul_comm, gcd_mul_right_sub_right (Nat.mul_comm _ _ ▸ h)]
 
-@[simp] theorem gcd_sub_mul_right_left {m n k : Nat} (h : k * m ≤ n) :
+@[simp, grind =] theorem gcd_sub_mul_right_left {m n k : Nat} (h : k * m ≤ n) :
     gcd (n - k * m) m = gcd n m := by
   rw [gcd_comm, gcd_sub_mul_right_right h, gcd_comm]
 
-@[simp] theorem gcd_sub_mul_left_left {m n k : Nat} (h : m * k ≤ n) :
+@[simp, grind =] theorem gcd_sub_mul_left_left {m n k : Nat} (h : m * k ≤ n) :
     gcd (n - m * k) m = gcd n m := by
   rw [Nat.mul_comm, gcd_sub_mul_right_left (Nat.mul_comm _ _ ▸ h)]
 
-@[simp] theorem gcd_mul_right_sub_left {m n k : Nat} (h : n ≤ k * m) :
+@[simp, grind =] theorem gcd_mul_right_sub_left {m n k : Nat} (h : n ≤ k * m) :
     gcd (k * m - n) m = gcd n m := by
   rw [gcd_comm, gcd_mul_right_sub_right h, gcd_comm]
 
-@[simp] theorem gcd_mul_left_sub_left {m n k : Nat} (h : n ≤ m * k) :
+@[simp, grind =] theorem gcd_mul_left_sub_left {m n k : Nat} (h : n ≤ m * k) :
     gcd (m * k - n) m = gcd n m := by
   rw [Nat.mul_comm, gcd_mul_right_sub_left (Nat.mul_comm _ _ ▸ h)]
 
-@[simp] theorem gcd_sub_self_right {m n : Nat} (h : m ≤ n) : gcd m (n - m) = gcd m n := by
+@[simp, grind =] theorem gcd_sub_self_right {m n : Nat} (h : m ≤ n) : gcd m (n - m) = gcd m n := by
   simpa using gcd_sub_mul_right_right (k := 1) (by simpa using h)
 
-@[simp] theorem gcd_self_sub_right {m n : Nat} (h : n ≤ m) : gcd m (m - n) = gcd m n := by
+@[simp, grind =] theorem gcd_self_sub_right {m n : Nat} (h : n ≤ m) : gcd m (m - n) = gcd m n := by
   simpa using gcd_mul_right_sub_right (k := 1) (by simpa using h)
 
-@[simp] theorem gcd_sub_self_left {m n : Nat} (h : m ≤ n) : gcd (n - m) m = gcd n m := by
+@[simp, grind =] theorem gcd_sub_self_left {m n : Nat} (h : m ≤ n) : gcd (n - m) m = gcd n m := by
   simpa using gcd_sub_mul_right_left (k := 1) (by simpa using h)
 
-@[simp] theorem gcd_self_sub_left {m n : Nat} (h : n ≤ m) : gcd (m - n) m = gcd n m := by
+@[simp, grind =] theorem gcd_self_sub_left {m n : Nat} (h : n ≤ m) : gcd (m - n) m = gcd n m := by
   simpa using gcd_mul_right_sub_left (k := 1) (by simpa using h)
 
 @[simp] theorem gcd_sub_left_left_of_dvd {n k : Nat} (m : Nat) (h : n ≤ k) :
@@ -399,6 +415,7 @@ protected theorem dvd_mul {k m n : Nat} : k ∣ m * n ↔ ∃ k₁ k₂, k₁
   · rintro ⟨k₁, k₂, hk₁, hk₂, rfl⟩
     exact Nat.mul_dvd_mul hk₁ hk₂
 
+@[grind]
 theorem gcd_mul_right_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) ∣ gcd k m * gcd k n := by
   let ⟨⟨⟨m', hm'⟩, ⟨n', hn'⟩⟩, (h : gcd k (m * n) = m' * n')⟩ :=
     dvdProdDvdOfDvdProd <| gcd_dvd_right k (m * n)
@@ -412,17 +429,21 @@ theorem gcd_mul_right_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) ∣ gcd k m * gc
 theorem gcd_mul_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) ∣ gcd k m * gcd k n :=
   gcd_mul_right_dvd_mul_gcd k m n
 
+@[grind]
 theorem gcd_mul_left_dvd_mul_gcd (k m n : Nat) : gcd (m * n) k ∣ gcd m k * gcd n k := by
   simpa [gcd_comm, Nat.mul_comm] using gcd_mul_right_dvd_mul_gcd _ _ _
 
+@[grind =]
 theorem dvd_gcd_mul_iff_dvd_mul {k n m : Nat} : k ∣ gcd k n * m ↔ k ∣ n * m := by
   refine ⟨(Nat.dvd_trans · <| Nat.mul_dvd_mul_right (k.gcd_dvd_right n) m), fun ⟨y, hy⟩ ↦ ?_⟩
   rw [← gcd_mul_right, hy, gcd_mul_left]
   exact Nat.dvd_mul_right k (gcd m y)
 
+@[grind =]
 theorem dvd_mul_gcd_iff_dvd_mul {k n m : Nat} : k ∣ n * gcd k m ↔ k ∣ n * m := by
   rw [Nat.mul_comm, dvd_gcd_mul_iff_dvd_mul, Nat.mul_comm]
 
+@[grind =]
 theorem dvd_gcd_mul_gcd_iff_dvd_mul {k n m : Nat} : k ∣ gcd k n * gcd k m ↔ k ∣ n * m := by
   rw [dvd_gcd_mul_iff_dvd_mul, dvd_mul_gcd_iff_dvd_mul]
 
@@ -468,6 +489,7 @@ theorem gcd_div_gcd_div_gcd_of_pos_right {n m : Nat} (h : 0 < m) :
     gcd (n / gcd n m) (m / gcd n m) = 1 := by
   rw [gcd_div (gcd_dvd_left _ _) (gcd_dvd_right _ _), Nat.div_self (gcd_pos_of_pos_right _ h)]
 
+@[grind =]
 theorem pow_gcd_pow {k n m : Nat} : gcd (n ^ k) (m ^ k) = (gcd n m) ^ k := by
   refine (Nat.eq_zero_or_pos n).elim (by rintro rfl; cases k <;> simp [Nat.pow_zero]) (fun hn => ?_)
   conv => lhs; rw [← Nat.div_mul_cancel (gcd_dvd_left n m)]
@@ -475,6 +497,7 @@ theorem pow_gcd_pow {k n m : Nat} : gcd (n ^ k) (m ^ k) = (gcd n m) ^ k := by
   rw [Nat.mul_pow, Nat.mul_pow, gcd_mul_right, pow_gcd_pow_of_gcd_eq_one, Nat.one_mul]
   exact gcd_div_gcd_div_gcd_of_pos_left hn
 
+@[grind =]
 theorem pow_dvd_pow_iff {a b n : Nat} (h : n ≠ 0) : a ^ n ∣ b ^ n ↔ a ∣ b := by
   rw [← gcd_eq_left_iff_dvd, ← gcd_eq_left_iff_dvd, pow_gcd_pow, Nat.pow_left_inj h]
 

src/Init/Data/Nat/Lcm.lean

@@ -31,15 +31,17 @@ def lcm (m n : Nat) : Nat := m * n / gcd m n
 
 theorem lcm_eq_mul_div (m n : Nat) : lcm m n = m * n / gcd m n := rfl
 
-@[simp] theorem gcd_mul_lcm (m n : Nat) : gcd m n * lcm m n = m * n := by
+@[simp, grind =] theorem gcd_mul_lcm (m n : Nat) : gcd m n * lcm m n = m * n := by
   rw [lcm_eq_mul_div,
     Nat.mul_div_cancel' (Nat.dvd_trans (gcd_dvd_left m n) (Nat.dvd_mul_right m n))]
 
-@[simp] theorem lcm_mul_gcd (m n : Nat) : lcm m n * gcd m n = m * n := by
+@[simp, grind =] theorem lcm_mul_gcd (m n : Nat) : lcm m n * gcd m n = m * n := by
   simp [Nat.mul_comm]
 
 @[simp] theorem lcm_dvd_mul (m n : Nat) : lcm m n ∣ m * n := ⟨gcd m n, by simp⟩
 
+grind_pattern lcm_dvd_mul => lcm m n
+
 @[simp] theorem gcd_dvd_mul (m n : Nat) : gcd m n ∣ m * n := ⟨lcm m n, by simp⟩
 
 @[simp] theorem lcm_le_mul {m n : Nat} (hm : 0 < m) (hn : 0 < n) : lcm m n ≤ m * n :=
@@ -48,22 +50,23 @@ theorem lcm_eq_mul_div (m n : Nat) : lcm m n = m * n / gcd m n := rfl
 @[simp] theorem gcd_le_mul {m n : Nat} (hm : 0 < m) (hn : 0 < n) : gcd m n ≤ m * n :=
   le_of_dvd (Nat.mul_pos hm hn) (gcd_dvd_mul _ _)
 
+@[grind =]
 theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
   rw [lcm_eq_mul_div, lcm_eq_mul_div, Nat.mul_comm n m, gcd_comm n m]
 instance : Std.Commutative lcm := ⟨lcm_comm⟩
 
-@[simp] theorem lcm_zero_left (m : Nat) : lcm 0 m = 0 := by simp [lcm_eq_mul_div]
+@[simp, grind =] theorem lcm_zero_left (m : Nat) : lcm 0 m = 0 := by simp [lcm_eq_mul_div]
 
-@[simp] theorem lcm_zero_right (m : Nat) : lcm m 0 = 0 := by simp [lcm_eq_mul_div]
+@[simp, grind =] theorem lcm_zero_right (m : Nat) : lcm m 0 = 0 := by simp [lcm_eq_mul_div]
 
-@[simp] theorem lcm_one_left (m : Nat) : lcm 1 m = m := by simp [lcm_eq_mul_div]
+@[simp, grind =] theorem lcm_one_left (m : Nat) : lcm 1 m = m := by simp [lcm_eq_mul_div]
 
-@[simp] theorem lcm_one_right (m : Nat) : lcm m 1 = m := by simp [lcm_eq_mul_div]
+@[simp, grind =] theorem lcm_one_right (m : Nat) : lcm m 1 = m := by simp [lcm_eq_mul_div]
 instance : Std.LawfulIdentity lcm 1 where
   left_id := lcm_one_left
   right_id := lcm_one_right
 
-@[simp] theorem lcm_self (m : Nat) : lcm m m = m := by
+@[simp, grind =] theorem lcm_self (m : Nat) : lcm m m = m := by
   match eq_zero_or_pos m with
   | .inl h => rw [h, lcm_zero_left]
   | .inr h => simp [lcm_eq_mul_div, Nat.mul_div_cancel _ h]
@@ -72,8 +75,12 @@ instance : Std.IdempotentOp lcm := ⟨lcm_self⟩
 theorem dvd_lcm_left (m n : Nat) : m ∣ lcm m n :=
   ⟨n / gcd m n, by rw [← Nat.mul_div_assoc m (Nat.gcd_dvd_right m n), lcm_eq_mul_div]⟩
 
+grind_pattern dvd_lcm_left => lcm m n
+
 theorem dvd_lcm_right (m n : Nat) : n ∣ lcm m n := lcm_comm n m ▸ dvd_lcm_left n m
 
+grind_pattern dvd_lcm_right => lcm m n
+
 theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
   intro h
   have h1 := gcd_mul_lcm m n
@@ -101,6 +108,7 @@ theorem lcm_dvd {m n k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) : lcm m n ∣ k := b
     rw [gcd_mul_lcm, ← gcd_mul_right, Nat.mul_comm n k]
     exact dvd_gcd (Nat.mul_dvd_mul_left _ H2) (Nat.mul_dvd_mul_right H1 _)
 
+@[grind =]
 theorem lcm_dvd_iff {m n k : Nat} : lcm m n ∣ k ↔ m ∣ k ∧ n ∣ k :=
   ⟨fun h => ⟨Nat.dvd_trans (dvd_lcm_left _ _) h, Nat.dvd_trans (dvd_lcm_right _ _) h⟩,
    fun ⟨hm, hn⟩ => lcm_dvd hm hn⟩
@@ -113,6 +121,7 @@ theorem lcm_eq_left_iff_dvd : lcm m n = m ↔ n ∣ m := by
 theorem lcm_eq_right_iff_dvd : lcm m n = n ↔ m ∣ n := by
   rw [lcm_comm, lcm_eq_left_iff_dvd]
 
+@[grind _=_]
 theorem lcm_assoc (m n k : Nat) : lcm (lcm m n) k = lcm m (lcm n k) :=
 Nat.dvd_antisymm
   (lcm_dvd
@@ -125,12 +134,14 @@ Nat.dvd_antisymm
       (dvd_lcm_right (lcm m n) k)))
 instance : Std.Associative lcm := ⟨lcm_assoc⟩
 
+@[grind =]
 theorem lcm_mul_left (m n k : Nat) : lcm (m * n) (m * k) = m * lcm n k := by
   refine (Nat.eq_zero_or_pos m).elim (by rintro rfl; simp) (fun hm => ?_)
   rw [lcm_eq_mul_div, gcd_mul_left,
     Nat.mul_div_assoc _ (Nat.mul_dvd_mul_left _ (gcd_dvd_right _ _)), Nat.mul_div_mul_left _ _ hm,
     lcm_eq_mul_div, Nat.mul_div_assoc _ (gcd_dvd_right _ _), Nat.mul_assoc]
 
+@[grind =]
 theorem lcm_mul_right (m n k : Nat) : lcm (m * n) (k * n) = lcm m k * n := by
   rw [Nat.mul_comm _ n, Nat.mul_comm _ n, Nat.mul_comm _ n, lcm_mul_left]
 
@@ -150,6 +161,7 @@ theorem lcm_eq_iff {n m l : Nat} :
     exact ⟨dvd_lcm_left _ _, dvd_lcm_right _ _, fun _ => Nat.lcm_dvd⟩
   · exact hl _ (dvd_lcm_left _ _) (dvd_lcm_right _ _)
 
+@[grind =]
 theorem lcm_div {m n k : Nat} (hkm : k ∣ m) (hkn : k ∣ n) : lcm (m / k) (n / k) = lcm m n / k := by
   refine (Nat.eq_zero_or_pos k).elim (by rintro rfl; simp) (fun hk => lcm_eq_iff.2
     ⟨Nat.div_dvd_div hkm (dvd_lcm_left m n), Nat.div_dvd_div hkn (dvd_lcm_right m n),
@@ -160,21 +172,27 @@ theorem lcm_div {m n k : Nat} (hkm : k ∣ m) (hkn : k ∣ n) : lcm (m / k) (n /
   · exact hkn
   · exact hkm
 
+@[grind]
 theorem lcm_dvd_lcm_of_dvd_left {m k : Nat} (n : Nat) (h : m ∣ k) : lcm m n ∣ lcm k n :=
   lcm_dvd (Nat.dvd_trans h (dvd_lcm_left _ _)) (dvd_lcm_right _ _)
 
+@[grind]
 theorem lcm_dvd_lcm_of_dvd_right {m k : Nat} (n : Nat) (h : m ∣ k) : lcm n m ∣ lcm n k :=
   lcm_dvd (dvd_lcm_left _ _) (Nat.dvd_trans h (dvd_lcm_right _ _))
 
+@[grind]
 theorem lcm_dvd_lcm_mul_left_left (m n k : Nat) : lcm m n ∣ lcm (k * m) n :=
   lcm_dvd_lcm_of_dvd_left _ (Nat.dvd_mul_left _ _)
 
+@[grind]
 theorem lcm_dvd_lcm_mul_right_left (m n k : Nat) : lcm m n ∣ lcm (m * k) n :=
   lcm_dvd_lcm_of_dvd_left _ (Nat.dvd_mul_right _ _)
 
+@[grind]
 theorem lcm_dvd_lcm_mul_left_right (m n k : Nat) : lcm m n ∣ lcm m (k * n) :=
   lcm_dvd_lcm_of_dvd_right _ (Nat.dvd_mul_left _ _)
 
+@[grind]
 theorem lcm_dvd_lcm_mul_right_right (m n k : Nat) : lcm m n ∣ lcm m (n * k) :=
   lcm_dvd_lcm_of_dvd_right _ (Nat.dvd_mul_right _ _)
 
@@ -184,16 +202,16 @@ theorem lcm_eq_left {m n : Nat} (h : n ∣ m) : lcm m n = m :=
 theorem lcm_eq_right {m n : Nat} (h : m ∣ n) : lcm m n = n :=
   lcm_eq_right_iff_dvd.2 h
 
-@[simp] theorem lcm_mul_left_left (m n : Nat) : lcm (m * n) n = m * n := by
+@[simp, grind =] theorem lcm_mul_left_left (m n : Nat) : lcm (m * n) n = m * n := by
   simpa [lcm_eq_iff, Nat.dvd_mul_left] using fun _ h _ => h
 
-@[simp] theorem lcm_mul_left_right (m n : Nat) : lcm n (m * n) = m * n := by
+@[simp, grind =] theorem lcm_mul_left_right (m n : Nat) : lcm n (m * n) = m * n := by
   simp [lcm_eq_iff, Nat.dvd_mul_left]
 
-@[simp] theorem lcm_mul_right_left (m n : Nat) : lcm (n * m) n = n * m := by
+@[simp, grind =] theorem lcm_mul_right_left (m n : Nat) : lcm (n * m) n = n * m := by
   simpa [lcm_eq_iff, Nat.dvd_mul_right] using fun _ h _ => h
 
-@[simp] theorem lcm_mul_right_right (m n : Nat) : lcm n (n * m) = n * m := by
+@[simp, grind =] theorem lcm_mul_right_right (m n : Nat) : lcm n (n * m) = n * m := by
   simp [lcm_eq_iff, Nat.dvd_mul_right]
 
 @[simp] theorem lcm_lcm_self_right_left (m n : Nat) : lcm m (lcm m n) = lcm m n := by
@@ -215,16 +233,20 @@ theorem lcm_eq_mul_iff {m n : Nat} : lcm m n = m * n ↔ m = 0 ∨ n = 0 ∨ gcd
   refine ⟨fun h => ⟨?_, ?_⟩, by rintro ⟨rfl, rfl⟩; simp⟩ <;>
     (apply Nat.eq_one_of_dvd_one; simp [← h, dvd_lcm_left, dvd_lcm_right])
 
+@[grind]
 theorem lcm_mul_right_dvd_mul_lcm (k m n : Nat) : lcm k (m * n) ∣ lcm k m * lcm k n :=
   lcm_dvd (Nat.dvd_mul_left_of_dvd (dvd_lcm_left _ _) _)
     (Nat.mul_dvd_mul (dvd_lcm_right _ _) (dvd_lcm_right _ _))
 
+@[grind]
 theorem lcm_mul_left_dvd_mul_lcm (k m n : Nat) : lcm (m * n) k ∣ lcm m k * lcm n k := by
   simpa [lcm_comm, Nat.mul_comm] using lcm_mul_right_dvd_mul_lcm _ _ _
 
+@[grind =]
 theorem lcm_dvd_mul_self_left_iff_dvd_mul {k n m : Nat} : lcm k n ∣ k * m ↔ n ∣ k * m :=
   ⟨fun h => Nat.dvd_trans (dvd_lcm_right _ _) h, fun h => lcm_dvd (Nat.dvd_mul_right k m) h⟩
 
+@[grind =]
 theorem lcm_dvd_mul_self_right_iff_dvd_mul {k m n : Nat} : lcm n k ∣ m * k ↔ n ∣ m * k := by
   rw [lcm_comm, Nat.mul_comm m, lcm_dvd_mul_self_left_iff_dvd_mul]
 
@@ -247,6 +269,7 @@ theorem lcm_mul_left_left_eq_mul_of_lcm_eq_mul {n m k} (h : lcm n m = n * m) :
     lcm (k * n) m = n * lcm k m := by
   rw [Nat.mul_comm, lcm_mul_right_left_eq_mul_of_lcm_eq_mul h]
 
+@[grind =]
 theorem pow_lcm_pow {k n m : Nat} : lcm (n ^ k) (m ^ k) = (lcm n m) ^ k := by
   rw [lcm_eq_mul_div, pow_gcd_pow, ← Nat.mul_pow, ← Nat.div_pow (gcd_dvd_mul _ _), lcm_eq_mul_div]
 

tests/lean/run/grind_cutsat_div_1.lean

@@ -22,7 +22,10 @@ theorem ex₄ (f : Int → Int) (a b : Int) (_ : 2 ∣ f (f a) + 1) (h₁ : 3
 /--
 trace: [grind.debug.cutsat.search.assign] a := 1
 [grind.debug.cutsat.search.assign] b := 0
+[grind.debug.cutsat.search.assign] ↑0 := 0
+[grind.debug.cutsat.search.assign] ↑1 := 1
 [grind.debug.cutsat.search.assign] 「1」 := 1
+[grind.debug.cutsat.search.assign] 「0」 := 0
 -/
 #guard_msgs (trace) in -- finds the model without any backtracking
 set_option trace.grind.debug.cutsat.search.assign true in
@@ -31,12 +34,18 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) : False := by
   sorry
 
 /--
-trace: [grind.cutsat.assert] -1*「1」 + 1 = 0
+trace: [grind.cutsat.assert] -1*「0」 = 0
+[grind.cutsat.assert] -1*「1」 + 1 = 0
+[grind.cutsat.assert] -1*↑1 + 1 = 0
+[grind.cutsat.assert] -1*↑0 = 0
 [grind.cutsat.assert] 2 ∣ a + 3
 [grind.cutsat.assert] 3 ∣ a + 3*b + -4
 [grind.debug.cutsat.search.assign] a := 1
 [grind.debug.cutsat.search.assign] b := 0
+[grind.debug.cutsat.search.assign] ↑0 := 0
+[grind.debug.cutsat.search.assign] ↑1 := 1
 [grind.debug.cutsat.search.assign] 「1」 := 1
+[grind.debug.cutsat.search.assign] 「0」 := 0
 -/
 #guard_msgs (trace) in
 set_option trace.grind.cutsat.assert true in
@@ -48,7 +57,10 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + 3*b - 4) : False := by
 /--
 trace: [grind.debug.cutsat.search.assign] a := 1
 [grind.debug.cutsat.search.assign] b := 15
+[grind.debug.cutsat.search.assign] ↑0 := 0
+[grind.debug.cutsat.search.assign] ↑1 := 1
 [grind.debug.cutsat.search.assign] 「1」 := 1
+[grind.debug.cutsat.search.assign] 「0」 := 0
 -/
 #guard_msgs (trace) in
 set_option trace.grind.debug.cutsat.search.assign true in
@@ -59,7 +71,10 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b < 18): False
 /--
 trace: [grind.debug.cutsat.search.assign] a := 1
 [grind.debug.cutsat.search.assign] b := 12
+[grind.debug.cutsat.search.assign] ↑0 := 0
+[grind.debug.cutsat.search.assign] ↑1 := 1
 [grind.debug.cutsat.search.assign] 「1」 := 1
+[grind.debug.cutsat.search.assign] 「0」 := 0
 -/
 #guard_msgs (trace) in
 set_option trace.grind.debug.cutsat.search.assign true in
@@ -70,8 +85,10 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b ≥ 11): Fals
 /--
 trace: [grind.debug.cutsat.search.assign] f 0 := 11
 [grind.debug.cutsat.search.assign] f 1 := 2
-[grind.debug.cutsat.search.assign] 「0」 := 0
+[grind.debug.cutsat.search.assign] ↑0 := 0
+[grind.debug.cutsat.search.assign] ↑1 := 1
 [grind.debug.cutsat.search.assign] 「1」 := 1
+[grind.debug.cutsat.search.assign] 「0」 := 0
 -/
 #guard_msgs (trace) in
 set_option trace.grind.debug.cutsat.search.assign true in

tests/lean/run/grind_gcd.lean

@@ -0,0 +1,21 @@
+open Nat
+
+theorem gcd_self (n : Nat) : gcd n n = n := by grind
+
+theorem gcd_eq_left_iff_dvd : gcd m n = m ↔ m ∣ n :=
+  ⟨by grind, by grind [gcd_eq_iff]⟩
+
+theorem gcd_eq_right_iff_dvd : gcd n m = m ↔ m ∣ n := by
+  grind [Nat.gcd_eq_left_iff_dvd]
+
+theorem lcm_self (m : Nat) : lcm m m = m := by grind
+
+theorem lcm_lcm_self_right_left (m n : Nat) : lcm m (lcm m n) = lcm m n := by grind
+
+theorem lcm_lcm_self_right_right (m n : Nat) : lcm m (lcm n m) = lcm m n := by grind
+
+theorem neg_fmod_self (a : Int) : (-a).fmod a = 0 := by grind
+
+theorem bmod_self {a : Nat} : Int.bmod a a = 0 := by grind
+
+theorem neg_bmod_self {a : Nat} : Int.bmod (-a) a = 0 := by grind