Optimize LeanModularForms proof elaboration

LeanPool/LeanModularForms/ContourIntegral/CrossingLimit.lean

@@ -124,9 +124,9 @@ theorem pv_tendsto_of_crossing_limit_asymmetric
     have hδR := hδR_pos ε hε_pos hε_lt
     have hδL_bd := hδL_small ε hε_pos hε_lt
     have hδR_bd := hδR_small ε hε_pos hε_lt
-    have h_left_lt : a < t₀ - δ_left ε := by linarith
-    have h_right_lt : t₀ + δ_right ε < b := by linarith
-    have h_mid_lt : t₀ - δ_left ε < t₀ + δ_right ε := by linarith
+    have h_left_lt : a < t₀ - δ_left ε := by linarith only [hδL_bd]
+    have h_right_lt : t₀ + δ_right ε < b := by linarith only [hδR_bd]
+    have h_mid_lt : t₀ - δ_left ε < t₀ + δ_right ε := by linarith only [hδL, hδR]
     -- Abbreviate the cutoff integrand
     set F := fun t => if ‖γ t - s‖ > ε then (γ t - s)⁻¹ * deriv γ t else (0 : ℂ) with hF_def
     -- F = 0 on the middle segment [t₀ - δL, t₀ + δR]
@@ -155,7 +155,11 @@ theorem pv_tendsto_of_crossing_limit_asymmetric
         mem_ae_iff.mpr (by rw [compl_compl]; exact (Set.finite_singleton _).measure_zero volume)
       filter_upwards [h_ne] with t ht_ne ht_mem
       rw [uIoc_of_le (le_of_lt h_right_lt)] at ht_mem
-      simp_all
+      simp_all only [mem_Ioo, mem_Ico, and_imp, mem_Ioc, mem_Icc, tsub_le_iff_right, and_self,
+        gt_iff_lt,
+        ite_eq_right_iff, mul_eq_zero, inv_eq_zero, ite_eq_left_iff, not_lt, zero_eq_mul,
+          mem_compl_iff, mem_singleton_iff,
+        ↓reduceIte]
     -- Integrability of F on each piece
     have hF_int_left : IntervalIntegrable F volume a (t₀ - δ_left ε) :=
       (hint_left ε hε_pos hε_lt).congr_ae
@@ -189,7 +193,9 @@ theorem pv_tendsto_of_crossing_limit_asymmetric
         ∫ t in (t₀ + δ_right ε)..b, (γ t - s)⁻¹ * deriv γ t :=
       intervalIntegral.integral_congr_ae hF_right
     -- Assemble
-    simp_all
+    simp_all only [mem_Ioo, mem_Ico, and_imp, mem_Ioc, mem_Icc, tsub_le_iff_right, and_self,
+      gt_iff_lt,
+      ite_eq_right_iff, mul_eq_zero, inv_eq_zero, ite_eq_left_iff, not_lt, zero_eq_mul, add_zero]
   exact h_limit.congr' h_ev.symm
 
 end ContourIntegral

LeanPool/LeanModularForms/ContourIntegral/PVSplit.lean

