Optimize LeanModularForms proofs and elaboration

LeanPool/LeanModularForms/ForMathlib/QExpansion.lean

@@ -47,7 +47,7 @@ theorem periodic_comp_ofComplex' (hΓ : Γ.width ∣ h) : Periodic (f ∘ ofComp
     simp only [comp_apply, ofComplex_apply_of_im_pos this, ofComplex_apply_of_im_pos hw,
       ← vAdd_width_periodic f k (Nat.cast_dvd_cast hΓ) ⟨w, hw⟩]
     congr 1
-    simp [UpperHalfPlane.ext_iff, add_comm]
+    simp only [Int.cast_natCast, UpperHalfPlane.ext_iff, coe_vadd, ofReal_natCast, add_comm]
   · have : im (w + h) ≤ 0 := by simpa only [add_im, natCast_im, add_zero, not_lt] using hw
     simp only [comp_apply, ofComplex_apply_of_im_nonpos this,
       ofComplex_apply_of_im_nonpos (not_lt.mp hw)]

LeanPool/LeanModularForms/ForMathlib/SlashActions.lean

@@ -49,4 +49,8 @@ theorem ModularForm.slash_neg' {k : ℤ} (g : SL(2, ℤ)) (f : ℍ → ℂ) (hk
   rw [SL_slash, ← slash_neg _ _ hk]
   congr
   ext
-  simp
+  simp only [Matrix.SpecialLinearGroup.coe_int_neg, Units.val_neg,
+    Matrix.SpecialLinearGroup.coe_GL_coe_matrix, Matrix.SpecialLinearGroup.coe_neg,
+    Matrix.SpecialLinearGroup.map_apply_coe, RingHom.mapMatrix_apply, Int.coe_castRingHom,
+    Matrix.neg_apply, Matrix.map_apply, neg_neg, Matrix.SpecialLinearGroup.mapGL_coe_matrix,
+    algebraMap_int_eq]

LeanPool/LeanModularForms/GeneralizedResidueTheory/Basic.lean

@@ -152,7 +152,8 @@ private theorem exists_min_above_in_finite_union
   have hS_above_finite : S_above.Finite :=
     hS_finite.subset (fun s hs => hs.1)
   have hne : hS_above_finite.toFinset.Nonempty := by
