chore: absorb steps into terminal grind (leanprover-community#32713)

kim-em · kim-em · commit 798365a9ee67 · 2025-12-11T11:46:53.000Z
This PR takes existing proofs that end with `grind`, and absorbs steps before `grind` that aren't needed. From [#mathlib4 > Weekly linting log @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Weekly.20linting.20log/near/562390081)
diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Interval.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Interval.lean
@@ -41,9 +41,6 @@ lemma prod_Icc_succ_eq_mul_endpoints {R : Type*} [CommGroup R] (f : ℤ → R) {
     f (N + 1) * f (-(N + 1) : ℤ) * ∏ m ∈ Icc (-N : ℤ) N, f m := by
   induction N
   · rw [Icc_succ_succ]
-    simp only [CharP.cast_eq_zero, neg_zero, Icc_self, zero_add, Int.reduceNeg, union_insert,
-      union_singleton, mem_insert, reduceCtorEq, mem_singleton, neg_eq_zero, one_ne_zero, or_self,
-      not_false_eq_true, prod_insert, prod_singleton]
     grind
   · rw [Icc_succ_succ, prod_union (by simp)]
     grind
diff --git a/Mathlib/Algebra/Polynomial/RuleOfSigns.lean b/Mathlib/Algebra/Polynomial/RuleOfSigns.lean
@@ -268,7 +268,6 @@ private lemma exists_cons_of_leadingCoeff_pos (η) (h₁ : 0 < leadingCoeff P) (
           monomial P.natDegree P.nextCoeff - C η * monomial P.natDegree P.leadingCoeff by
         grind [X_mul_monomial, sub_mul, mul_sub, self_sub_monomial_natDegree_leadingCoeff,
           natDegree_eraseLead_add_one, leadingCoeff_eraseLead_eq_nextCoeff]
-      rw [nextCoeff_of_natDegree_pos (h₇ ▸ P.natDegree.succ_pos), h₇] at h₉
       grind [coeff_X_sub_C_mul, C_mul_monomial, nextCoeff_of_natDegree_pos, leadingCoeff]
   · rw [h_cons, leadingCoeff_mul, leadingCoeff_X_sub_C, one_mul, h₂]
 
diff --git a/Mathlib/Analysis/Analytic/Order.lean b/Mathlib/Analysis/Analytic/Order.lean
@@ -370,8 +370,6 @@ theorem isClopen_setOf_analyticOrderAt_eq_top (hf : AnalyticOnNhd 𝕜 f U) :
     obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
     use Subtype.val ⁻¹' t'
     simp only [isOpen_induced h₂t', mem_preimage, h₃t', and_self, and_true]
-    intro w hw
-    simp only [mem_setOf_eq]
     grind
 
 /-- On a connected set, there exists a point where a meromorphic function `f` has finite order iff
diff --git a/Mathlib/CategoryTheory/Filtered/Basic.lean b/Mathlib/CategoryTheory/Filtered/Basic.lean
@@ -245,11 +245,7 @@ theorem sup_exists :
     rw [← Category.assoc]
     by_cases h : X = X' ∧ Y = Y'
     · rcases h with ⟨rfl, rfl⟩
-      by_cases hf : f = f'
-      · subst hf
-        apply coeq_condition
-      · rw [@w' _ _ mX mY f']
-        grind
+      grind [coeq_condition]
     · rw [@w' _ _ mX' mY' f' _]
       apply Finset.mem_of_mem_insert_of_ne mf'
       contrapose! h
diff --git a/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean
@@ -114,7 +114,6 @@ theorem map_injective_of_injective {f : G →g G'} (hinj : Function.Injective f)
     | nil => simp at h
     | cons _ _ =>
       simp only [map_cons, cons.injEq] at h
-      cases hinj h.1
       grind
 
 section mapLe
diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean
@@ -1208,10 +1208,7 @@ lemma find_of_find_le {p : Fin (m + n) → Prop} [DecidablePred p]
 
 theorem find?_eq_dite {p : Fin n → Bool} :
     find? p = if h : ∃ i, p i then some (Fin.find (p ·) h) else none := by
-  split_ifs with h
-  · simp_rw [find?_eq_some_iff, Fin.find_spec h, lt_find_iff]
-    grind
-  · simpa [find?_eq_none_iff] using h
+  split_ifs <;> grind
 
 theorem find?_decide_eq_dite :
     find? (p ·) = if h : ∃ i, p i then some (Fin.find p h) else none := by
diff --git a/Mathlib/Data/Finset/Pi.lean b/Mathlib/Data/Finset/Pi.lean
@@ -122,9 +122,7 @@ theorem pi_insert [∀ a, DecidableEq (β a)] {s : Finset α} {t : ∀ a : α, F
   exact ((pi s t).nodup.map <| Multiset.Pi.cons_injective ha).dedup.symm
 
 theorem pi_singletons {β : Type*} (s : Finset α) (f : α → β) :
-    (s.pi fun a => ({f a} : Finset β)) = {fun a _ => f a} := by
-  ext
-  grind
+    (s.pi fun a => ({f a} : Finset β)) = {fun a _ => f a} := by grind
 
 theorem pi_const_singleton {β : Type*} (s : Finset α) (i : β) :
     (s.pi fun _ => ({i} : Finset β)) = {fun _ _ => i} :=
diff --git a/Mathlib/Data/Nat/Sqrt.lean b/Mathlib/Data/Nat/Sqrt.lean
@@ -106,7 +106,6 @@ private lemma sqrt_isSqrt (n : ℕ) : IsSqrt n (sqrt n) := by
     simp only [shiftLeft_eq, Nat.one_mul]
     refine Nat.le_of_lt (Nat.le_trans lt_log2_self (le_add_right_of_le ?_))
     rw [← Nat.pow_add]
-    apply Nat.pow_le_pow_right (by decide)
     grind
 
 lemma sqrt_le (n : ℕ) : sqrt n * sqrt n ≤ n := (sqrt_isSqrt n).left
diff --git a/Mathlib/Data/PFun.lean b/Mathlib/Data/PFun.lean
@@ -497,7 +497,6 @@ theorem dom_comp (f : β →. γ) (g : α →. β) : (f.comp g).Dom = g.preimage
 @[simp]
 theorem preimage_comp (f : β →. γ) (g : α →. β) (s : Set γ) :
     (f.comp g).preimage s = g.preimage (f.preimage s) := by
-  ext
   grind
 
 @[simp]
diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean
@@ -139,7 +139,7 @@ theorem MonotoneOn.intervalIntegral_deriv_mem_uIcc {f : ℝ → ℝ} {a b : ℝ}
     refine intervalIntegral.integral_congr_ae ?_
     rw [uIoc_of_le hab]
     filter_upwards [h₂] with x _ _
-    exact abs_eq_self.mpr (f_deriv_nonneg (by rw [← Ioc_diff_right]; grind)) |>.symm
+    exact abs_eq_self.mpr (f_deriv_nonneg (by grind)) |>.symm
 
 /-- If `f` has bounded variation on `uIcc a b`, then `f'` is interval integrable on `a..b`. -/
 theorem BoundedVariationOn.intervalIntegrable_deriv {f : ℝ → ℝ} {a b : ℝ}
diff --git a/Mathlib/Order/Interval/Finset/Basic.lean b/Mathlib/Order/Interval/Finset/Basic.lean
@@ -856,39 +856,26 @@ theorem Ico_union_Ico {a b c d : α} (h₁ : min a b ≤ max c d) (h₂ : min c
 theorem Ico_inter_Ico {a b c d : α} : Ico a b ∩ Ico c d = Ico (max a c) (min b d) := by
   rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]
 
-theorem Ioc_inter_Ioc {a b c d : α} : Ioc a b ∩ Ioc c d = Ioc (max a c) (min b d) := by
-  grind
+theorem Ioc_inter_Ioc {a b c d : α} : Ioc a b ∩ Ioc c d = Ioc (max a c) (min b d) := by grind
 
 @[simp]
-theorem Ico_filter_lt (a b c : α) : {x ∈ Ico a b | x < c} = Ico a (min b c) := by
-  ext
-  grind
+theorem Ico_filter_lt (a b c : α) : {x ∈ Ico a b | x < c} = Ico a (min b c) := by grind
 
 @[simp]
-theorem Ico_filter_le (a b c : α) : {x ∈ Ico a b | c ≤ x} = Ico (max a c) b := by
-  ext
-  grind
+theorem Ico_filter_le (a b c : α) : {x ∈ Ico a b | c ≤ x} = Ico (max a c) b := by grind
 
 @[simp]
-theorem Ioo_filter_lt (a b c : α) : {x ∈ Ioo a b | x < c} = Ioo a (min b c) := by
-  ext
-  simp [and_assoc]
+theorem Ioo_filter_lt (a b c : α) : {x ∈ Ioo a b | x < c} = Ioo a (min b c) := by grind
 
 @[simp]
 theorem Iio_filter_lt {α} [LinearOrder α] [LocallyFiniteOrderBot α] (a b : α) :
-    {x ∈ Iio a | x < b} = Iio (min a b) := by
-  ext
-  simp
+    {x ∈ Iio a | x < b} = Iio (min a b) := by grind
 
 @[simp]
-theorem Ico_diff_Ico_left (a b c : α) : Ico a b \ Ico a c = Ico (max a c) b := by
-  ext
-  grind
+theorem Ico_diff_Ico_left (a b c : α) : Ico a b \ Ico a c = Ico (max a c) b := by grind
 
 @[simp]
-theorem Ico_diff_Ico_right (a b c : α) : Ico a b \ Ico c b = Ico a (min b c) := by
-  ext
-  grind
+theorem Ico_diff_Ico_right (a b c : α) : Ico a b \ Ico c b = Ico a (min b c) := by grind
 
 @[simp]
 theorem Ioc_disjoint_Ioc : Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ := by
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean b/Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
@@ -287,9 +287,7 @@ theorem hasProd_prod_support_of_ne_finset_one (hf : ∀ b ∈ L.support, b ∉ s
     (L.filter.biInter_mem (Set.toFinite _)).mpr (fun b hb ↦ hb.2)
   filter_upwards [h1, L.eventually_le_support] with t ht ht'
   simp only [Set.mem_iInter] at ht
-  apply Finset.prod_congr_of_eq_on_inter <;>
-  · simp only [Set.mem_toFinset]
-    grind
+  apply Finset.prod_congr_of_eq_on_inter <;> grind
 
 /-- If a function `f` is `1` outside of a finite set `s`, then it `HasProd` `∏ b ∈ s, f b`. -/
 @[to_additive /-- If a function `f` vanishes outside of a finite set `s`, then it `HasSum`