@@ -61,18 +61,18 @@ theorem pv_split_at_crossing {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} {ε δ : 
   have hδ_lt_right : δ < b - t₀ := lt_of_lt_of_le hδ_small (min_le_right _ _)
   have ha_lt_t₀ : a < t₀ := ht₀.1
   have ht₀_lt_b : t₀ < b := ht₀.2
-  have h_left_lt : a < t₀ - δ := by linarith
-  have h_mid_lt : t₀ - δ < t₀ + δ := by linarith
-  have h_right_lt : t₀ + δ < b := by linarith
+  have h_left_lt : a < t₀ - δ := by linarith only [hδ_lt_left]
+  have h_mid_lt : t₀ - δ < t₀ + δ := by linarith only [hδ]
+  have h_right_lt : t₀ + δ < b := by linarith only [hδ_lt_right]
   -- F = 0 on the middle segment [t₀ - δ, t₀ + δ]
   have hF_mid : ∀ t ∈ uIoc (t₀ - δ) (t₀ + δ), F t = 0 := by
     intro t ht
-    rw [uIoc_of_le (by linarith)] at ht
+    rw [uIoc_of_le (by linarith only [hδ])] at ht
     simp only [hF_def]
     rw [ite_eq_right (not_lt.mpr _)]
     apply h_near
     rw [abs_le]
-    constructor <;> [linarith [ht.1]; linarith [ht.2]]
+    constructor <;> [linarith only [ht, ht.1]; linarith only [ht, ht.2]]
   -- F = (γ t - s)⁻¹ * deriv γ t a.e. on [a, t₀ - δ]
   -- (The single boundary point t = t₀ - δ is measure zero; for all other t in Ioc a (t₀-δ)
   --  we have |t - t₀| > δ strictly, so h_far applies.)
@@ -85,10 +85,10 @@ theorem pv_split_at_crossing {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} {ε δ : 
     simp only [hF_def]
     rw [ite_eq_left]
     -- ht : t ∈ Ioc a (t₀ - δ), t ≠ t₀ - δ, so t < t₀ - δ, giving |t - t₀| > δ
-    apply h_far t ⟨le_of_lt ht.1, le_trans ht.2 (by linarith)⟩
-    rw [abs_of_nonpos (by linarith [ht.2])]
+    apply h_far t ⟨le_of_lt ht.1, le_trans ht.2 (by linarith only [hδ, hδ_lt_right])⟩
+    rw [abs_of_nonpos (by linarith only [hδ, ht, ht.2])]
     have : t < t₀ - δ := lt_of_le_of_ne ht.2 (fun h => ht_ne (Set.mem_singleton_iff.mpr h))
-    linarith
+    linarith only [this]
   -- F = (γ t - s)⁻¹ * deriv γ t a.e. on [t₀ + δ, b]
   have hF_right : ∀ᵐ t ∂volume, t ∈ uIoc (t₀ + δ) b →
       F t = (γ t - s)⁻¹ * deriv γ t := by
@@ -99,9 +99,9 @@ theorem pv_split_at_crossing {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} {ε δ : 
     simp only [hF_def]
     rw [ite_eq_left]
     -- ht : t ∈ Ioc (t₀ + δ) b, so t₀ + δ < t, giving |t - t₀| = t - t₀ > δ
-    apply h_far t ⟨le_trans (by linarith) (le_of_lt ht.1), ht.2⟩
-    rw [abs_of_nonneg (by linarith [ht.1])]
-    linarith [ht.1]
+    apply h_far t ⟨le_trans (by linarith only [hδ, hδ_lt_left]) (le_of_lt ht.1), ht.2⟩
+    rw [abs_of_nonneg (by linarith only [hδ, ht, ht.1])]
+    linarith only [ht, ht.1]
   -- Integrability of F on each piece
   have hF_int_left : IntervalIntegrable F volume a (t₀ - δ) :=
     hint_left.congr_ae ((ae_restrict_iff' measurableSet_uIoc).mpr
@@ -131,6 +131,8 @@ theorem pv_split_at_crossing {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} {ε δ : 
       ∫ t in (t₀ + δ)..b, (γ t - s)⁻¹ * deriv γ t :=
     integral_congr_ae hF_right
   -- Assemble
-  simp_all
+  simp_all only [mem_Ioo, and_self, lt_min_iff, mem_Icc, and_imp, gt_iff_lt, ite_eq_right_iff,
+    mul_eq_zero,
+    inv_eq_zero, ite_eq_left_iff, not_lt, zero_eq_mul, add_zero]
 
 end ContourIntegral

LeanPool/LeanModularForms/ContourIntegral/SegmentFTC.lean

@@ -58,7 +58,7 @@ theorem ftc_telescope_closed_split {f : ℝ → ℂ} {a b t₀ δ : ℝ}
       Complex.log (f b) - Complex.log (f (t₀ + δ))) :
     (∫ t in a..(t₀ - δ), deriv f t / f t) + (∫ t in (t₀ + δ)..b, deriv f t / f t) =
     Complex.log (f (t₀ - δ)) - Complex.log (f (t₀ + δ)) := by
-  simp_all
+  simp_all only [sub_add_sub_cancel]
 
 /-- FTC on three consecutive segments telescopes: the integral over [a,d] is
 log(f d) - log(f a) if each sub-interval satisfies the FTC-for-log. -/

LeanPool/LeanModularForms/ForMathlib/Bounds.lean

@@ -8,10 +8,6 @@ module
 public import Mathlib.NumberTheory.ModularForms.Bounds
 public import LeanPool.LeanModularForms.ForMathlib.Petersson
 
-import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
-import Mathlib.Combinatorics.Matroid.Init
-import Mathlib.MeasureTheory.Integral.Bochner.Basic
-import Mathlib.Tactic.Positivity.Finset
 
 /-!
 # Bounds for modular forms

LeanPool/LeanModularForms/ForMathlib/IsBoundedAtImInfty.lean

@@ -7,12 +7,6 @@ module
 
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
 
-import Mathlib.Algebra.Order.Algebra
-import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
-import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-import Mathlib.Data.Sym.Sym2.Init
-import Mathlib.Tactic.NormNum.GCD
-import Mathlib.Tactic.Positivity.Finset
 
 /-!
 # Boundedness of Eisenstein series

LeanPool/LeanModularForms/ForMathlib/LevelOne.lean

@@ -12,10 +12,6 @@ public import LeanPool.LeanModularForms.ForMathlib.CongruenceSubgrps
 public import LeanPool.LeanModularForms.ForMathlib.Identities
 public import Mathlib.NumberTheory.ModularForms.LevelOne.Basic
 
-import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
-import Mathlib.Combinatorics.Matroid.Init
-import Mathlib.MeasureTheory.Integral.Bochner.Basic
-import Mathlib.Tactic.Positivity.Finset
 /-!
 # Level one modular forms
 

LeanPool/LeanModularForms/GeneralizedResidueTheory/ArcCalculus.lean

@@ -55,12 +55,21 @@ theorem unitArc_at_end (θ₁ θ₂ a b : ℝ) (hab : a ≠ b) :
     unitArc θ₁ θ₂ a b b = exp (↑θ₂ * I) := by
   simp only [unitArc]
   have hba : b - a ≠ 0 := sub_ne_zero.mpr (Ne.symm hab)
-  simp_all
+  simp_all only [ne_eq, not_false_eq_true, div_self, one_mul, add_sub_cancel]
 
 /-- The unit arc is continuous. -/
 theorem unitArc_continuous (θ₁ θ₂ a b : ℝ) : Continuous (unitArc θ₁ θ₂ a b) := by
   unfold unitArc
-  fun_prop
+  exact Continuous.cexp
+      (Continuous.mul_const
+        (Continuous.comp' continuous_ofReal
+          (Continuous.const_add
+            (Continuous.mul_const
+              (Continuous.comp' (Continuous.div_const continuous_id' (b - a))
+                (Continuous.fun_sub continuous_id' continuous_const))
+              (θ₂ - θ₁))
+            θ₁))
+        I)
 
 /-- Helper: the angle function for the unit arc has a specific derivative. -/
 private lemma unitArc_angle_hasDerivAt (θ₁ θ₂ a b t : ℝ) (_hab : b - a ≠ 0) :
@@ -107,8 +116,8 @@ theorem exp_sub_norm_sq (θ₁ θ₂ : ℝ) :
   have hc1 := Real.sin_sq_add_cos_sq θ₁
   have hc2 := Real.sin_sq_add_cos_sq θ₂
   rw [Real.cos_sub]
-  nlinarith [sq_nonneg (Real.cos θ₁ - Real.cos θ₂),
-             sq_nonneg (Real.sin θ₁ - Real.sin θ₂)]
+  nlinarith only [hc1, hc2, sq_nonneg (Real.cos θ₁ - Real.cos θ₂),
+    sq_nonneg (Real.sin θ₁ - Real.sin θ₂)]
 
 /-- sin is positive on the open interval (0, π). -/
 theorem sin_pos_of_mem_Ioo_zero_pi {θ : ℝ} (hθ : θ ∈ Ioo 0 π) : 0 < Real.sin θ :=
@@ -122,12 +131,12 @@ theorem abs_cos_le_half_of_mem_Icc {θ : ℝ} (hθ : θ ∈ Icc (π / 3) (2 * π
   have h2 : θ ≤ 2 * π / 3 := hθ.2
   rw [abs_le]; constructor
   · have : Real.cos (2 * π / 3) ≤ Real.cos θ :=
-      Real.cos_le_cos_of_nonneg_of_le_pi (by linarith) (by linarith) h2
+      Real.cos_le_cos_of_nonneg_of_le_pi (by linarith only [hpi, h1]) (by linarith only [hpi]) h2
     rw [show (2 * π / 3 : ℝ) = π - π / 3 from by ring,
       Real.cos_pi_sub, Real.cos_pi_div_three] at this
-    linarith
+    linarith only [this]
   · have : Real.cos θ ≤ Real.cos (π / 3) :=
-      Real.cos_le_cos_of_nonneg_of_le_pi (by linarith) (by linarith) h1
-    simp_all
+      Real.cos_le_cos_of_nonneg_of_le_pi (by linarith only [hpi]) (by linarith only [hpi, h2]) h1
+    simp_all only [mem_Icc, and_self, cos_pi_div_three, one_div]
 
 end ArcCalculus

LeanPool/LeanModularForms/GeneralizedResidueTheory/Basic.lean

@@ -161,7 +161,7 @@ private theorem exists_min_above_in_finite_union
       ((Set.Finite.mem_toFinset hS_above_finite).mpr hs)
   exact ⟨s_min, hs_min_in.2,
     hs_min_le b ⟨Set.mem_union_left _ rfl, ht_lt_b⟩,
-    fun x hx hxS => by linarith [hs_min_le x ⟨hxS, hx.1⟩, hx.2]⟩
+    fun x hx hxS => by linarith only [hs_min_le, hx, hxS, hs_min_le x ⟨hxS, hx.1⟩, hx.2]⟩
 
 private theorem eq_on_Ioo_of_deriv_zero
     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
@@ -176,7 +176,7 @@ private theorem eq_on_Ioo_of_deriv_zero
       f x = f y :=
     fun x hx y hy => IsOpen.is_const_of_deriv_eq_zero
       isOpen_Ioo isPreconnected_Ioo h_diff h_dz hx hy
-  have h_mid : (t + s_min) / 2 ∈ Ioo t s_min := by constructor <;> linarith
+  have h_mid : (t + s_min) / 2 ∈ Ioo t s_min := by constructor <;> linarith only [ht_lt_s]
   have h_eq_mid : ∀ x ∈ Ioo t s_min, f x = f ((t + s_min) / 2) :=
     fun x hx => h_const x hx _ h_mid
   have h_cont_Ioo : ContinuousWithinAt f (Ioo t s_min) t :=

LeanPool/LeanModularForms/GeneralizedResidueTheory/CauchyPrimitive.lean

@@ -8,7 +8,6 @@ module
 public import Mathlib.Analysis.Calculus.Deriv.Basic
 public import Mathlib.Analysis.Complex.Basic
 public import Mathlib.Topology.Algebra.Module.ModuleTopology
-import Mathlib.Analysis.Calculus.ParametricIntervalIntegral
 import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
 
@@ -47,7 +46,7 @@ private lemma segment_subset_convex {S : Set ℂ} (hS : Convex ℝ S)
     {c z : ℂ} (hc : c ∈ S) (hz : z ∈ S) :
     ∀ t ∈ Icc (0 : ℝ) 1, c + t • (z - c) ∈ S := fun t ht => by
   rw [show c + t • (z - c) = (1 - t) • c + t • z from by module]
-  exact hS hc hz (by linarith [ht.2]) ht.1 (by linarith [ht.1])
+  exact hS hc hz (by linarith only [ht, ht.2]) ht.1 (by linarith only [ht.1])
 
 private lemma integral_t_mul_deriv_eq {f : ℂ → ℂ} {S : Set ℂ}
     {c z : ℂ} (hS_open : IsOpen S)
@@ -109,7 +108,10 @@ private lemma integral_t_mul_deriv_eq {f : ℂ → ℂ} {S : Set ℂ}
     intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt
       hu_cont hv_cont hu_deriv hv_deriv hu'_int hv'_int
   simp only [u, v, u', v'] at h_parts
-  simp_all
+  simp_all only [mem_Icc, real_smul, and_imp, zero_le_one, uIcc_of_le, inf_of_le_left,
+    sup_of_le_right, mem_Ioo,
+      ofReal_one, one_smul, add_sub_cancel, one_mul, ofReal_zero, zero_smul, add_zero, zero_mul,
+        sub_zero]
 
 private lemma continuous_segmentMap (c w : ℂ) :
     Continuous (fun t : ℝ => c + t • (w - c)) :=
@@ -236,7 +238,10 @@ private lemma segmentIntegrand_lipschitzOnWith {f : ℂ → ℂ}
     _ = |t| * M * ‖x - y‖ := by ring
     _ = |t| * M * dist x y := by rw [dist_eq_norm]
     _ ≤ Real.toNNReal (|t| * M) * dist x y := by
-        simp_all
+        simp_all only [mem_Icc, Metric.mem_ball, real_smul, add_sub_add_left_eq_sub,
+          Complex.norm_mul, norm_real,
+            Real.norm_eq_abs, Real.coe_toNNReal', mul_nonneg_iff_of_pos_right, abs_nonneg,
+              sup_of_le_left, Std.le_refl]
 
 private lemma hasDerivAt_segmentIntegral_aux {f : ℂ → ℂ}
     {S : Set ℂ} {c z : ℂ} {ε : ℝ}
@@ -381,7 +386,8 @@ private lemma hasDerivAt_segmentIntegral {f : ℂ → ℂ}
   suffices hH : HasDerivAt H (H' z) z by
     have h_prod := hH.mul h1
     refine h_prod.congr_deriv ?_
-    simp_all
+    simp_all only [mem_Icc, real_smul, and_imp, gt_iff_lt, intervalIntegral.integral_mul_const,
+        mul_eq_mul_right_iff, hasDerivAt_sub_const_iff, mul_one, sub_add_cancel]
   exact hasDerivAt_segmentIntegral_aux hε_pos hS_convex
     hS_open hc hz hf hε_ball
 

LeanPool/LeanModularForms/GeneralizedResidueTheory/GeneralizedResidueTheorem.lean

@@ -161,7 +161,7 @@ theorem generalizedResidueTheorem (U : Set ℂ) (hU : IsOpen U)
       generalizedWindingNumber' γ.toFun γ.a γ.b s * residueAt f s := by
     have hL_eq : L = cauchyPrincipalValueOn S0 f_res γ.toFun γ.a γ.b :=
       (hL.limUnder_eq).symm
-    simp_all
+    simp_all only [gt_iff_lt, ne_eq, Set.mem_Icc, and_imp, implies_true]
   rw [← h_limit_eq]
   have hPV_res_tendsto : Tendsto (fun ε => ∫ t in γ.a..γ.b,
       cauchyPrincipalValueIntegrandOn S0
@@ -270,7 +270,7 @@ theorem generalizedResidueTheorem_simplePoles (U : Set ℂ) (hU : IsOpen U)
       2 * Real.pi * I * ∑ s ∈ S0,
         generalizedWindingNumber' γ.toFun γ.a γ.b s *
           residueSimplePole f s := by
-    simp_all
+    simp_all only [gt_iff_lt, ne_eq, Set.mem_Icc, and_imp, implies_true]
   have hCancel : Tendsto
       (fun ε =>
         (∫ t in γ.a..γ.b, cauchyPrincipalValueIntegrandOn S0 f γ.toFun ε t) -