-    rw [Set.Finite.toFinset_nonempty]; exact ⟨b, by simp [S_above, S, ht_lt_b]⟩
+    rw [Set.Finite.toFinset_nonempty]; exact ⟨b, by simp only [singleton_union, mem_insert_iff,
+      SetLike.mem_coe, mem_ofPred_eq, true_or, ht_lt_b, and_self, S_above, S]⟩
   set s_min := hS_above_finite.toFinset.min' hne
   have hs_min_in : s_min ∈ S_above :=
     (Set.Finite.mem_toFinset hS_above_finite).mp (Finset.min'_mem _ hne)

LeanPool/LeanModularForms/GeneralizedResidueTheory/Bridges.lean

@@ -38,11 +38,11 @@ private theorem rescale_mem_Icc (γ : PiecewiseC1Curve) (t : I) :
 
 private theorem rescale_zero (γ : PiecewiseC1Curve) :
     (γ.rescale ⟨0, left_mem_Icc.mpr zero_le_one⟩ : ℝ) = γ.a := by
-  simp [rescale, iccHomeoI_symm_apply_coe]
+  simp only [rescale, Icc.mk_zero, iccHomeoI_symm_apply_coe, Icc.coe_zero, mul_zero, zero_add]
 
 private theorem rescale_one (γ : PiecewiseC1Curve) :
     (γ.rescale ⟨1, right_mem_Icc.mpr zero_le_one⟩ : ℝ) = γ.b := by
-  simp [rescale, iccHomeoI_symm_apply_coe]
+  simp only [rescale, Icc.mk_one, iccHomeoI_symm_apply_coe, Icc.coe_one, mul_one, sub_add_cancel]
 
 /-- Convert a `PiecewiseC1Curve` to a mathlib `Path` by rescaling `[a,b]` to `[0,1]`.
 The path goes from `γ(a)` to `γ(b)`. -/

LeanPool/LeanModularForms/GeneralizedResidueTheory/CauchyPrimitive.lean

@@ -83,7 +83,7 @@ private lemma integral_t_mul_deriv_eq {f : ℂ → ℂ} {S : Set ℂ}
     have h3 : HasDerivAt (fun _ : ℝ => c) 0 t :=
       hasDerivAt_const t c
     convert h3.add h2 using 1
-    ring
+    ac_rfl
   have hv_deriv : ∀ x ∈ Set.Ioo (min 0 1) (max 0 1),
       HasDerivAt v (v' x) x := by
     intro t ht
@@ -96,7 +96,7 @@ private lemma integral_t_mul_deriv_eq {f : ℂ → ℂ} {S : Set ℂ}
     convert h_chain using 1
     · rfl
     · simp only [γ]
-      ring
+      ac_rfl
   have hu'_int : IntervalIntegrable u' MeasureTheory.volume 0 1 :=
     ContinuousOn.intervalIntegrable continuousOn_const
   have hv'_int : IntervalIntegrable v' MeasureTheory.volume 0 1 := by
@@ -235,7 +235,7 @@ private lemma segmentIntegrand_lipschitzOnWith {f : ℂ → ℂ}
         h_bound
     _ = M * ‖t • (x - y)‖ := by rw [h_diff]
     _ = M * (|t| * ‖x - y‖) := by rw [norm_smul]; simp only [Real.norm_eq_abs]
-    _ = |t| * M * ‖x - y‖ := by ring
+    _ = |t| * M * ‖x - y‖ := by ac_rfl
     _ = |t| * M * dist x y := by rw [dist_eq_norm]
     _ ≤ Real.toNNReal (|t| * M) * dist x y := by
         simp_all only [mem_Icc, Metric.mem_ball, real_smul, add_sub_add_left_eq_sub,
@@ -382,7 +382,7 @@ private lemma hasDerivAt_segmentIntegral {f : ℂ → ℂ}
       ∫ (t : ℝ) in (0 : ℝ)..1, ↑t * deriv f (c + t • (z - c)) * (z - c) from
       (intervalIntegral.integral_mul_const (𝕜 := ℂ) _ _).symm]
     convert h_ibp using 2
-    ext t; ring
+    ext t; ac_rfl
   suffices hH : HasDerivAt H (H' z) z by
     have h_prod := hH.mul h1
     refine h_prod.congr_deriv ?_

LeanPool/LeanModularForms/GeneralizedResidueTheory/Cycle.lean

@@ -14,7 +14,6 @@ import LeanPool.LeanModularForms.GeneralizedResidueTheory.Homotopy.Integrality
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
 import Mathlib.CategoryTheory.Category.Init
 import Mathlib.Combinatorics.Matroid.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Contour Cycles
@@ -142,7 +141,7 @@ private theorem sum_swap_winding_residue (Γ : ContourCycle) (S0 : Finset ℂ)
       2 * ↑Real.pi * I *
         (↑(Γ γ) * generalizedWindingNumber' γ.toFun γ.a γ.b s *
           residueAt f s)
-    from by ring), ← Finset.mul_sum, ← Finset.sum_mul]
+    from by ac_rfl), ← Finset.mul_sum, ← Finset.sum_mul]
 
 /-- **Generalized Residue Theorem for simple poles on a cycle.**
 
@@ -260,11 +259,11 @@ theorem windingNumberCycle_isInt (Γ : ContourCycle)
     ∃ n : ℤ, windingNumberCycle Γ z = ↑n := by
   simp only [windingNumberCycle, Finsupp.sum]
   apply Finset.sum_induction _ (fun x : ℂ => ∃ n : ℤ, x = ↑n)
-  · rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩; exact ⟨a + b, by push_cast; ring⟩
+  · rintro _ _ ⟨a, rfl⟩ ⟨b, rfl⟩; exact ⟨a + b, by push_cast; ac_rfl⟩
   · exact ⟨0, Int.cast_zero.symm⟩
   · intro γ hγ
     obtain ⟨m, hm⟩ := windingNumber_isInt_of_immersion_closed_avoiding γ z
       (h_closed γ hγ) (h_avoids γ hγ)
-    exact ⟨Γ γ * m, by rw [hm]; push_cast; ring⟩
+    exact ⟨Γ γ * m, by rw [hm]; push_cast; ac_rfl⟩
 
 end

LeanPool/LeanModularForms/GeneralizedResidueTheory/GeneralizedResidueTheorem.lean

@@ -18,7 +18,6 @@ import LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue.FlatnessTransf
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
 import Mathlib.CategoryTheory.Category.Init
 import Mathlib.Combinatorics.Matroid.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Generalized Residue Theorem -- Public API
