chore: weekly lints for 2026-02-16 (leanprover-community#35490)

chenson2018 · chenson2018 · commit 0c5ce9932040 · 2026-02-21T23:47:15.000Z
Changes suggested by the `mergeWithGrind` linter, from the weekly job posted at [#mathlib4 > Weekly linting log @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Weekly.20linting.20log/near/574041907). As suggested by @Vierkantor, I have used the `linter.tacticAnalysis.mergeWithGrind` option to turn off the linter in two theorems: one where there was a comment about not making this change for performance reasons and another that appears to be a bug with the linter. Now that there is a precedent for using the `grind` interactive mode in Mathlib, I have used this in one proof where it results in fewer calls to `grind` and a clearer proof.
diff --git a/Mathlib/Algebra/BigOperators/Associated.lean b/Mathlib/Algebra/BigOperators/Associated.lean
@@ -57,6 +57,8 @@ theorem Prod.associated_iff {M N : Type*} [Monoid M] [Monoid N] {x z : M × N} :
   fun ⟨⟨u₁, h₁⟩, ⟨u₂, h₂⟩⟩ =>
     ⟨MulEquiv.prodUnits.invFun (u₁, u₂), Prod.eq_iff_fst_eq_snd_eq.2 ⟨h₁, h₂⟩⟩⟩
 
+-- TODO: this seems to trigger a bug in the mergeWithGrind linter
+set_option linter.tacticAnalysis.mergeWithGrind false in
 theorem Associated.prod {M : Type*} [CommMonoid M] {ι : Type*} (s : Finset ι) (f : ι → M)
     (g : ι → M) (h : ∀ i, i ∈ s → (f i) ~ᵤ (g i)) : (∏ i ∈ s, f i) ~ᵤ (∏ i ∈ s, g i) := by
   induction s using Finset.induction with
diff --git a/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean b/Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@@ -798,7 +798,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; grind
+  have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by grind
   rw [← prod_filter_ne_one, ← this, prod_biUnion]
   swap
   · intro i hi j hj hij a hai haj k hk
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NthRootLemmas.lean
@@ -66,9 +66,6 @@ private theorem nthRoot.lt_pow_go_succ_aux0 (hb : b ≠ 0) :
     Nat.le_div_iff_mul_le (by positivity)]
   have := (Commute.all (b : ℤ) (a - b)).pow_add_mul_le_add_pow_of_sq_nonneg
     (by positivity) (sq_nonneg _) (sq_nonneg _) (by grind) (n + 1)
-  -- `grind` should solve this, but:  https://github.com/leanprover/lean4/issues/11539
-  simp [mul_sub, ← add_sub_assoc] at this
-  norm_cast at this
   grind
 
 private theorem nthRoot.always_exists (n a : ℕ) :
diff --git a/Mathlib/Data/DFinsupp/Defs.lean b/Mathlib/Data/DFinsupp/Defs.lean
@@ -945,7 +945,6 @@ theorem support_zipWith {f : ∀ i, β₁ i → β₂ i → β i} {hf : ∀ i, f
 end MapRangeAndZipWith
 
 theorem erase_def (i : ι) (f : Π₀ i, β i) : f.erase i = mk (f.support.erase i) fun j => f j.1 := by
-  ext
   grind
 
 @[simp]
diff --git a/Mathlib/Data/Setoid/Partition.lean b/Mathlib/Data/Setoid/Partition.lean
@@ -505,14 +505,15 @@ some of the sets to obtain a coarser partition. -/
 noncomputable def coarserPartition (hs : IndexedPartition s) {κ : Type*} (g : ι → κ)
     (hg : g.Surjective) :
     IndexedPartition (fun k : κ => ⋃ i ∈ g ⁻¹' {k}, s i) where
-  eq_of_mem {_x _i _j} hxi hxj := by
+  eq_of_mem {x _i _j} hxi hxj := by
     obtain ⟨a, ⟨c, hc⟩, ha⟩ := hxi
     obtain ⟨b, ⟨d, hd⟩, hb⟩ := hxj
-    simp only [← hc, mem_iUnion] at ha
-    simp only [← hd, mem_iUnion] at hb
-    have : c = d := hs.eq_of_mem ha.2 hb.2
-    by_contra!
-    grind [disjoint_iff_forall_ne.mp ((disjoint_singleton.mpr this).preimage g) ha.1 hb.1]
+    grind =>
+      instantiate [mem_iUnion]
+      have hb : x ∈ s d
+      have ha : x ∈ s c
+      have : c = d := hs.eq_of_mem ha hb
+      finish
   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 ?_
diff --git a/Mathlib/Geometry/Euclidean/Angle/Bisector.lean b/Mathlib/Geometry/Euclidean/Angle/Bisector.lean
@@ -296,9 +296,7 @@ lemma two_zsmul_oangle_eq_of_dist_orthogonalProjection_line_eq {p p₁ p₂ p₃
       convert (ha.inf_affineSpan_eq_affineSpan_inter {0, 1} {0, 2})
       · simp [Set.image_insert_eq]
       · simp [Set.image_insert_eq]
-      · suffices {p₁} = ![p₁, p₂, p₃] '' {0} by
-          convert this
-          grind
+      · suffices {p₁} = ![p₁, p₂, p₃] '' {0} by grind
         simp
     have hsup : line[ℝ, p₁, p₂] ⊔ line[ℝ, p₁, p₃] = ⊤ := by
       rw [← AffineSubspace.span_union]
diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/AbsolutelyContinuousFun.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/AbsolutelyContinuousFun.lean
@@ -97,7 +97,6 @@ lemma exists_dist_slope_lt_pairwiseDisjoint_hasSum {f f' : ℝ → F} {d b η :
   apply_fun fun x ↦ x.toReal at vol_sum
   rw [ENNReal.tsum_toReal_eq (by simp), ENNReal.toReal_ofReal (by linarith),
       ← Summable.hasSum_iff (by grind [tsum_def])] at vol_sum
-  convert vol_sum with z
   grind [ENNReal.toReal_ofReal]
 
 /-- If `f` is absolutely continuous on `[d, b]` and there is a collection of pairwise disjoint
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean b/Mathlib/MeasureTheory/MeasurableSpace/Pi.lean
@@ -61,6 +61,8 @@ theorem IsCountablySpanning.pi {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCoun
     (surjective_decode_getD (ι → ℕ) default).iUnion_comp fun x => Set.pi univ fun i => s i (x i),
     iUnion_univ_pi s, h2s, pi_univ]
 
+-- `grind` can close the goal from the point marked by the comment below, but is slow
+set_option linter.tacticAnalysis.mergeWithGrind false in
 /-- The product of generated σ-algebras is the one generated by boxes, if both generating sets
   are countably spanning. -/
 theorem generateFrom_pi_eq {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsCountablySpanning (C i)) :
diff --git a/Mathlib/MeasureTheory/SetSemiring.lean b/Mathlib/MeasureTheory/SetSemiring.lean
@@ -546,7 +546,7 @@ protected lemma Ioc [LinearOrder α] [Nonempty α] :
       rcases Ioc_mem_setOf_Ioc_le u (min u' v) with ⟨u'', v'', h'', heq⟩
       rw [this, heq]
       exact ⟨{Set.Ioc u'' v''}, by grind, by simp, by simp⟩
-    rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by ext; simp; grind]
+    rw [show Set.Ioc u v \ Set.Ioc u' v' = Set.Ioc u u' ∪ Set.Ioc v' v by grind]
     refine ⟨{Set.Ioc u u', Set.Ioc v' v}, by grind, ?_, by simp⟩
     intro a ha b hb hab
     simp [Function.onFun]
diff --git a/Mathlib/RingTheory/Polynomial/Morse.lean b/Mathlib/RingTheory/Polynomial/Morse.lean
@@ -74,8 +74,7 @@ theorem Splits.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia
       (by simp [hπ]) (by simp [hπ]) (by simpa [← rootSet.coe_smul]) (by simpa [← rootSet.coe_smul])
     grind [rootSet.coe_smul]
   · simp [hz']
-  · have key := hp (g • z) (g • z).2 z z.2 (g • x) (g • x).2 x x.2 (by simp [hπ]) (by simp [hπ])
-    grind [rootSet.coe_smul, SetLike.coe_eq_coe]
+  · grind [rootSet.coe_smul, SetLike.coe_eq_coe]
 
 /-- If the roots of `f` in `S` have at most one collision modulo each maximal ideal `m`, and if a
 group `G` acting transitively on the roots in `S` is generated by inertia subgroups, then `G`
diff --git a/Mathlib/RingTheory/Unramified/LocalRing.lean b/Mathlib/RingTheory/Unramified/LocalRing.lean
@@ -175,7 +175,6 @@ lemma localRingHom_injective_of_primesOver_eq_singleton
   obtain ⟨r, hrp, t, e'⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ haq
   refine (IsLocalization.mk'_eq_zero_iff _ _).mpr
     ⟨⟨r, hrp⟩, FaithfulSMul.algebraMap_injective R S ?_⟩
-  simp only [map_mul, e', map_zero]
   grind
 
 lemma finite_of_primesOver_eq_singleton [Module.Finite R S] [q.LiesOver p] :
diff --git a/MathlibTest/TacticAnalysis.lean b/MathlibTest/TacticAnalysis.lean
@@ -1,6 +1,7 @@
 import Mathlib.Tactic.TacticAnalysis.Declarations
 import Mathlib.Tactic.AdaptationNote
 import Lean.LibrarySuggestions
+import Mathlib.Algebra.BigOperators.Associated
 
 section terminalReplacement
 
@@ -26,7 +27,7 @@ warning: `simp only` failed where `simp` succeeded.
 Original tactic:
   simp
 Counterexample:
-  import Init.Data.List.Basic
+  import Mathlib.Algebra.GroupWithZero.Nat
 -/
 -- The counterexample name contains a number that varies between runs, so we can't fully test this.
 #guard_msgs (substring := true) in
@@ -59,13 +60,13 @@ example : x = z := by
 
 -- Definitions using `where` clauses did not get picked up by the framework,
 -- since apparently their syntax bounds do not match the original.
-structure Fact (p : Prop) : Prop where
+structure Fact' (p : Prop) : Prop where
   out : p
 /--
 warning: Try this: rw [xy, yz]
 -/
 #guard_msgs in
-example : Fact (x = z) where
+example : Fact' (x = z) where
   out := by
     rw [xy]
     rw [yz]
@@ -153,6 +154,20 @@ example : 0 = 0 := by
 
 set_option linter.unusedTactic true
 
+-- This is a false positive. Before `convert_to`, there is an mvar for the `DecidableEq` instance
+-- used with `Finset.instInsert` that is not properly handled
+
+/-- warning: 'convert_to Associated (∏ i ∈ insert j s, f i) (∏ i ∈ insert j s, g i); grind' can be replaced with 'grind' -/
+#guard_msgs in
+theorem Associated.prod' {M : Type*} [CommMonoid M] {ι : Type*} (s : Finset ι) (f : ι → M)
+    (g : ι → M) (h : ∀ i, i ∈ s → Associated (f i) (g i)) : Associated (∏ i ∈ s, f i) (∏ i ∈ s, g i) := by
+  induction s using Finset.induction with
+  | empty => grind [Associated.prod]
+  | insert j s hjs IH =>
+    classical
+    convert_to Associated (∏ i ∈ insert j s, f i) (∏ i ∈ insert j s, g i)
+    grind [Associated.mul_mul]
+
 end mergeWithGrind
 
 section replaceWithGrind
@@ -191,7 +206,7 @@ example {α : Type u} (f : α → Type max u v) : 1 = 1 := by
 -- Ensure the effects of `classical` are picked up. Otherwise we get an error like:
 -- failed to synthesize
 --   Decidable b
-theorem forall_imp_iff_exists_imp {α : Type} {p : α → Prop} {b : Prop} [ha : Nonempty α] :
+theorem forall_imp_iff_exists_imp' {α : Type} {p : α → Prop} {b : Prop} [ha : Nonempty α] :
     (∀ x, p x) → b ↔ ∃ x, p x → b := by
   classical
   let ⟨a⟩ := ha
