chore(NumberTheory/LSeries): unsqueeze lots of terminal simps (#21133)

Author: loefflerd

Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

@@ -177,12 +177,11 @@ variable (P : StrongFEPair E)
 
 /-- As `x → ∞`, `f x` decays faster than any power of `x`. -/
 lemma hf_top' (r : ℝ) : P.f =O[atTop] (· ^ r) := by
-  simpa only [P.hf₀, sub_zero] using P.hf_top r
+  simpa [P.hf₀] using P.hf_top r
 
 /-- As `x → 0`, `f x` decays faster than any power of `x`. -/
 lemma hf_zero' (r : ℝ) : P.f =O[𝓝[>] 0] (· ^ r) := by
-  have := P.hg₀ ▸ P.hf_zero r
-  simpa only [smul_zero, sub_zero]
+  simpa using (P.hg₀ ▸ P.hf_zero r :)
 
 /-!
 ## Main theorems on strong FE-pairs
@@ -231,8 +230,7 @@ theorem functional_equation (s : ℂ) :
   simp_rw [P.h_feq' t ht, ← mul_smul]
   -- some simple `cpow` arithmetic to finish
   rw [cpow_neg, ofReal_cpow (le_of_lt ht)]
-  have : (t : ℂ) ^ (P.k : ℂ) ≠ 0 := by
-    simpa only [← ofReal_cpow (le_of_lt ht), ofReal_ne_zero] using (rpow_pos_of_pos ht _).ne'
+  have : (t : ℂ) ^ (P.k : ℂ) ≠ 0 := by simpa [← ofReal_cpow ht.le] using (rpow_pos_of_pos ht _).ne'
   field_simp [P.hε]
 
 end StrongFEPair
@@ -397,13 +395,13 @@ theorem differentiableAt_Λ {s : ℂ} (hs : s ≠ 0 ∨ P.f₀ = 0) (hs' : s ≠
     DifferentiableAt ℂ P.Λ s := by
   refine ((P.differentiable_Λ₀ s).sub ?_).sub ?_
   · rcases hs with hs | hs
-    · simpa only [one_div] using (differentiableAt_inv hs).smul_const P.f₀
-    · simpa only [hs, smul_zero] using differentiableAt_const (0 : E)
+    · simpa using (differentiableAt_inv hs).smul_const _
+    · simp [hs]
   · rcases hs' with hs' | hs'
     · apply DifferentiableAt.smul_const
       apply (differentiableAt_const _).div ((differentiableAt_const _).sub (differentiable_id _))
-      rwa [sub_ne_zero, ne_comm]
-    · simpa only [hs', smul_zero] using differentiableAt_const (0 : E)
+      simpa [sub_eq_zero, eq_comm]
+    · simp [hs']
 
 /-- Relation between `Λ s` and the Mellin transform of `f - f₀`, where the latter is defined. -/
 theorem hasMellin [CompleteSpace E]

Mathlib/NumberTheory/LSeries/Basic.lean

@@ -104,8 +104,8 @@ lemma pow_mul_term_eq (f : ℕ → ℂ) (s : ℂ) (n : ℕ) :
 lemma norm_term_eq (f : ℕ → ℂ) (s : ℂ) (n : ℕ) :
     ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / n ^ s.re := by
   rcases eq_or_ne n 0 with rfl | hn
-  · simp only [term_zero, norm_zero, ↓reduceIte]
-  · rw [if_neg hn, term_of_ne_zero hn, norm_div, norm_natCast_cpow_of_pos <| Nat.pos_of_ne_zero hn]
+  · simp
+  · simp [hn, norm_natCast_cpow_of_pos <| Nat.pos_of_ne_zero hn]
 
 lemma norm_term_le {f g : ℕ → ℂ} (s : ℂ) {n : ℕ} (h : ‖f n‖ ≤ ‖g n‖) :
     ‖term f s n‖ ≤ ‖term g s n‖ := by
@@ -118,8 +118,8 @@ lemma norm_term_le_of_re_le_re (f : ℕ → ℂ) {s s' : ℂ} (h : s.re ≤ s'.r
     ‖term f s' n‖ ≤ ‖term f s n‖ := by
   simp only [norm_term_eq]
   split
-  next => rfl
-  next hn => gcongr; exact Nat.one_le_cast.mpr <| Nat.one_le_iff_ne_zero.mpr hn
+  · next => rfl
+  · next hn => gcongr; exact Nat.one_le_cast.mpr <| Nat.one_le_iff_ne_zero.mpr hn
 
 section positivity
 
@@ -178,9 +178,9 @@ lemma LSeriesSummable.congr' {f g : ℕ → ℂ} (s : ℂ) (h : f =ᶠ[atTop] g)
     rw [eventuallyEq_iff_exists_mem] at h ⊢
     obtain ⟨S, hS, hS'⟩ := h
     refine ⟨S \ {0}, diff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩
-    simp only [Set.mem_diff, Set.mem_singleton_iff] at hn
-    simp only [term_of_ne_zero hn.2, hS' hn.1]
-  exact Eventually.mono this.symm fun n hn ↦ by simp only [hn, le_rfl]
+    rw [Set.mem_diff, Set.mem_singleton_iff] at hn
+    simp [hn.2, hS' hn.1]
+  exact this.symm.mono fun n hn ↦ by simp [hn]
 
 open Filter in
 /-- If `f` and `g` agree on large `n : ℕ`, then the `LSeries` of `f` converges at `s`
@@ -195,8 +195,7 @@ theorem LSeries.eq_zero_of_not_LSeriesSummable (f : ℕ → ℂ) (s : ℂ) :
 
 @[simp]
 theorem LSeriesSummable_zero {s : ℂ} : LSeriesSummable 0 s := by
-  simp only [LSeriesSummable, funext (term_def 0 s), Pi.zero_apply, zero_div, ite_self,
-    summable_zero]
+  simp [LSeriesSummable, funext (term_def 0 s), summable_zero]
 
 /-- This states that the L-series of the sequence `f` converges absolutely at `s` and that
 the value there is `a`. -/
@@ -221,7 +220,7 @@ lemma LSeriesHasSum_iff {f : ℕ → ℂ} {s a : ℂ} :
 
 lemma LSeriesHasSum_congr {f g : ℕ → ℂ} (s a : ℂ) (h : ∀ {n}, n ≠ 0 → f n = g n) :
     LSeriesHasSum f s a ↔ LSeriesHasSum g s a := by
-  simp only [LSeriesHasSum_iff, LSeriesSummable_congr s h, LSeries_congr s h]
+  simp [LSeriesHasSum_iff, LSeriesSummable_congr s h, LSeries_congr s h]
 
 lemma LSeriesSummable.of_re_le_re {f : ℕ → ℂ} {s s' : ℂ} (h : s.re ≤ s'.re)
     (hf : LSeriesSummable f s) : LSeriesSummable f s' := by
@@ -260,7 +259,7 @@ scoped[LSeries.notation] notation "δ" => delta
 @[simp]
 lemma LSeries_zero : LSeries 0 = 0 := by
   ext
-  simp only [LSeries, LSeries.term, Pi.zero_apply, zero_div, ite_self, tsum_zero]
+  simp [LSeries, LSeries.term]
 
 section delta
 
@@ -272,16 +271,14 @@ open Nat Complex
 
 lemma term_delta (s : ℂ) (n : ℕ) : term δ s n = if n = 1 then 1 else 0 := by
   rcases eq_or_ne n 0 with rfl | hn
-  · simp only [term_zero, zero_ne_one, ↓reduceIte]
-  · simp only [ne_eq, hn, not_false_eq_true, term_of_ne_zero, delta]
-    rcases eq_or_ne n 1 with rfl | hn'
-    · simp only [↓reduceIte, cast_one, one_cpow, ne_eq, one_ne_zero, not_false_eq_true, div_self]
-    · simp only [hn', ↓reduceIte, zero_div]
+  · simp
+  · rcases eq_or_ne n 1 with hn' | hn' <;>
+    simp [hn, hn', delta]
 
 lemma mul_delta_eq_smul_delta {f : ℕ → ℂ} : f * δ = f 1 • δ := by
   ext n
-  simp only [Pi.mul_apply, delta, mul_ite, mul_one, mul_zero, Pi.smul_apply, smul_eq_mul]
-  split_ifs with hn <;> simp only [hn]
+  by_cases hn : n = 1 <;>
+  simp [hn, delta]
 
 lemma mul_delta {f : ℕ → ℂ} (h : f 1 = 1) : f * δ = δ := by
   rw [mul_delta_eq_smul_delta, h, one_smul]
@@ -297,7 +294,7 @@ end LSeries
 /-- The L-series of `δ` is the constant function `1`. -/
 lemma LSeries_delta : LSeries δ = 1 := by
   ext
-  simp only [LSeries, LSeries.term_delta, tsum_ite_eq, Pi.one_apply]
+  simp [LSeries, LSeries.term_delta]
 
 end delta
 
@@ -335,31 +332,25 @@ lemma LSeriesSummable_of_le_const_mul_rpow {f : ℕ → ℂ} {x : ℝ} {s : ℂ}
     (h : ∃ C, ∀ n ≠ 0, ‖f n‖ ≤ C * n ^ (x - 1)) :
     LSeriesSummable f s := by
   obtain ⟨C, hC⟩ := h
-  have hC₀ : 0 ≤ C := by
-    specialize hC 1 one_ne_zero
-    simp only [Nat.cast_one, Real.one_rpow, mul_one] at hC
-    exact (norm_nonneg _).trans hC
+  have hC₀ : 0 ≤ C := (norm_nonneg <| f 1).trans <| by simpa using hC 1 one_ne_zero
   have hsum : Summable fun n : ℕ ↦ ‖(C : ℂ) / n ^ (s + (1 - x))‖ := by
     simp_rw [div_eq_mul_inv, norm_mul, ← cpow_neg]
     have hsx : -s.re + x - 1 < -1 := by linarith only [hs]
     refine Summable.mul_left _ <|
       Summable.of_norm_bounded_eventually_nat (fun n ↦ (n : ℝ) ^ (-s.re + x - 1)) ?_ ?_
-    · simp only [Real.summable_nat_rpow, hsx]
-    · simp only [neg_add_rev, neg_sub, norm_norm, Filter.eventually_atTop]
-      refine ⟨1, fun n hn ↦ ?_⟩
+    · simpa
+    · simp only [norm_norm, Filter.eventually_atTop]
+      refine ⟨1, fun n hn ↦ le_of_eq ?_⟩
       simp only [norm_natCast_cpow_of_pos hn, add_re, sub_re, neg_re, ofReal_re, one_re]
-      convert le_refl ?_ using 2
-      ring
+      ring_nf
   refine Summable.of_norm <| hsum.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ ?_)
   rcases n.eq_zero_or_pos with rfl | hn
-  · simp only [term_zero, norm_zero]
-    exact norm_nonneg _
+  · simpa only [term_zero, norm_zero] using norm_nonneg _
   have hn' : 0 < (n : ℝ) ^ s.re := Real.rpow_pos_of_pos (Nat.cast_pos.mpr hn) _
   simp_rw [term_of_ne_zero hn.ne', norm_div, norm_natCast_cpow_of_pos hn, div_le_iff₀ hn',
     norm_eq_abs (C : ℂ), abs_ofReal, _root_.abs_of_nonneg hC₀, div_eq_mul_inv, mul_assoc,
     ← Real.rpow_neg <| Nat.cast_nonneg _, ← Real.rpow_add <| Nat.cast_pos.mpr hn]
-  simp only [add_re, sub_re, one_re, ofReal_re, neg_add_rev, neg_sub, neg_add_cancel_right]
-  exact hC n <| Nat.pos_iff_ne_zero.mp hn
+  simpa using hC n <| Nat.pos_iff_ne_zero.mp hn
 
 open Filter Finset Real Nat in
 /-- If `f = O(n^(x-1))` and `re s > x`, then the `LSeries` of `f` is summable at `s`. -/
@@ -386,12 +377,11 @@ lemma LSeriesSummable_of_isBigO_rpow {f : ℕ → ℂ} {x : ℝ} {s : ℂ} (hs :
 /-- If `f` is bounded, then its `LSeries` is summable at `s` when `re s > 1`. -/
 theorem LSeriesSummable_of_bounded_of_one_lt_re {f : ℕ → ℂ} {m : ℝ}
     (h : ∀ n ≠ 0, Complex.abs (f n) ≤ m) {s : ℂ} (hs : 1 < s.re) :
-    LSeriesSummable f s := by
-  refine LSeriesSummable_of_le_const_mul_rpow hs ⟨m, fun n hn ↦ ?_⟩
-  simp only [norm_eq_abs, sub_self, Real.rpow_zero, mul_one, h n hn]
+    LSeriesSummable f s :=
+  LSeriesSummable_of_le_const_mul_rpow hs ⟨m, fun n hn ↦ by simp [h n hn]⟩
 
 /-- If `f` is bounded, then its `LSeries` is summable at `s : ℝ` when `s > 1`. -/
 theorem LSeriesSummable_of_bounded_of_one_lt_real {f : ℕ → ℂ} {m : ℝ}
     (h : ∀ n ≠ 0, Complex.abs (f n) ≤ m) {s : ℝ} (hs : 1 < s) :
     LSeriesSummable f s :=
-  LSeriesSummable_of_bounded_of_one_lt_re h <| by simp only [ofReal_re, hs]
+  LSeriesSummable_of_bounded_of_one_lt_re h <| by simp [hs]

Mathlib/NumberTheory/LSeries/Convergence.lean

@@ -41,47 +41,42 @@ open LSeries
 
 lemma LSeriesSummable_of_abscissaOfAbsConv_lt_re {f : ℕ → ℂ} {s : ℂ}
     (hs : abscissaOfAbsConv f < s.re) : LSeriesSummable f s := by
-  simp only [abscissaOfAbsConv, sInf_lt_iff, Set.mem_image, Set.mem_setOf_eq,
-    exists_exists_and_eq_and, EReal.coe_lt_coe_iff] at hs
-  obtain ⟨y, hy, hys⟩ := hs
+  obtain ⟨y, hy, hys⟩ : ∃ a : ℝ, LSeriesSummable f a ∧ a < s.re := by
+    simpa [abscissaOfAbsConv, sInf_lt_iff] using hs
   exact hy.of_re_le_re <| ofReal_re y ▸ hys.le
 
 lemma LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re {f : ℕ → ℂ} {s : ℂ}
     (hs : abscissaOfAbsConv f < s.re) :
     ∃ x : ℝ, x < s.re ∧ LSeriesSummable f x := by
   obtain ⟨x, hx₁, hx₂⟩ := EReal.exists_between_coe_real hs
-  exact ⟨x, EReal.coe_lt_coe_iff.mp hx₂, LSeriesSummable_of_abscissaOfAbsConv_lt_re hx₁⟩
+  exact ⟨x, by simpa using hx₂, LSeriesSummable_of_abscissaOfAbsConv_lt_re hx₁⟩
 
 lemma LSeriesSummable.abscissaOfAbsConv_le {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) :
-    abscissaOfAbsConv f ≤ s.re := by
-  refine sInf_le <| Membership.mem.out ?_
-  simp only [Set.mem_setOf_eq, Set.mem_image, EReal.coe_eq_coe_iff, exists_eq_right]
-  exact h.of_re_le_re <| by simp only [ofReal_re, le_refl]
+    abscissaOfAbsConv f ≤ s.re :=
+  sInf_le <| by simpa using h.of_re_le_re (by simp)
 
 lemma LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable {f : ℕ → ℂ} {x : ℝ}
     (h : ∀ y : ℝ, x < y → LSeriesSummable f y) :
     abscissaOfAbsConv f ≤ x := by
-  refine sInf_le_iff.mpr fun y hy ↦ ?_
-  simp only [mem_lowerBounds, Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp,
-    forall_apply_eq_imp_iff₂] at hy
-  have H (a : EReal) : x < a → y ≤ a := by
-    induction' a with a₀
-    · simp only [not_lt_bot, le_bot_iff, IsEmpty.forall_iff]
-    · exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)
-    · simp only [EReal.coe_lt_top, le_top, forall_true_left]
-  exact Set.Ioi_subset_Ici_iff.mp H
+  refine sInf_le_iff.mpr fun y hy ↦ le_of_forall_gt_imp_ge_of_dense fun a ↦ ?_
+  replace hy : ∀ (a : ℝ), LSeriesSummable f a → y ≤ a := by simpa [mem_lowerBounds] using hy
+  cases a with
+  | h_real a₀ => exact_mod_cast fun ha ↦ hy a₀ (h a₀ ha)
+  | h_bot => simp
+  | h_top => simp
 
 lemma LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' {f : ℕ → ℂ} {x : EReal}
     (h : ∀ y : ℝ, x < y → LSeriesSummable f y) :
     abscissaOfAbsConv f ≤ x := by
-  induction' x with y
-  · refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_
-    induction' y with z
-    · simp only [gt_iff_lt, lt_self_iff_false] at hy
-    · exact ⟨z - 1,  ⟨z-1, h (z - 1) <| EReal.bot_lt_coe _, rfl⟩, by norm_cast; exact sub_one_lt z⟩
-    · exact ⟨0, ⟨0, h 0 <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩
-  · exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| by exact_mod_cast h
-  · exact le_top
+  cases x with
+  | h_real => exact abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable <| mod_cast h
+  | h_top => exact le_top
+  | h_bot =>
+    refine le_of_eq <| sInf_eq_bot.mpr fun y hy ↦ ?_
+    cases y with
+    | h_bot => simp at hy
+    | h_real y => exact ⟨_,  ⟨_, h _ <| EReal.bot_lt_coe _, rfl⟩, mod_cast sub_one_lt y⟩
+    | h_top => exact ⟨_, ⟨_, h _ <| EReal.bot_lt_coe 0, rfl⟩, EReal.zero_lt_top⟩
 
 /-- If `‖f n‖` is bounded by a constant times `n^x`, then the abscissa of absolute convergence
 of `f` is bounded by `x + 1`. -/
@@ -108,35 +103,27 @@ lemma LSeries.abscissaOfAbsConv_le_of_isBigO_rpow {f : ℕ → ℂ} {x : ℝ}
 /-- If `f` is bounded, then the abscissa of absolute convergence of `f` is bounded above by `1`. -/
 lemma LSeries.abscissaOfAbsConv_le_of_le_const {f : ℕ → ℂ} (h : ∃ C, ∀ n ≠ 0, ‖f n‖ ≤ C) :
     abscissaOfAbsConv f ≤ 1 := by
-  convert abscissaOfAbsConv_le_of_le_const_mul_rpow (x := 0) ?_
-  · simp only [EReal.coe_zero, zero_add]
-  · simpa only [norm_eq_abs, Real.rpow_zero, mul_one] using h
+  simpa using abscissaOfAbsConv_le_of_le_const_mul_rpow (x := 0) (by simpa using h)
 
 open Filter in
 /-- If `f` is `O(1)`, then the abscissa of absolute convergence of `f` is bounded above by `1`. -/
-lemma LSeries.abscissaOfAbsConv_le_one_of_isBigO_one {f : ℕ → ℂ} (h : f =O[atTop] (1 : ℕ → ℝ)) :
+lemma LSeries.abscissaOfAbsConv_le_one_of_isBigO_one {f : ℕ → ℂ} (h : f =O[atTop] fun _ ↦ (1 : ℝ)) :
     abscissaOfAbsConv f ≤ 1 := by
-  convert abscissaOfAbsConv_le_of_isBigO_rpow (x := 0) ?_
-  · simp only [EReal.coe_zero, zero_add]
-  · simpa only [Real.rpow_zero] using h
+  simpa using abscissaOfAbsConv_le_of_isBigO_rpow (x := 0) (by simpa using h)
 
 /-- If `f` is real-valued and `x` is strictly greater than the abscissa of absolute convergence
 of `f`, then the real series `∑' n, f n / n ^ x` converges. -/
 lemma LSeries.summable_real_of_abscissaOfAbsConv_lt {f : ℕ → ℝ} {x : ℝ}
     (h : abscissaOfAbsConv (f ·) < x) :
     Summable fun n : ℕ ↦ f n / (n : ℝ) ^ x := by
-  have h' : abscissaOfAbsConv (f ·) < (x : ℂ).re := by simpa only [ofReal_re] using h
-  have := LSeriesSummable_of_abscissaOfAbsConv_lt_re h'
-  rw [LSeriesSummable, show term _ _ = fun n ↦ _ from rfl] at this
-  conv at this =>
-    enter [1, n]
-    rw [term_def, ← ofReal_natCast, ← ofReal_cpow n.cast_nonneg, ← ofReal_div, ← ofReal_zero,
-      ← apply_ite]
-  rw [summable_ofReal] at this
+  have aux : term (f ·) x = fun n ↦ ↑(if n = 0 then 0 else f n / (n : ℝ) ^ x) := by
+    ext n
+    simp [term_def, apply_ite ((↑) : ℝ → ℂ), ofReal_cpow n.cast_nonneg]
+  have := LSeriesSummable_of_abscissaOfAbsConv_lt_re (ofReal_re x ▸ h)
+  simp only [LSeriesSummable, aux, summable_ofReal] at this
   refine this.congr_cofinite ?_
-  filter_upwards [Set.Finite.compl_mem_cofinite <| Set.finite_singleton 0] with n hn
-  simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at hn
-  exact if_neg hn
+  filter_upwards [(Set.finite_singleton 0).compl_mem_cofinite] with n hn
+    using if_neg (by simpa using hn)
 
 /-- If `F` is a binary operation on `ℕ → ℂ` with the property that the `LSeries` of `F f g`
 converges whenever the `LSeries` of `f` and `g` do, then the abscissa of absolute convergence