@@ -245,7 +244,8 @@ theorem generalizedResidueTheorem_simplePoles (U : Set ℂ) (hU : IsOpen U)
     intro s hs
     rw [h_res_sing_eq s hs]
     have h_eq : (fun z => residueSimplePole f s / (z - s)) =
-        (fun z => residueSimplePole f s * (fun z => (z - s)⁻¹) z) := by ext z; simp [div_eq_mul_inv]
+        (fun z => residueSimplePole f s * (fun z => (z - s)⁻¹) z) := by ext z; simp only [
+          div_eq_mul_inv]
     rw [h_eq]
     apply CauchyPrincipalValueExists'.const_mul
     apply cauchyPrincipalValueExists_of_singular_inv γ s

LeanPool/LeanModularForms/GeneralizedResidueTheory/HomologicalCauchy.lean

@@ -11,7 +11,6 @@ public import LeanPool.LeanModularForms.GeneralizedResidueTheory.HomologicalCauc
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
 import Mathlib.CategoryTheory.Category.Init
 import Mathlib.Combinatorics.Matroid.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Null-Homologous Curves and the Cauchy Integral Theorem

LeanPool/LeanModularForms/GeneralizedResidueTheory/HomologicalCauchy/Basic.lean

@@ -12,7 +12,6 @@ import LeanPool.LeanModularForms.GeneralizedResidueTheory.Residue
 import Mathlib.Analysis.Calculus.FDeriv.Mul
 import Mathlib.CategoryTheory.Category.Init
 import Mathlib.Combinatorics.Matroid.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
 
 /-!
@@ -87,7 +86,7 @@ private lemma partition_filter_card_lt_left (P : Finset ℝ) {a' b' c : ℝ}
     exact ⟨ht.1, ht.2.1, lt_trans ht.2.2 hcb⟩
   · intro hsub
     have hcmem := hsub (Finset.mem_filter.mpr ⟨hc_part, hac, hcb⟩)
-    simp_all
+    simp_all only [Finset.mem_filter, lt_self_iff_false, and_false]
 
 private lemma partition_filter_card_lt_right (P : Finset ℝ) {a' b' c : ℝ}
     (hc_part : c ∈ P) (hac : a' < c) (hcb : c < b') :
@@ -100,7 +99,7 @@ private lemma partition_filter_card_lt_right (P : Finset ℝ) {a' b' c : ℝ}
     exact ⟨ht.1, lt_trans hac ht.2.1, ht.2.2⟩
   · intro hsub
     have hcmem := hsub (Finset.mem_filter.mpr ⟨hc_part, hac, hcb⟩)
-    simp_all
+    simp_all only [Finset.mem_filter, lt_self_iff_false, and_true, and_false]
 
 private lemma ftc_inductive_step {F : ℂ → ℂ} {f : ℂ → ℂ}
     (γ : PiecewiseC1Curve) (m : ℕ) (a' b' c : ℝ)

LeanPool/LeanModularForms/GeneralizedResidueTheory/HomologicalCauchy/DixonProof.lean

@@ -16,7 +16,6 @@ import Mathlib.Analysis.Normed.Module.Connected
 import Mathlib.CategoryTheory.Category.Init
 import Mathlib.Combinatorics.Matroid.Init
 import Mathlib.LinearAlgebra.Complex.FiniteDimensional
-import Mathlib.MeasureTheory.Covering.Besicovitch
 import Mathlib.Topology.MetricSpace.HausdorffDimension
 
 /-!
@@ -146,7 +145,7 @@ theorem dixonH1_eq (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
       (fun t => f w / (γ.toFun t - w) * deriv γ.toFun t) volume γ.a γ.b := by
     rw [show (fun t => f w / (γ.toFun t - w) * deriv γ.toFun t) =
         (fun t => f w * ((γ.toFun t - w)⁻¹ * deriv γ.toFun t)) from by
-      ext t; rw [div_eq_mul_inv]; ring]
+      ext t; rw [div_eq_mul_inv]; ac_rfl]
     exact h_base_int.const_mul _
   rw [intervalIntegral.integral_sub
     (dixonH1_cauchyIntegrand_integrable hU hf γ hγ_in_U w hoff) h_fw_int]
@@ -218,12 +217,12 @@ private lemma dixonH2_deriv_bound (f : ℂ → ℂ) (γ : PiecewiseC1Immersion)
         apply mul_le_mul
         · apply mul_le_mul
           · exact hM_f t ht
