chore: simplify simp/grind patterns as suggested by linter (leanprover-community#34714)

This PR removes redundant `simp`, `simp only`, and `have` statements before `grind` where grind can handle the goal directly, as suggested by the grind linter in the nightly testing run.

Addresses 6 of the 14 warnings from https://github.com/leanprover-community/mathlib4/actions/runs/21578471064

Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Weekly.20linting.20log/near/571353143

The remaining warnings involve cases where the preprocessing step (`norm_cast`, `ext`, `convert_to`, etc.) is actually necessary for grind to succeed.

🤖 Prepared with Claude Code

Author: kim-em

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -797,7 +797,7 @@ theorem prod_biUnion_of_pairwise_eq_one [DecidableEq ι] {s : Finset κ} {t : κ
     ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i := by
   classical
   let t' k := (t k).filter (fun i ↦ f i ≠ 1)
-  have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by ext; simp [t']; grind
+  have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by ext; grind
   rw [← prod_filter_ne_one, ← this, prod_biUnion]
   swap
   · intro i hi j hj hij a hai haj k hk

Mathlib/Data/Setoid/Partition.lean

@@ -510,8 +510,7 @@ noncomputable def coarserPartition (hs : IndexedPartition s) {κ : Type*} (g : 
     simp only [← hd, mem_iUnion] at hb
     have : c = d := hs.eq_of_mem ha.2 hb.2
     by_contra!
-    have : c ≠ d := disjoint_iff_forall_ne.mp ((disjoint_singleton.mpr this).preimage g) ha.1 hb.1
-    grind
+    grind [disjoint_iff_forall_ne.mp ((disjoint_singleton.mpr this).preimage g) ha.1 hb.1]
   some k := hs.some ((singleton_nonempty k).preimage hg).some
   some_mem k := by
     refine mem_iUnion_of_mem ((singleton_nonempty k).preimage hg).some ?_

Mathlib/MeasureTheory/Measure/AddContent.lean

@@ -255,8 +255,7 @@ private lemma AddContent.supClosureFun_apply_of_mem (hC : IsSetSemiring C)
       rw [hJs i hi]
       exact subset_sUnion_of_mem ha
     let K : Finset (Set α) := Finset.biUnion I J
-    have : ⋃₀ ↑I = ⋃₀ (↑K : Set (Set α)) := by
-      simp [K, sUnion_eq_biUnion] at hJs ⊢; grind
+    have : ⋃₀ ↑I = ⋃₀ (↑K : Set (Set α)) := by grind
     rw [this, m.supClosureFun_apply hC (J := K) (by simpa [K] using hJC) _ rfl]; swap
     · simp only [K, coe_biUnion]
       refine (h'I.mono_on ?_).biUnion hJdisj

Mathlib/NumberTheory/FactorisationProperties.lean

@@ -220,7 +220,6 @@ theorem abundancyIndex_le_of_dvd (hn : n ≠ 0) (hd : m ∣ n) :
 
 theorem Abundant.of_dvd (h : Abundant m) (hd : m ∣ n) (hn : n ≠ 0) : Abundant n := by
   have := abundancyIndex_le_of_dvd hn hd
-  have := ne_zero_of_dvd_ne_zero hn hd
   grind [abundant_iff_two_lt_abundancyIndex]
 
 theorem Abundant.mul_left (h : Abundant n) (hm : m ≠ 0) : Abundant (m * n) := by

Mathlib/Order/Interval/Finset/Gaps.lean

@@ -138,7 +138,6 @@ theorem intervalGapsWithin_snd_le {a b : α} (hFab : ∀ ⦃z⦄, z ∈ F → a
   by_cases hj : j = k
   · simp [hj]
   · have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j) (by grind))
-    simp only [Nat.succ_eq_add_one] at this
     grind
 
 theorem intervalGapsWithin_fst_le_snd {a b : α} (hab : a ≤ b)

Mathlib/Topology/Sets/CompactOpenCovered.lean

@@ -117,8 +117,7 @@ lemma of_isCompact_of_forall_exists_isCompactOpenCovered [TopologicalSpace S] {U
     · simp [Opens.forall]
       aesop
     · simpa using ⟨⟨Us x hx, hUo _ _⟩, ⟨x, by simpa⟩, hUx _ _⟩
-  · simp [Opens.forall]
-    grind
+  · grind
 
 lemma image {i : ι} (V : Opens (X i)) (hV : IsCompact (X := X i) V) :
     IsCompactOpenCovered f (f i '' V) := by