chore: golf using grind. add grind annotations. (#32738)

Author: euprunin

Mathlib/Data/Finsupp/Basic.lean

@@ -1110,10 +1110,7 @@ theorem extendDomain_eq_embDomain_subtype (f : Subtype P →₀ M) :
 
 theorem support_extendDomain_subset (f : Subtype P →₀ M) :
     ↑(f.extendDomain).support ⊆ {x | P x} := by
-  intro x
-  rw [extendDomain_support, mem_coe, mem_map, Embedding.coe_subtype]
-  rintro ⟨x, -, rfl⟩
-  exact x.prop
+  grind
 
 @[simp]
 theorem subtypeDomain_extendDomain (f : Subtype P →₀ M) :

Mathlib/Data/Nat/PrimeFin.lean

@@ -36,7 +36,7 @@ def primeFactors (n : ℕ) : Finset ℕ := n.primeFactorsList.toFinset
 
 @[simp] lemma toFinset_factors (n : ℕ) : n.primeFactorsList.toFinset = n.primeFactors := rfl
 
-@[simp] lemma mem_primeFactors : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
+@[simp, grind =] lemma mem_primeFactors : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n ∧ n ≠ 0 := by
   simp_rw [← toFinset_factors, List.mem_toFinset, mem_primeFactorsList']
 
 lemma mem_primeFactors_of_ne_zero (hn : n ≠ 0) : p ∈ n.primeFactors ↔ p.Prime ∧ p ∣ n := by

Mathlib/Data/Seq/Basic.lean

@@ -157,7 +157,7 @@ theorem take_succ_cons {n : ℕ} {x : α} {s : Seq α} :
     (cons x s).take (n + 1) = x :: s.take n := by
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem getElem?_take : ∀ (n k : ℕ) (s : Seq α),
     (s.take k)[n]? = if n < k then s.get? n else none
   | n, 0, s => by simp [take]
@@ -488,7 +488,7 @@ end Join
 
 section Drop
 
-@[simp]
+@[simp, grind =]
 theorem drop_get? {n m : ℕ} {s : Seq α} : (s.drop n).get? m = s.get? (n + m) := by
   induction n generalizing m with
   | zero => simp [drop]
@@ -541,18 +541,8 @@ theorem drop_length' {n : ℕ} {s : Seq α} :
 
 theorem take_drop {s : Seq α} {n m : ℕ} :
     (s.take n).drop m = (s.drop m).take (n - m) := by
-  induction m generalizing n s with
-  | zero => simp [drop]
-  | succ k ih =>
-    cases s
-    · simp
-    cases n with
-    | zero => simp
-    | succ l =>
-      simp only [take, destruct_cons, List.drop_succ_cons, Nat.reduceSubDiff]
-      rw [ih]
-      congr 1
-      rw [drop_succ_cons]
+  ext
+  grind
 
 end Drop
 

Mathlib/LinearAlgebra/Lagrange.lean

@@ -452,17 +452,7 @@ theorem interpolate_eq_add_interpolate_erase (hvs : Set.InjOn v s) (hi : i ∈ s
 open scoped Classical in
 theorem interpolate_poly_eq_self
     (hvs : Set.InjOn v s) {P : Polynomial F} (hP : P.degree < s.card) :
-    interpolate s v (fun i => P.eval (v i)) = P := by
-  classical
-  let t : Finset F := s.image v
-  have ht : t.card = s.card := Finset.card_image_iff.mpr hvs
-  apply eq_of_degrees_lt_of_eval_finset_eq t
-  · rw [ht]
-    apply degree_interpolate_lt _ hvs
-  · rwa [ht]
-  · intro x hx
-    obtain ⟨i, hi, rfl⟩ := Finset.mem_image.mp hx
-    rw [eval_interpolate_at_node _ hvs hi]
+    interpolate s v (fun i => P.eval (v i)) = P := (eq_interpolate hvs hP).symm
 
 theorem leadingCoeff_eq_sum
     (hvs : Set.InjOn v s) {P : Polynomial F} (hP : s.card = P.degree + 1) :

Mathlib/NumberTheory/Divisors.lean

@@ -106,7 +106,7 @@ theorem cons_self_properDivisors (h : n ≠ 0) :
     cons n (properDivisors n) self_notMem_properDivisors = divisors n := by
   rw [cons_eq_insert, insert_self_properDivisors h]
 
-@[simp]
+@[simp, grind =]
 theorem mem_divisors {m : ℕ} : n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0 := by
   rcases eq_or_ne m 0 with (rfl | hm); · simp [divisors]
   simp only [hm, Ne, not_false_iff, and_true, ← filter_dvd_eq_divisors hm, mem_filter,
@@ -554,10 +554,8 @@ theorem prod_divisorsAntidiagonal' {M : Type*} [CommMonoid M] (f : ℕ → ℕ 
 /-- The factors of `n` are the prime divisors -/
 theorem primeFactors_eq_to_filter_divisors_prime (n : ℕ) :
     n.primeFactors = {p ∈ divisors n | p.Prime} := by
-  rcases n.eq_zero_or_pos with (rfl | hn)
-  · simp
-  · ext q
-    simpa [hn, hn.ne', mem_primeFactorsList] using and_comm
+  ext
+  grind
 
 lemma primeFactors_filter_dvd_of_dvd {m n : ℕ} (hn : n ≠ 0) (hmn : m ∣ n) :
     {p ∈ n.primeFactors | p ∣ m} = m.primeFactors := by

Mathlib/NumberTheory/SumTwoSquares.lean

@@ -225,7 +225,7 @@ theorem Nat.eq_sq_add_sq_iff {n : ℕ} :
   -- now `0 < n`
   refine eq_sq_add_sq_iff_eq_sq_mul.trans ⟨fun ⟨a, b, h₁, h₂⟩ q hq h ↦ ?_, fun H ↦ ?_⟩
   · have : Fact q.Prime := ⟨prime_of_mem_primeFactors hq⟩
-    have : q ∣ b → q ∈ b.primeFactors := by grind [mem_primeFactors]
+    have : q ∣ b → q ∈ b.primeFactors := by grind
     grind (splits := 10) [padicValNat.mul, padicValNat.pow,
       padicValNat.eq_zero_of_not_dvd, mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one]
   · obtain ⟨b, a, hb₀, ha₀, hab, hb⟩ := sq_mul_squarefree_of_pos hn₀