-          · exact pow_le_pow_left₀ (by positivity)
+          · exact pow_le_pow_left₀ (by exact inv_nonneg_of_nonneg (norm_nonneg (γ.toFun t - x)))
               (inv_anti₀ hε_pos (hdist_lb x hx_ball t ht)) 2
-          · positivity
+          · exact Even.pow_nonneg (even_two_mul 1) ‖γ.toFun t - x‖⁻¹
           · exact hM_f_nn
         · exact hM_d t ht
-        · positivity
+        · exact norm_nonneg (deriv γ.toFun t)
         · simp_all only [mem_Icc, and_imp, Metric.mem_ball, uIoc_of_le, mem_Ioc, and_true,
           inv_pow, inv_pos,
               pow_succ_pos, mul_nonneg_iff_of_pos_right]
@@ -280,8 +279,8 @@ private lemma dixonH2_hasDerivAt (f : ℂ → ℂ) (γ : PiecewiseC1Immersion)
       exact mul_le_mul
         (mul_le_mul (hM_f t ht)
           (pow_le_pow_left₀ (by positivity) (inv_anti₀ hε_pos (_hdist_lb_w t ht)) 2)
-          (by positivity) _hM_f_nn)
-        (hM_d t ht) (by positivity) (mul_nonneg _hM_f_nn (by positivity))
+          (by exact Even.pow_nonneg (even_two_mul 1) ‖γ.toFun t - w‖⁻¹) _hM_f_nn)
+        (hM_d t ht) (by exact norm_nonneg (deriv γ.toFun t)) (mul_nonneg _hM_f_nn (by positivity))
   have hF'_meas : AEStronglyMeasurable (dixonH2_F' f γ w)
       (volume.restrict (Set.uIoc γ.a γ.b)) := hF'_int.def'.aestronglyMeasurable
   have h_bound : ∀ᵐ t ∂volume, t ∈ Set.uIoc γ.a γ.b →
@@ -516,7 +515,7 @@ private theorem dixonH1_F'_aestronglyMeasurable {M_d C_b δ₀ : ℝ}
         have hC : Filter.Tendsto (fun n : ℕ => (1 : ℂ) / ((n : ℂ) + 1)) Filter.atTop (𝓝 0) := by
           have := Complex.continuous_ofReal.continuousAt.tendsto.comp hR
           simp only [Function.comp_def] at this
