chore: replace long terminal simp only […]:s (≥4 lemmas) with bare simp:s (leanprover-community#36639)

euprunin · euprunin · commit be0a10d1f1d5 · 2026-03-14T14:51:28.000Z
The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective.

Trace profiling results (differences &lt;30 ms considered measurement noise):
* `Polynomial.degree_sum_le`: unchanged 🎉
* `AlgebraicGeometry.Scheme.PartialMap.ext_iff`: unchanged 🎉
* `MeromorphicAt.inv`: 515 ms before, 469 ms after  🎉
* `IsLowerSet.le_card_inter_finset'`: unchanged 🎉
* `SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle`: unchanged 🎉
* `List.Vector.scanl_get`: unchanged 🎉
* `isSeparable_algebraMap`: unchanged 🎉
* `ArithmeticFunction.vonMangoldt.not_summable_residueClass_prime_div`: 643 ms before, 597 ms after  🎉
* `CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup`: 163 ms before, 120 ms after  🎉
* `ProbabilityTheory.meas_ge_le_variance_div_sq`: unchanged 🎉
* `MvPowerSeries.mem_nonZeroDivisorsRight_of_constantCoeff`: 936 ms before, 485 ms after  🎉
* `Polynomial.mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero`: unchanged 🎉
* `ENNReal.limsup_sub_const`: 185 ms before, 95 ms after  🎉

Profiled using `set_option trace.profiler true in`.

This PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR
diff --git a/Mathlib/Algebra/Polynomial/Degree/Defs.lean b/Mathlib/Algebra/Polynomial/Degree/Defs.lean
@@ -388,7 +388,7 @@ theorem degree_update_le (p : R[X]) (n : ℕ) (a : R) : degree (p.update n a) 
 
 theorem degree_sum_le (s : Finset ι) (f : ι → R[X]) :
     degree (∑ i ∈ s, f i) ≤ s.sup fun b => degree (f b) :=
-  Finset.cons_induction_on s (by simp only [sum_empty, sup_empty, degree_zero, le_refl])
+  Finset.cons_induction_on s (by simp)
     fun a s has ih =>
     calc
       degree (∑ i ∈ cons a s has, f i) ≤ max (degree (f a)) (degree (∑ i ∈ s, f i)) := by
diff --git a/Mathlib/AlgebraicGeometry/RationalMap.lean b/Mathlib/AlgebraicGeometry/RationalMap.lean
@@ -62,7 +62,7 @@ lemma ext_iff (f g : X.PartialMap Y) :
     f = g ↔ ∃ e : f.domain = g.domain, f.hom = (X.isoOfEq e).hom ≫ g.hom := by
   constructor
   · rintro rfl
-    simp only [exists_true_left, Scheme.isoOfEq_rfl, Iso.refl_hom, Category.id_comp]
+    simp
   · obtain ⟨U, hU, f⟩ := f
     obtain ⟨V, hV, g⟩ := g
     rintro ⟨rfl : U = V, e⟩
diff --git a/Mathlib/Analysis/Meromorphic/Basic.lean b/Mathlib/Analysis/Meromorphic/Basic.lean
@@ -244,7 +244,7 @@ lemma inv {f : 𝕜 → 𝕜'} (hf : MeromorphicAt f x) : MeromorphicAt f⁻¹ x
     refine ⟨n + 1, (this.fun_smul <| hg_an.inv hg_ne).congr ?_⟩
     filter_upwards [hg_eq, hg_an.continuousAt.eventually_ne hg_ne] with z hfg hg_ne'
     rcases eq_or_ne z x with rfl | hz_ne
-    · simp only [sub_self, pow_succ, mul_zero, zero_smul]
+    · simp
     · replace hfg := congr_arg (·⁻¹) hfg
       simp only [smul_inv₀] at hfg
       rw [inv_smul_eq_iff₀ (pow_ne_zero m (sub_ne_zero.mpr hz_ne)), smul_comm,
diff --git a/Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean b/Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean
@@ -61,7 +61,7 @@ theorem IsLowerSet.le_card_inter_finset' (h𝒜 : IsLowerSet (𝒜 : Set (Finset
     obtain rfl | rfl := h𝒜s
     · simp only [card_empty, zero_mul, empty_inter, mul_zero, le_refl]
     obtain rfl | rfl := hℬs
-    · simp only [card_empty, inter_empty, mul_zero, le_refl]
+    · simp
     · simp only [card_empty, pow_zero, inter_singleton_of_mem, mem_singleton, card_singleton,
         le_refl]
   | insert a s hs ih =>
diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
@@ -795,7 +795,7 @@ theorem adj_and_reachable_delete_edges_iff_exists_cycle {v w : V} :
       rw [Sym2.eq_swap]
       intro h
       cases hp (Walk.edges_toPath_subset p h)
-    · simp only [Sym2.eq_swap, Walk.edges_cons, List.mem_cons, true_or]
+    · simp
   · rintro ⟨u, c, hc, he⟩
     refine ⟨c.adj_of_mem_edges he, ?_⟩
     by_contra! hb
diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean
@@ -375,7 +375,7 @@ theorem scanl_get (i : Fin n) :
   | succ n hn =>
     rw [← cons_head_tail v, scanl_cons, get_cons_succ]
     refine Fin.cases ?_ ?_ i
-    · simp only [get_zero, scanl_head, Fin.castSucc_zero, head_cons]
+    · simp
     · intro i'
       simp only [hn, Fin.castSucc_succ, get_cons_succ]
 
diff --git a/Mathlib/FieldTheory/Separable.lean b/Mathlib/FieldTheory/Separable.lean
@@ -656,7 +656,7 @@ variable [Ring K] [Algebra F K]
 variable {F} in
 theorem isSeparable_algebraMap (x : F) : IsSeparable F (algebraMap F K x) :=
   Polynomial.Separable.of_dvd (Polynomial.separable_X_sub_C (x := x))
-    (minpoly.dvd F (algebraMap F K x) (by simp only [map_sub, aeval_X, aeval_C, sub_self]))
+    (minpoly.dvd F (algebraMap F K x) (by simp))
 
 instance Algebra.isSeparable_self : Algebra.IsSeparable F F :=
   ⟨isSeparable_algebraMap⟩
diff --git a/Mathlib/NumberTheory/LSeries/PrimesInAP.lean b/Mathlib/NumberTheory/LSeries/PrimesInAP.lean
@@ -430,7 +430,7 @@ lemma not_summable_residueClass_prime_div (ha : IsUnit a) :
   have H₁ {x : ℝ} (hx : 1 < x) : ∑' n, residueClass a n / (n : ℝ) ^ x ≤ C := by
     refine Summable.tsum_le_tsum (fun n ↦ ?_) ?_ key
     · rcases n.eq_zero_or_pos with rfl | hn
-      · simp only [Nat.cast_zero, Real.zero_rpow (zero_lt_one.trans hx).ne', div_zero, le_refl]
+      · simp
       · refine div_le_div_of_nonneg_left (residueClass_nonneg a _) (mod_cast hn) ?_
         conv_lhs => rw [← Real.rpow_one n]
         exact Real.rpow_le_rpow_of_exponent_le (by norm_cast) hx.le
diff --git a/Mathlib/Order/CompactlyGenerated/Basic.lean b/Mathlib/Order/CompactlyGenerated/Basic.lean
@@ -125,8 +125,7 @@ theorem isCompactElement_iff_exists_le_sSup_of_le_sSup (k : α) :
       have Sne : S.Nonempty := by
         suffices ⊥ ∈ S from Set.nonempty_of_mem this
         use ∅
-        simp only [Set.empty_subset, Finset.coe_empty, Finset.sup_empty,
-          and_self_iff]
+        simp
       -- Now apply the defn of compact and finish.
       obtain ⟨j, ⟨hjS, hjk⟩⟩ := hk S Sne dir_US (le_trans hsup sup_S)
       obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
diff --git a/Mathlib/Probability/Moments/Variance.lean b/Mathlib/Probability/Moments/Variance.lean
@@ -379,7 +379,7 @@ theorem meas_ge_le_variance_div_sq [IsFiniteMeasure μ] {X : Ω → ℝ} (hX : M
     (hc : 0 < c) : μ {ω | c ≤ |X ω - μ[X]|} ≤ ENNReal.ofReal (variance X μ / c ^ 2) := by
   rw [ENNReal.ofReal_div_of_pos (sq_pos_of_ne_zero hc.ne.symm), hX.ofReal_variance_eq]
   convert @meas_ge_le_evariance_div_sq _ _ _ _ hX.1 c.toNNReal (by simp [hc]) using 1
-  · simp only [Real.coe_toNNReal', max_le_iff, abs_nonneg, and_true]
+  · simp
   · rw [ENNReal.ofReal_pow hc.le]
     rfl
 
diff --git a/Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean b/Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean
@@ -69,8 +69,7 @@ theorem mem_nonZeroDivisorsRight_of_constantCoeff {φ : MvPowerSeries σ R}
     · simp only [← mem_antidiagonal.mp huv, le_add_iff_nonneg_right, zero_le]
     · rintro rfl
       simp_all
-  · simp only [mem_antidiagonal, add_zero, not_true_eq_false, coeff_zero_eq_constantCoeff,
-      false_implies]
+  · simp
 
 -- TODO: derive from `mem_nonZeroDivisorsRight_of_constantCoeff` using `MulOpposite`
 theorem mem_nonZeroDivisorsLeft_of_constantCoeff {φ : MvPowerSeries σ R}
diff --git a/Mathlib/RingTheory/Polynomial/Ideal.lean b/Mathlib/RingTheory/Polynomial/Ideal.lean
@@ -32,7 +32,7 @@ theorem mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero {b : R[X]} {P : R[X][X]
   rw [Ideal.mem_span_pair]
   constructor <;> intro h
   · rcases h with ⟨_, _, rfl⟩
-    simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul, add_zero, mul_zero, sub_self]
+    simp
   · rcases dvd_iff_isRoot.mpr h with ⟨p, hp⟩
     rcases @X_sub_C_dvd_sub_C_eval _ b _ P with ⟨q, hq⟩
     exact ⟨C p, q, by rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]⟩
diff --git a/Mathlib/Topology/Instances/ENNReal/Lemmas.lean b/Mathlib/Topology/Instances/ENNReal/Lemmas.lean
@@ -787,7 +787,7 @@ variable {ι : Type*} {f : Filter ι} {u v : ι → ℝ≥0∞}
 lemma limsup_sub_const (F : Filter ι) (f : ι → ℝ≥0∞) (c : ℝ≥0∞) :
     Filter.limsup (fun i ↦ f i - c) F = Filter.limsup f F - c := by
   rcases F.eq_or_neBot with rfl | _
-  · simp only [limsup_bot, bot_eq_zero', zero_le, tsub_eq_zero_of_le]
+  · simp
   · exact (Monotone.map_limsSup_of_continuousAt (F := F.map f) (f := fun (x : ℝ≥0∞) ↦ x - c)
     (fun _ _ h ↦ tsub_le_tsub_right h c) (continuous_sub_right c).continuousAt).symm
 