-          exact this.congr (fun n => by push_cast; ring)
+          exact this.congr (fun n => by push_cast; ac_rfl)
         exact hC
       · exact Filter.Eventually.of_forall (fun n => by
           apply div_ne_zero one_ne_zero
@@ -527,7 +526,8 @@ private theorem dixonH1_F'_aestronglyMeasurable {M_d C_b δ₀ : ℝ}
         ((1 : ℂ) / (↑n + 1))⁻¹ •
           (dslope f (γ.toFun t) (w₀ + 1 / (↑n + 1)) - dslope f (γ.toFun t) w₀) *
         deriv γ.toFun t := by
-      simp_all
+      simp_all only [mem_Icc, and_imp, mem_image, Metric.mem_ball, forall_exists_index, mem_Ioc,
+        and_true, hasDerivAt_deriv_iff, one_div, inv_inv, smul_eq_mul, implies_true]
     simp_rw [hGn_eq]
     exact (hderiv.tendsto_slope_zero.comp h_tendsto_zero).mul_const _
 
@@ -590,7 +590,7 @@ theorem dixonH1_differentiableOn (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
     apply Filter.eventually_of_mem (Metric.ball_mem_nhds w₀ hε_pos)
     intro x hx
     exact (dixonH1_dslope_intervalIntegrable hU hf γ hγ_in_U x C M_d hC_pos
-      (fun c hc => hBd c hc x (Metric.ball_subset_ball (by linarith) hx))
+      (fun c hc => hBd c hc x (Metric.ball_subset_ball (by linarith only [hε_pos, h2ε_le_δ₀]) hx))
       hM_d).def'.aestronglyMeasurable
   have hF'_meas := dixonH1_F'_aestronglyMeasurable hU hf γ hγ_in_U w₀ hw₀
     hdslope_diff hM_d hδ₀_pos hBd hC_pos
@@ -717,7 +717,7 @@ theorem dixonFunction_differentiable (hU : IsOpen U) (hf : DifferentiableOn ℂ
         obtain ⟨n2, hn2⟩ := hwn_int w'' hw''
         have hm : generalizedWindingNumber' γ.toFun γ.a γ.b w''' -
             generalizedWindingNumber' γ.toFun γ.a γ.b w'' = (n1 - n2 : ℤ) := by
-          push_cast [hn1, hn2]; ring
+          push_cast [hn1, hn2]; ac_rfl
         have h_norm_m : ‖((n1 - n2 : ℤ) : ℂ)‖ < 1 / 2 := hm ▸ h_lt
         rw [Complex.norm_intCast] at h_norm_m
         have h_zero : n1 - n2 = 0 := by
@@ -793,9 +793,9 @@ private lemma windingNumber_norm_lt_one (γ : PiecewiseC1Immersion) {R M_d : ℝ
     (hw : M_d * (γ.b - γ.a) / (2 * Real.pi) < ‖w‖ - R) :
     ‖generalizedWindingNumber' γ.toFun γ.a γ.b w‖ < 1 := by
   have hab : γ.a ≤ γ.b := le_of_lt γ.hab
-  have hba_nn : 0 ≤ γ.b - γ.a := by linarith
+  have hba_nn : 0 ≤ γ.b - γ.a := by exact sub_nonneg.mpr hab
   have h2pi_pos : 0 < 2 * Real.pi := Real.two_pi_pos
-  have hpos : 0 < ‖w‖ - R := by linarith
+  have hpos : 0 < ‖w‖ - R := by exact sub_pos.mpr hR_lt
   rw [generalizedWindingNumber_eq_classical_away γ.toPiecewiseC1Curve w hoff, norm_mul,
     norm_inv, norm_mul, norm_mul, Complex.norm_two, Complex.norm_real,
     Real.norm_of_nonneg Real.pi_pos.le, Complex.norm_I, mul_one]
@@ -956,9 +956,9 @@ lemma piecewiseC1_image_interior_empty (γ : PiecewiseC1Immersion) :
         hLip.mono Set.inter_subset_right⟩
     · apply lt_of_le_of_lt (dimH_mono (Set.subset_univ _))
       simp only [Real.dimH_univ]
-      simp_all
+      simp_all only [finrank_real_complex, Nat.cast_ofNat, Nat.one_lt_ofNat]
   · rw [(γ.partition.finite_toSet.image γ.toFun).dimH_zero]
-    simp_all
+    simp_all only [finrank_real_complex, Nat.cast_ofNat, Nat.ofNat_pos]
 
 theorem contourIntegral_eq_zero_of_nullHomologous (hU : IsOpen U) (hf : DifferentiableOn ℂ f U)
     (γ : PiecewiseC1Immersion) (h_null : IsNullHomologous γ U) :

LeanPool/LeanModularForms/GeneralizedResidueTheory/HomologicalCauchy/Meromorphic.lean

@@ -19,7 +19,6 @@ import LeanPool.LeanModularForms.GeneralizedResidueTheory.WindingNumber.Proposit
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
 import Mathlib.CategoryTheory.Category.Init
 import Mathlib.Combinatorics.Matroid.Init
-import Mathlib.MeasureTheory.Covering.Besicovitch
 
 /-!
 # Meromorphic Contour Integral Vanishing (Null-Homologous)
@@ -426,7 +425,7 @@ theorem conditionsAB_imply_higherOrderCancel_nh (U : Set ℂ) (hU : IsOpen U)
       exact intervalIntegrable_cpvIntegrandOn_of_continuousOn_diff
         U S0 _ hfres_cont γ h_null.image_subset ε hε
     rw [← intervalIntegral.integral_sub h_int_f h_int_fres]
-    simp_all
+    simp_all only [ne_eq, mem_Icc, and_imp]
   exact higherOrderCancel_assembly_nh U hU S0 f hf γ h_null
     hMero hCondA hCondB hγ_meas h_no_endpt h_unique_cross hS0_in_U
 
@@ -489,6 +488,6 @@ lemma pv_res_tendsto_of_immersion_nullHomologous (U : Set ℂ) (S : Set ℂ)
       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
+    simp_all only [gt_iff_lt, ne_eq, mem_Icc, and_imp]
+  simp_all only [gt_iff_lt, ne_eq, mem_Icc, and_imp]
 

LeanPool/LeanModularForms/GeneralizedResidueTheory/Homotopy/CircleParam.lean

@@ -54,7 +54,8 @@ lemma circleParam_closed (z₀ : ℂ) (r : ℝ) (a b : ℝ) (hab : a < b) :
   simp only [circleParam]
   have hne : (b : ℂ) - a ≠ 0 := by
     simp only [sub_ne_zero, Complex.ofReal_inj, ne_eq]; exact ne_of_gt hab
-  simp_all
+  simp_all only [ne_eq, sub_self, zero_div, mul_zero, exp_zero, mul_one, not_false_eq_true,
+    div_self, exp_two_pi_mul_I]
 
 lemma circleParam_dist (z₀ : ℂ) (r : ℝ) (hr : 0 ≤ r)
     (a b : ℝ) (_hab : a < b) (t : ℝ) :
@@ -339,10 +340,10 @@ theorem winding_of_S1_curve_eq_degree (z₀ : ℂ) (a b : ℝ) (_hab : a < b)
     have h2 := h1.const_mul I
     have h3 : HasDerivAt (fun u => exp (I * (θ u : ℂ)))
         (exp (I * (θ t : ℂ)) * (I * (Complex.ofReal (deriv θ t)))) t :=
-      ((hasDerivAt_exp _).scomp t h2).congr_deriv (by rw [smul_eq_mul]; ring)
+      ((hasDerivAt_exp _).scomp t h2).congr_deriv (by rw [smul_eq_mul]; ac_rfl)
     have h4 := (hasDerivAt_const t z₀).add h3
     simp only [zero_add] at h4
-    exact h4.congr_deriv (by ring)
+    exact h4.congr_deriv (by ac_rfl)
   have h_integrand : ∀ t,
       (γ t - z₀)⁻¹ * deriv γ t =
       I * (Complex.ofReal (deriv θ t)) := by
@@ -368,8 +369,8 @@ theorem winding_of_S1_curve_eq_degree (z₀ : ℂ) (a b : ℝ) (_hab : a < b)
         (fun x _ => hasDerivAt_ofReal_comp θ x (hθ_diff x)) h_ofReal_int
     rw [h_ftc,
       show (θ b : ℂ) - (θ a : ℂ) = ((θ b - θ a : ℝ) : ℂ) from
-        by push_cast; ring,
-      hθ_change]; push_cast; ring
+        by push_cast; ac_rfl,
+      hθ_change]; push_cast; ac_rfl
   have h_S1 : ∀ t, ‖γ t - z₀‖ = 1 := by
     intro t; simp only [γ, add_sub_cancel_left, mul_comm I]; exact norm_exp_ofReal_mul_I _
   have hint_const : ∀ ε > 0, ε < 1 →

LeanPool/LeanModularForms/GeneralizedResidueTheory/Homotopy/Integrality.lean

@@ -211,8 +211,10 @@ private lemma exists_partition_free_subinterval
     exact ⟨by linarith [le_max_right a (t - ε / 2), hs.1],
            by linarith [min_le_right b (t + ε / 2), hs.2]⟩
   · intro x hx
-    simp_all
-  · simp_all
+    simp_all only [mem_Ioo, sub_lt_self_iff, lt_add_iff_pos_right, and_self, not_false_eq_true,
+      gt_iff_lt, and_imp, max_lt_iff, lt_min_iff]
+  · simp_all only [mem_Ioo, sub_lt_self_iff, lt_add_iff_pos_right, and_self, not_false_eq_true,
+    gt_iff_lt, and_imp, max_lt_iff, div_pos_iff_of_pos_left, Nat.ofNat_pos, lt_min_iff]
 
 private lemma logDeriv_integrand_bound
     {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} {M δ : ℝ}
@@ -516,7 +518,7 @@ theorem winding_integrand_bounded_of_uniform_avoidance
       ≤ ‖(H (t, s) - z₀)⁻¹‖ * ‖deriv (fun t' => H (t', s)) t‖ := norm_mul_le _ _
     _ ≤ δ⁻¹ * M := mul_le_mul h_inv_bound (hM_bound t ht s hs)
         (norm_nonneg _) (le_of_lt (inv_pos.mpr hδ_pos))
-    _ = M / δ := by ring
+    _ = M / δ := by ac_rfl
 
 private lemma gFunc_constant_smooth
     {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ}
@@ -630,7 +632,7 @@ private theorem integral_closed_curve_eq_two_pi_int
       (hγ_avoid b (right_mem_Icc.mpr (le_of_lt hab))))
   rw [Complex.exp_eq_one_iff] at hexp
   obtain ⟨n, hn⟩ := hexp
-  exact ⟨n, by rw [hn]; ring⟩
+  exact ⟨n, by rw [hn]; ac_rfl⟩
 
 /-- The winding number of a smooth closed curve avoiding z₀
 is an integer. -/