diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean
index f1a86dba16e40d..7d250d8f3dc2c0 100644
--- a/Mathlib/Analysis/Analytic/Basic.lean
+++ b/Mathlib/Analysis/Analytic/Basic.lean
@@ -237,20 +237,6 @@ theorem HasFPowerSeriesOnBall.mono (hf : HasFPowerSeriesOnBall f p x r) (r'_pos
     (hr : r' ≤ r) : HasFPowerSeriesOnBall f p x r' :=
   ⟨le_trans hr hf.1, r'_pos, fun hy => hf.hasSum (Metric.eball_subset_eball hr hy)⟩
 
-lemma HasFPowerSeriesWithinOnBall.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F}
-    {s : Set E} {x : E} {r : ℝ≥0∞} (h : HasFPowerSeriesWithinOnBall f p s x r)
-    (h' : EqOn g f (s ∩ Metric.eball x r)) (h'' : g x = f x) :
-    HasFPowerSeriesWithinOnBall g p s x r := by
-  refine ⟨h.r_le, h.r_pos, ?_⟩
-  intro y hy h'y
-  convert h.hasSum hy h'y using 1
-  simp only [mem_insert_iff, add_eq_left] at hy
-  rcases hy with rfl | hy
-  · simpa using h''
-  · apply h'
-    refine ⟨hy, ?_⟩
-    simpa [edist_eq_enorm_sub] using h'y
-
 /-- Variant of `HasFPowerSeriesWithinOnBall.congr` in which one requests equality on `insert x s`
 instead of separating `x` and `s`. -/
 lemma HasFPowerSeriesWithinOnBall.congr' {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F}
@@ -261,6 +247,16 @@ lemma HasFPowerSeriesWithinOnBall.congr' {f g : E → F} {p : FormalMultilinearS
   convert h.hasSum hy h'y using 1
   exact h' ⟨hy, by simpa [edist_eq_enorm_sub] using h'y⟩
 
+lemma HasFPowerSeriesWithinOnBall.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F}
+    {s : Set E} {x : E} {r : ℝ≥0∞} (h : HasFPowerSeriesWithinOnBall f p s x r)
+    (h' : EqOn g f (s ∩ Metric.eball x r)) (h'' : g x = f x) :
+    HasFPowerSeriesWithinOnBall g p s x r := by
+  refine h.congr' ?_
+  rintro y ⟨hy, h'y⟩
+  rcases hy with rfl | hy
+  · simpa using h''
+  · exact h' ⟨hy, by simpa [edist_eq_enorm_sub] using h'y⟩
+
 lemma HasFPowerSeriesWithinAt.congr {f g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E}
     {x : E} (h : HasFPowerSeriesWithinAt f p s x) (h' : g =ᶠ[𝓝[s] x] f) (h'' : g x = f x) :
     HasFPowerSeriesWithinAt g p s x := by
diff --git a/Mathlib/Analysis/Analytic/CPolynomialDef.lean b/Mathlib/Analysis/Analytic/CPolynomialDef.lean
index c3d24a71bd6d4e..8234d9144da2db 100644
--- a/Mathlib/Analysis/Analytic/CPolynomialDef.lean
+++ b/Mathlib/Analysis/Analytic/CPolynomialDef.lean
@@ -233,20 +233,16 @@ the ball. -/
 theorem HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_zero
     (hf : HasFiniteFPowerSeriesOnBall f pf x 0 r) : ∀ y ∈ Metric.eball x r, f y = 0 := by
   intro y hy
-  rw [hf.eq_partialSum' y hy 0 le_rfl, FormalMultilinearSeries.partialSum]
-  simp only [Finset.range_zero, Finset.sum_empty]
+  simpa [FormalMultilinearSeries.partialSum] using hf.eq_partialSum' y hy 0 le_rfl
 
 theorem HasFiniteFPowerSeriesOnBall.bound_zero_of_eq_zero (hf : ∀ y ∈ Metric.eball x r, f y = 0)
     (r_pos : 0 < r) (hp : ∀ n, p n = 0) : HasFiniteFPowerSeriesOnBall f p x 0 r := by
-  refine ⟨⟨?_, r_pos, ?_⟩, fun n _ ↦ hp n⟩
-  · rw [p.radius_eq_top_of_forall_image_add_eq_zero 0 (fun n ↦ by rw [add_zero]; exact hp n)]
-    exact le_top
-  · intro y hy
-    rw [hf (x + y)]
-    · convert hasSum_zero
-      rw [hp, ContinuousMultilinearMap.zero_apply]
-    · rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
-        ← edist_zero_right, ← Metric.mem_eball]
+  refine HasFiniteFPowerSeriesOnBall.mk' (fun n _ ↦ hp n) r_pos ?_
+  intro y hy
+  rw [hf (x + y)]
+  · simp
+  · rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
+      ← edist_zero_right, ← Metric.mem_eball]
 
 /-- If `f` has a formal power series at `x` bounded by `0`, then `f` is equal to `0` in a
 neighborhood of `x`. -/
diff --git a/Mathlib/Analysis/Analytic/Composition.lean b/Mathlib/Analysis/Analytic/Composition.lean
index 57015f27b54b07..2a60068e27629c 100644
--- a/Mathlib/Analysis/Analytic/Composition.lean
+++ b/Mathlib/Analysis/Analytic/Composition.lean
@@ -916,12 +916,8 @@ theorem HasFiniteFPowerSeriesAt.comp {m n : ℕ} {g : F → G} {f : E → F}
     contrapose! hi
     rw [← c.sum_blocksFun]
     rcases eq_zero_or_pos c.length with h'c | h'c
-    · have : ∑ j : Fin c.length, c.blocksFun j = 0 := by
-        apply Finset.sum_eq_zero (fun j hj ↦ ?_)
-        have := j.2
-        grind
-      rw [this]
-      exact mul_pos (by grind) hn
+    · have hi0 : i = 0 := (Composition.length_eq_zero (c := c)).1 h'c
+      simpa [hi0, h'c] using mul_pos (Nat.zero_lt_of_lt hc) hn
     · calc ∑ j : Fin c.length, c.blocksFun j
       _ < ∑ j : Fin c.length, n := by
         apply Finset.sum_lt_sum (fun j hj ↦ (hi j).le)
diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean
index 8e4a7cb6769404..99de973b0bb31f 100644
--- a/Mathlib/Analysis/Analytic/Constructions.lean
+++ b/Mathlib/Analysis/Analytic/Constructions.lean
@@ -927,11 +927,8 @@ lemma AnalyticWithinAt.zpow {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ}
 @[to_fun]
 lemma AnalyticAt.zpow {f : E → 𝕝} {z : E} {n : ℤ} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
     AnalyticAt 𝕜 (f ^ n) z := by
-  by_cases hn : 0 ≤ n
-  · exact zpow_nonneg h₁f hn
-  · rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]
-    conv => arg 2; intro x; rw [zpow_neg]
-    exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)
+  rw [← analyticWithinAt_univ] at h₁f ⊢
+  exact h₁f.zpow h₂f
 
 /-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
diff --git a/Mathlib/Analysis/Analytic/ConvergenceRadius.lean b/Mathlib/Analysis/Analytic/ConvergenceRadius.lean
index 06d1363bb19a8e..c171b75623dbde 100644
--- a/Mathlib/Analysis/Analytic/ConvergenceRadius.lean
+++ b/Mathlib/Analysis/Analytic/ConvergenceRadius.lean
@@ -252,17 +252,9 @@ theorem radius_eq_top_of_summable_norm (p : FormalMultilinearSeries 𝕜 E F)
   ENNReal.eq_top_of_forall_nnreal_le fun r => p.le_radius_of_summable_norm (hs r)
 
 theorem radius_eq_top_iff_summable_norm (p : FormalMultilinearSeries 𝕜 E F) :
-    p.radius = ∞ ↔ ∀ r : ℝ≥0, Summable fun n => ‖p n‖ * (r : ℝ) ^ n := by
-  constructor
-  · intro h r
-    obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius
-      (show (r : ℝ≥0∞) < p.radius from h.symm ▸ ENNReal.coe_lt_top)
-    refine .of_norm_bounded
-      (g := fun n ↦ (C : ℝ) * a ^ n) ((summable_geometric_of_lt_one ha.1.le ha.2).mul_left _)
-      fun n ↦ ?_
-    specialize hp n
-    rwa [Real.norm_of_nonneg (by positivity)]
-  · exact p.radius_eq_top_of_summable_norm
+    p.radius = ∞ ↔ ∀ r : ℝ≥0, Summable fun n => ‖p n‖ * (r : ℝ) ^ n :=
+  ⟨fun h _ ↦ p.summable_norm_mul_pow (h.symm ▸ ENNReal.coe_lt_top),
+    p.radius_eq_top_of_summable_norm⟩
 
 /-- If the radius of `p` is positive, then `‖pₙ‖` grows at most geometrically. -/
 theorem le_mul_pow_of_radius_pos (p : FormalMultilinearSeries 𝕜 E F) (h : 0 < p.radius) :
diff --git a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean
index 3800e8c99e9a1f..a82f6110453b2f 100644
--- a/Mathlib/Analysis/Analytic/IteratedFDeriv.lean
+++ b/Mathlib/Analysis/Analytic/IteratedFDeriv.lean
@@ -127,17 +127,9 @@ lemma ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal
   rw [← sum_comp (Equiv.embeddingEquivOfFinite (Fin n))]
   congr with σ
   congr with i
-  have A : ∃ y, σ y = i := by
-    have : Function.Bijective σ := (Fintype.bijective_iff_injective_and_card _).2 ⟨σ.injective, rfl⟩
-    exact this.surjective i
-  rcases A with ⟨y, rfl⟩
-  simp only [EmbeddingLike.apply_eq_iff_eq, exists_eq, ↓reduceDIte,
-    Function.Embedding.toEquivRange_symm_apply_self, ContinuousLinearMap.coe_pi',
-    ContinuousLinearMap.coe_id', id_eq, g]
-  congr 1
-  symm
+  obtain ⟨y, rfl⟩ := σ.equivOfFiniteSelfEmbedding.surjective i
   simp [inv_apply, Perm.inv_def,
-    ofBijective_symm_apply_apply, Function.Embedding.equivOfFiniteSelfEmbedding]
+    ofBijective_symm_apply_apply, Function.Embedding.equivOfFiniteSelfEmbedding, g]
 
 private lemma HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset
     (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s)
diff --git a/Mathlib/Analysis/Analytic/OfScalars.lean b/Mathlib/Analysis/Analytic/OfScalars.lean
index b84df5d936ab81..712002e39cf022 100644
--- a/Mathlib/Analysis/Analytic/OfScalars.lean
+++ b/Mathlib/Analysis/Analytic/OfScalars.lean
@@ -64,15 +64,9 @@ theorem ofScalars_series_of_subsingleton [Subsingleton E] : ofScalars E c = 0 :=
 
 variable (𝕜) in
 theorem ofScalars_series_injective [Nontrivial E] : Function.Injective (ofScalars E (𝕜 := 𝕜)) := by
-  intro _ _
-  refine Function.mtr fun h ↦ ?_
-  simp_rw [FormalMultilinearSeries.ext_iff, ofScalars, ContinuousMultilinearMap.ext_iff,
-    ContinuousMultilinearMap.smul_apply]
-  push Not
-  obtain ⟨n, hn⟩ := Function.ne_iff.1 h
-  refine ⟨n, fun _ ↦ 1, ?_⟩
-  simp only [mkPiAlgebraFin_apply, List.ofFn_const, List.prod_replicate, one_pow, ne_eq]
-  exact (smul_left_injective 𝕜 one_ne_zero).ne hn
+  intro c c' h
+  funext n
+  simpa [ofScalars] using congrArg (fun p => p n fun _ ↦ (1 : E)) h
 
 variable (c)
 
@@ -91,19 +85,16 @@ lemma coeff_ofScalars {𝕜 : Type*} [NontriviallyNormedField 𝕜] {p : ℕ →
     (FormalMultilinearSeries.ofScalars 𝕜 p).coeff n = p n := by
   simp [FormalMultilinearSeries.coeff, FormalMultilinearSeries.ofScalars, List.prod_ofFn]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ofScalars_add (c' : ℕ → 𝕜) : ofScalars E (c + c') = ofScalars E c + ofScalars E c' := by
-  unfold ofScalars
-  simp_rw [Pi.add_apply, Pi.add_def _ _]
-  exact funext fun n ↦ Module.add_smul (c n) (c' n) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)
+  ext n x
+  simp [ofScalars, add_smul]
 
 lemma ofScalars_sub (c' : ℕ → 𝕜) : ofScalars E (c - c') = ofScalars E c - ofScalars E c' := by
   ext; simp [ofScalars, sub_smul]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem ofScalars_smul (x : 𝕜) : ofScalars E (x • c) = x • ofScalars E c := by
-  unfold ofScalars
-  simp [Pi.smul_def x _, smul_smul]
+  ext n y
+  simp [ofScalars, smul_smul]
 
 theorem ofScalars_comp_neg_id :
     (ofScalars E c).compContinuousLinearMap (-ContinuousLinearMap.id _ _) =
diff --git a/Mathlib/Analysis/Analytic/Order.lean b/Mathlib/Analysis/Analytic/Order.lean
index a740430c245744..c90b060fff7703 100644
--- a/Mathlib/Analysis/Analytic/Order.lean
+++ b/Mathlib/Analysis/Analytic/Order.lean
@@ -611,14 +611,9 @@ codiscrete sets.
 theorem preimage_zero_mem_codiscreteWithin {x : 𝕜} (h₁f : AnalyticOnNhd 𝕜 f U) (h₂f : f x ≠ 0)
     (hx : x ∈ U) (hU : IsConnected U) :
     f ⁻¹' {0}ᶜ ∈ codiscreteWithin U := by
-  filter_upwards [h₁f.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top,
-    self_mem_codiscreteWithin U] with a ha h₂a
-  rw [← (h₁f x hx).analyticOrderAt_eq_zero] at h₂f
-  have {u : U} : analyticOrderAt f u ≠ ⊤ := by
-    apply (h₁f.exists_analyticOrderAt_ne_top_iff_forall hU).1
-    use ⟨x, hx⟩
-    simp_all
-  simp_all [(h₁f a h₂a).analyticOrderAt_eq_zero]
+  rcases h₁f.eqOn_zero_or_eventually_ne_zero_of_preconnected hU.isPreconnected with hzero | hne
+  · exact (h₂f (hzero hx)).elim
+  · simpa [Filter.Eventually, Set.mem_setOf_eq] using hne
 
 /--
 If an analytic function `f` is not constantly zero on `𝕜`, then its set of zeros is codiscrete.
diff --git a/Mathlib/Analysis/Analytic/Within.lean b/Mathlib/Analysis/Analytic/Within.lean
index ab7e8a9cbc5fcf..cea3d711a4eb5d 100644
--- a/Mathlib/Analysis/Analytic/Within.lean
+++ b/Mathlib/Analysis/Analytic/Within.lean
@@ -118,16 +118,10 @@ lemma hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall [CompleteSpac
   constructor
   · intro h
     refine ⟨fun y ↦ p.sum (y - x), ?_, ?_⟩
-    · intro y ⟨ys,yb⟩
-      simp only [mem_eball, edist_eq_enorm_sub] at yb
-      have e0 := p.hasSum (x := y - x) ?_
-      · have e1 := (h.hasSum (y := y - x) ?_ ?_)
-        · simp only [add_sub_cancel] at e1
-          exact e1.unique e0
-        · simpa only [add_sub_cancel]
-        · simpa only [mem_eball, edist_zero_right]
-      · simp only [mem_eball, edist_zero_right]
-        exact lt_of_lt_of_le yb h.r_le
+    · rintro y ⟨ys, yb⟩
+      have : f (x + (y - x)) = p.sum (y - x) :=
+        h.sum (y := y - x) (by simpa using ys) (by simpa [edist_eq_enorm_sub] using yb)
+      simpa using this
     · refine ⟨h.r_le, h.r_pos, ?_⟩
       intro y lt
       simp only [add_sub_cancel_left]
@@ -181,19 +175,15 @@ lemma analyticWithinAt_iff_exists_analyticAt' [CompleteSpace F] {f : E → F} {s
   refine ⟨?_, ?_⟩
   · rintro ⟨g, hf, hg⟩
     rcases mem_nhdsWithin.1 hf with ⟨u, u_open, xu, hu⟩
-    let g' := Set.piecewise u g f
-    refine ⟨g', ?_, ?_, ?_⟩
-    · have : x ∈ u ∩ insert x s := ⟨xu, by simp⟩
-      simpa [g', xu, this] using hu this
+    refine ⟨u.piecewise g f, ?_, ?_, ?_⟩
+    · simpa [xu] using hu ⟨xu, by simp⟩
     · intro y hy
       by_cases h'y : y ∈ u
-      · have : y ∈ u ∩ insert x s := ⟨h'y, hy⟩
-        simpa [g', h'y, this] using hu this
-      · simp [g', h'y]
-    · apply hg.congr
-      filter_upwards [u_open.mem_nhds xu] with y hy using by simp [g', hy]
+      · simpa [h'y] using hu ⟨h'y, hy⟩
+      · simp [h'y]
+    · exact hg.congr <| (Set.piecewise_eqOn u g f).symm.eventuallyEq_of_mem (u_open.mem_nhds xu)
   · rintro ⟨g, -, hf, hg⟩
-    exact ⟨g, by filter_upwards [self_mem_nhdsWithin] using hf, hg⟩
+    exact ⟨g, hf.eventuallyEq_of_mem self_mem_nhdsWithin, hg⟩
 
 alias ⟨AnalyticWithinAt.exists_analyticAt, _⟩ := analyticWithinAt_iff_exists_analyticAt'
 
diff --git a/Mathlib/Analysis/AperiodicOrder/Delone/Basic.lean b/Mathlib/Analysis/AperiodicOrder/Delone/Basic.lean
index f3f33a2615c0b3..98bd4bd06faac3 100644
--- a/Mathlib/Analysis/AperiodicOrder/Delone/Basic.lean
+++ b/Mathlib/Analysis/AperiodicOrder/Delone/Basic.lean
@@ -119,14 +119,11 @@ theorem copy_eq (D : DeloneSet X)
 lemma packingRadius_lt_dist_of_mem_ne (D : DeloneSet X) {x y : X}
     (hx : x ∈ D) (hy : y ∈ D) (hne : x ≠ y) :
     D.packingRadius < dist x y := by
-  have hsep : ENNReal.ofReal D.packingRadius < ENNReal.ofReal (dist x y) := by
-    simpa [edist_dist] using D.isSeparated_packingRadius hx hy hne
-  exact (ENNReal.ofReal_lt_ofReal_iff (h := dist_pos.mpr hne)).1 hsep
+  simpa [edist_dist] using D.isSeparated_packingRadius hx hy hne
 
 lemma exists_dist_le_coveringRadius (D : DeloneSet X) (x : X) :
     ∃ y ∈ D, dist x y ≤ D.coveringRadius := by
-  obtain ⟨y, hy, hdist⟩ := D.isCover_coveringRadius (x := x) (by trivial)
-  exact ⟨y, hy, by simpa [edist_dist] using hdist⟩
+  simpa [edist_dist] using D.isCover_coveringRadius (by trivial)
 
 lemma eq_of_mem_ball (D : DeloneSet X) {r : ℝ≥0} (hr : r ≤ D.packingRadius / 2)
     {x y z : X} (hx : x ∈ D) (hy : y ∈ D) (hxz : x ∈ ball z r) (hyz : y ∈ ball z r) :
@@ -170,11 +167,7 @@ lemma mapBilipschitz_trans {Z : Type*} [MetricSpace Z] (D : DeloneSet X)
     D.mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f)
       (mul_pos hf₁_pos hg₁_pos) (mul_pos hg₂_pos hf₂_pos)
       (hg_anti.comp hf_anti) (hg_lip.comp hf_lip) := by
-  ext
-  · simp only [mapBilipschitz_carrier, Equiv.trans_apply, Set.mem_image]
-    exact exists_exists_and_eq_and
-  · simp only [mapBilipschitz_packingRadius, NNReal.coe_div, div_div]
-  · simp only [mapBilipschitz_coveringRadius, NNReal.coe_mul, mul_assoc]
+  (ext <;> simp [mapBilipschitz, Equiv.trans_apply, div_div, mul_assoc]); grind
 
 /-- The image of a Delone set under an isometry. This is a specialization of
 `DeloneSet.mapBilipschitz` where the packing and covering radii are preserved because the
diff --git a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
index da0b9801f78be5..a43601830c924f 100644
--- a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
+++ b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
@@ -118,13 +118,9 @@ theorem isEquivalent_zero_iff_isBigO_zero : u ~[l] 0 ↔ u =O[l] (0 : α → β)
 
 theorem isEquivalent_const_iff_tendsto {c : β} (h : c ≠ 0) :
     u ~[l] const _ c ↔ Tendsto u l (𝓝 c) := by
-  simp +unfoldPartialApp only [IsEquivalent, const, isLittleO_const_iff h]
-  constructor <;> intro h
-  · have := h.sub (tendsto_const_nhds (x := -c))
-    simp only [Pi.sub_apply, sub_neg_eq_add, sub_add_cancel, zero_add] at this
-    exact this
-  · have := h.sub (tendsto_const_nhds (x := c))
-    rwa [sub_self] at this
+  rw [IsEquivalent]
+  change (u - const α c) =o[l] (fun _ : α => c) ↔ Tendsto u l (𝓝 c)
+  simpa [isLittleO_const_iff h] using tendsto_sub_const_iff c (c := c)
 
 theorem IsEquivalent.tendsto_const {c : β} (hu : u ~[l] const _ c) : Tendsto u l (𝓝 c) := by
   rcases em <| c = 0 with rfl | h
@@ -207,16 +203,13 @@ theorem isEquivalent_of_tendsto_one (huv : Tendsto (u / v) l (𝓝 1)) :
 
 theorem isEquivalent_iff_tendsto_one (hz : ∀ᶠ x in l, v x ≠ 0) :
     u ~[l] v ↔ Tendsto (u / v) l (𝓝 1) := by
-  constructor
-  · intro hequiv
-    have := hequiv.isLittleO.tendsto_div_nhds_zero
-    simp only [Pi.sub_apply, sub_div] at this
-    have key : Tendsto (fun x ↦ v x / v x) l (𝓝 1) :=
-      (tendsto_congr' <| hz.mono fun x hnz ↦ @div_self _ _ (v x) hnz).mpr tendsto_const_nhds
-    convert this.add key
-    · simp
-    · simp
-  · exact isEquivalent_of_tendsto_one
+  rw [IsEquivalent, isLittleO_iff_tendsto' (hz.mono fun x hx hx0 => (hx hx0).elim)]
+  change Tendsto (fun x ↦ (u x - v x) / v x) l (𝓝 0) ↔ Tendsto (u / v) l (𝓝 1)
+  have : Tendsto (fun x ↦ (u x - v x) / v x) l (𝓝 0) ↔
+      Tendsto (fun x ↦ u x / v x - 1) l (𝓝 0) :=
+    tendsto_congr' <| hz.mono fun x hx => by simp [sub_div, hx]
+  rw [this]
+  exact tendsto_sub_nhds_zero_iff
 
 end NormedField
 
diff --git a/Mathlib/Analysis/Asymptotics/Defs.lean b/Mathlib/Analysis/Asymptotics/Defs.lean
index 951b910e2a6905..6a6a6ec488e5fd 100644
--- a/Mathlib/Analysis/Asymptotics/Defs.lean
+++ b/Mathlib/Analysis/Asymptotics/Defs.lean
@@ -897,21 +897,17 @@ section
 
 variable (l' : Filter β)
 
-protected theorem IsBigO.comp_fst : f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst) := by
-  simp only [isBigO_iff, eventually_prod_iff]
-  exact fun ⟨c, hc⟩ ↦ ⟨c, _, hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩
+protected theorem IsBigO.comp_fst : f =O[l] g → (f ∘ Prod.fst) =O[l ×ˢ l'] (g ∘ Prod.fst) :=
+  fun h ↦ h.comp_tendsto Filter.tendsto_fst
 
-protected theorem IsBigO.comp_snd : f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd) := by
-  simp only [isBigO_iff, eventually_prod_iff]
-  exact fun ⟨c, hc⟩ ↦ ⟨c, fun _ ↦ True, eventually_true l', _, hc, fun _ ↦ id⟩
+protected theorem IsBigO.comp_snd : f =O[l] g → (f ∘ Prod.snd) =O[l' ×ˢ l] (g ∘ Prod.snd) :=
+  fun h ↦ h.comp_tendsto Filter.tendsto_snd
 
-protected theorem IsLittleO.comp_fst : f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst) := by
-  simp only [isLittleO_iff, eventually_prod_iff]
-  exact fun h _ hc ↦ ⟨_, h hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩
+protected theorem IsLittleO.comp_fst : f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst) :=
+  fun h ↦ h.comp_tendsto Filter.tendsto_fst
 
-protected theorem IsLittleO.comp_snd : f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd) := by
-  simp only [isLittleO_iff, eventually_prod_iff]
-  exact fun h _ hc ↦ ⟨fun _ ↦ True, eventually_true l', _, h hc, fun _ ↦ id⟩
+protected theorem IsLittleO.comp_snd : f =o[l] g → (f ∘ Prod.snd) =o[l' ×ˢ l] (g ∘ Prod.snd) :=
+  fun h ↦ h.comp_tendsto Filter.tendsto_snd
 
 end
 
diff --git a/Mathlib/Analysis/Asymptotics/ExpGrowth.lean b/Mathlib/Analysis/Asymptotics/ExpGrowth.lean
index f66f18c0270adc..cfbdb3e0386540 100644
--- a/Mathlib/Analysis/Asymptotics/ExpGrowth.lean
+++ b/Mathlib/Analysis/Asymptotics/ExpGrowth.lean
@@ -250,25 +250,17 @@ lemma expGrowthSup_inv : expGrowthSup u⁻¹ = - expGrowthInf u := by
 -- `IsBigO` property is spelt out.
 lemma expGrowthInf_le_of_eventually_le (hb : b ≠ ∞) (h : ∀ᶠ n in atTop, u n ≤ b * v n) :
     expGrowthInf u ≤ expGrowthInf v := by
-  apply (expGrowthInf_eventually_monotone h).trans
-  rcases eq_zero_or_pos b with rfl | b_pos
-  · simp only [zero_mul, ← Pi.zero_def, expGrowthInf_zero, bot_le]
-  · apply (expGrowthInf_mul_le _ _).trans_eq <;> rw [expGrowthSup_const b_pos.ne' hb]
-    · exact zero_add (expGrowthInf v)
-    · exact .inl zero_ne_bot
-    · exact .inl zero_ne_top
+  rw [expGrowthInf_def, expGrowthInf_def]
+  exact linearGrowthInf_le_of_eventually_le (u := log ∘ u) (v := log ∘ v) (b := log b) (by simpa) <|
+    h.mono fun n hn ↦ by simpa [Pi.mul_apply, log_mul_add, add_comm] using log_monotone hn
 
 -- Bound on `expGrowthSup` under a `IsBigO` hypothesis. However, `ℝ≥0∞` is not normed, so the
 -- `IsBigO` property is spelt out.
 lemma expGrowthSup_le_of_eventually_le (hb : b ≠ ∞) (h : ∀ᶠ n in atTop, u n ≤ b * v n) :
     expGrowthSup u ≤ expGrowthSup v := by
-  apply (expGrowthSup_eventually_monotone h).trans
-  rcases eq_zero_or_pos b with rfl | b_pos
-  · simp only [zero_mul, ← Pi.zero_def, expGrowthSup_zero, bot_le]
-  · apply (expGrowthSup_mul_le _ _).trans_eq <;> rw [expGrowthSup_const b_pos.ne' hb]
-    · exact zero_add (expGrowthSup v)
-    · exact .inl zero_ne_bot
-    · exact .inl zero_ne_top
+  rw [expGrowthSup_def, expGrowthSup_def]
+  exact linearGrowthSup_le_of_eventually_le (u := log ∘ u) (v := log ∘ v) (b := log b) (by simpa) <|
+    h.mono fun n hn ↦ by simpa [Pi.mul_apply, log_mul_add, add_comm] using log_monotone hn
 
 lemma expGrowthInf_of_eventually_ge (hb : b ≠ 0) (h : ∀ᶠ n in atTop, b * u n ≤ v n) :
     expGrowthInf u ≤ expGrowthInf v := by
diff --git a/Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean b/Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
index 43ba4e5458f0c8..e9d6760992c10a 100644
--- a/Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
+++ b/Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
@@ -44,18 +44,9 @@ open Bornology
 
 theorem Asymptotics.isLittleO_pow_pow_cobounded_of_lt (hpq : p < q) :
     (· ^ p) =o[cobounded R] (· ^ q) := by
-  nontriviality R
-  have noc : NormOneClass R := NormMulClass.toNormOneClass
-  refine IsLittleO.of_bound fun c cpos ↦ ?_
-  rw [← Nat.sub_add_cancel hpq.le]
-  simp_rw [pow_add, norm_mul, norm_pow, eventually_iff_exists_mem]
-  refine ⟨{y | c⁻¹ ≤ ‖y‖ ^ (q - p)}, ?_, fun y my ↦ ?_⟩
-  · have key : Tendsto (‖·‖ ^ (q - p)) (cobounded R) atTop :=
-      (tendsto_pow_atTop (Nat.sub_ne_zero_iff_lt.mpr hpq)).comp tendsto_norm_cobounded_atTop
-    rw [tendsto_atTop] at key
-    exact mem_map.mp (key c⁻¹)
-  · rw [← inv_mul_le_iff₀ cpos]
-    gcongr; exact my
+  rw [← Nat.add_sub_of_le hpq.le]
+  simpa [pow_add] using (isBigO_refl (· ^ p) (cobounded R)).mul_isLittleO
+    ((isLittleO_const_id_cobounded 1).pow (Nat.sub_pos_of_lt hpq))
 
 theorem Asymptotics.isBigO_pow_pow_cobounded_of_le (hpq : p ≤ q) :
     (· ^ p) =O[cobounded R] (· ^ q) := by
diff --git a/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean b/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
index b1001051c200d5..0979ac0f780d5c 100644
--- a/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
+++ b/Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
@@ -158,14 +158,10 @@ variable {l k f}
 
 theorem SuperpolynomialDecay.trans_eventually_abs_le (hf : SuperpolynomialDecay l k f)
     (hfg : abs ∘ g ≤ᶠ[l] abs ∘ f) : SuperpolynomialDecay l k g := by
-  rw [superpolynomialDecay_iff_abs_tendsto_zero] at hf ⊢
-  refine fun z =>
-    tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (hf z)
-      (Eventually.of_forall fun x => abs_nonneg _) (hfg.mono fun x hx => ?_)
-  calc
-    |k x ^ z * g x| = |k x ^ z| * |g x| := abs_mul (k x ^ z) (g x)
-    _ ≤ |k x ^ z| * |f x| := by gcongr _ * ?_; exact hx
-    _ = |k x ^ z * f x| := (abs_mul (k x ^ z) (f x)).symm
+  rw [superpolynomialDecay_iff_superpolynomialDecay_abs] at hf ⊢
+  exact (superpolynomialDecay_zero l (fun a => |k a|)).trans_eventuallyLE
+    (Eventually.of_forall fun x => abs_nonneg (k x)) hf
+    (Eventually.of_forall fun x => abs_nonneg (g x)) hfg
 
 theorem SuperpolynomialDecay.trans_abs_le (hf : SuperpolynomialDecay l k f)
     (hfg : ∀ x, |g x| ≤ |f x|) : SuperpolynomialDecay l k g :=
diff --git a/Mathlib/Analysis/BoxIntegral/Basic.lean b/Mathlib/Analysis/BoxIntegral/Basic.lean
index 907f94655b6723..4a73a24792f489 100644
--- a/Mathlib/Analysis/BoxIntegral/Basic.lean
+++ b/Mathlib/Analysis/BoxIntegral/Basic.lean
@@ -747,12 +747,8 @@ theorem integrable_of_continuousOn [CompleteSpace E] {I : Box ι} {f : ℝⁿ 
     (hc : ContinuousOn f (Box.Icc I)) (μ : Measure ℝⁿ) [IsLocallyFiniteMeasure μ] :
     Integrable.{u, v, v} I l f μ.toBoxAdditive.toSMul := by
   apply integrable_of_bounded_and_ae_continuousWithinAt
-  · obtain ⟨C, hC⟩ := (NormedSpace.isBounded_iff_subset_smul_closedBall ℝ).1
-                        (I.isCompact_Icc.image_of_continuousOn hc).isBounded
-    use ‖C‖, fun x hx ↦ by
-      simpa only [smul_unitClosedBall, mem_closedBall_zero_iff] using hC (Set.mem_image_of_mem f hx)
-  · refine eventually_of_mem ?_ (fun x hx ↦ hc.continuousWithinAt hx)
-    rw [mem_ae_iff, μ.restrict_apply] <;> simp [MeasurableSet.compl_iff.2 I.measurableSet_Icc]
+  · exact I.isCompact_Icc.exists_bound_of_continuousOn hc
+  · exact ae_restrict_of_forall_mem I.measurableSet_Icc fun x hx ↦ hc.continuousWithinAt hx
 
 variable {l}
 
diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean
index 64048745bab0a2..dee1534aca942e 100644
--- a/Mathlib/Analysis/BoxIntegral/Partition/Split.lean
+++ b/Mathlib/Analysis/BoxIntegral/Partition/Split.lean
@@ -187,12 +187,8 @@ theorem sum_split_boxes {M : Type*} [AddCommMonoid M] (I : Box ι) (i : ι) (x :
 /-- If `x ∉ (I.lower i, I.upper i)`, then the hyperplane `{y | y i = x}` does not split `I`. -/
 theorem split_of_notMem_Ioo (h : x ∉ Ioo (I.lower i) (I.upper i)) : split I i x = ⊤ := by
   refine ((isPartitionTop I).eq_of_boxes_subset fun J hJ => ?_).symm
-  rcases mem_top.1 hJ with rfl; clear hJ
-  rw [mem_boxes, mem_split_iff]
-  rw [mem_Ioo, not_and_or, not_lt, not_lt] at h
-  cases h <;> [right; left]
-  · rwa [eq_comm, Box.splitUpper_eq_self]
-  · rwa [eq_comm, Box.splitLower_eq_self]
+  rcases mem_top.1 hJ with rfl
+  grind [Box.splitUpper_eq_self, Box.splitLower_eq_self, mem_boxes, mem_split_iff, not_lt]
 
 theorem coe_eq_of_mem_split_of_mem_le {y : ι → ℝ} (h₁ : J ∈ split I i x) (h₂ : y ∈ J)
     (h₃ : y i ≤ x) : (J : Set (ι → ℝ)) = ↑I ∩ { y | y i ≤ x } := by
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
index 91c04a0b1a975a..dcbf49ddf72e92 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
@@ -256,7 +256,7 @@ lemma toNNReal_smul (r : ℝ≥0) (f : C(X, ℝ)₀) : (r • f).toNNReal = r 
 
 @[simp]
 lemma toNNReal_neg_smul (r : ℝ≥0) (f : C(X, ℝ)₀) : (-(r • f)).toNNReal = r • (-f).toNNReal := by
-  rw [NNReal.smul_def, ← smul_neg, ← NNReal.smul_def, toNNReal_smul]
+  simpa [smul_neg] using (toNNReal_smul (X := X) r (-f))
 
 lemma toNNReal_mul_add_neg_mul_add_mul_neg_eq (f g : C(X, ℝ)₀) :
     ((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) =
diff --git a/Mathlib/Analysis/CStarAlgebra/Unitization.lean b/Mathlib/Analysis/CStarAlgebra/Unitization.lean
index 6e789d584bd5a7..0830c1c2a863ea 100644
--- a/Mathlib/Analysis/CStarAlgebra/Unitization.lean
+++ b/Mathlib/Analysis/CStarAlgebra/Unitization.lean
@@ -169,6 +169,7 @@ instance Unitization.instCStarRing : CStarRing (Unitization 𝕜 E) where
     rw [h₂, h₃]
     /- use the definition of the norm, and split into cases based on whether the norm in the first
     coordinate is bigger or smaller than the norm in the second coordinate. -/
+    -- `grind` works here but is much slower
     by_cases! h : ‖(Unitization.splitMul 𝕜 E x).fst‖ ≤ ‖(Unitization.splitMul 𝕜 E x).snd‖
     · rw [sq, sq, sup_eq_right.mpr h, sup_eq_right.mpr (mul_self_le_mul_self (norm_nonneg _) h)]
     · replace h := h.le
diff --git a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
index b6863131993544..5aad9a30dce5a0 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
@@ -688,11 +688,8 @@ variable (f)
 set, is Borel-measurable. -/
 theorem measurableSet_of_differentiableWithinAt_Ici_of_isComplete {K : Set F} (hK : IsComplete K) :
     MeasurableSet { x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K } := by
-  -- simp [differentiable_set_eq_d K hK, D, measurableSet_b, MeasurableSet.iInter,
-  --   MeasurableSet.iUnion]
   simp only [differentiable_set_eq_D K hK, D]
-  repeat apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter] <;> intro
-  exact measurableSet_B
+  grind [MeasurableSet.iUnion, MeasurableSet.iInter, measurableSet_B]
 
 variable [CompleteSpace F]
 
@@ -877,12 +874,7 @@ theorem measurableSet_of_differentiableAt_of_isComplete_with_param
   rw [this]
   simp only [D, mem_iInter, mem_iUnion]
   simp only [setOf_forall, setOf_exists]
-  refine MeasurableSet.iInter (fun _ ↦ ?_)
-  refine MeasurableSet.iUnion (fun _ ↦ ?_)
-  refine MeasurableSet.iInter (fun _ ↦ ?_)
-  refine MeasurableSet.iInter (fun _ ↦ ?_)
-  refine MeasurableSet.iInter (fun _ ↦ ?_)
-  refine MeasurableSet.iInter (fun _ ↦ ?_)
+  repeat apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter] <;> intro
   have : ProperSpace E := .of_locallyCompactSpace 𝕜
   exact (isOpen_B_with_param hf K).measurableSet
 
diff --git a/Mathlib/Analysis/Complex/CauchyIntegral.lean b/Mathlib/Analysis/Complex/CauchyIntegral.lean
index 75a9ab01cb8d82..fb25951480ffb2 100644
--- a/Mathlib/Analysis/Complex/CauchyIntegral.lean
+++ b/Mathlib/Analysis/Complex/CauchyIntegral.lean
@@ -14,6 +14,7 @@ public import Mathlib.Analysis.Real.Cardinality
 public import Mathlib.MeasureTheory.Integral.CircleIntegral
 public import Mathlib.MeasureTheory.Integral.DivergenceTheorem
 public import Mathlib.MeasureTheory.Measure.Lebesgue.Complex
+public import Mathlib.Topology.Algebra.Module.Cardinality
 
 /-!
 # Cauchy integral formula
@@ -516,19 +517,8 @@ theorem two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_c
     rw [circleIntegral_sub_inv_smul_of_differentiable_on_off_countable_aux hs hz hc hd,
       inv_smul_smul₀]
     simp [Real.pi_ne_zero, I_ne_zero]
-  refine mem_closure_iff_nhds.2 fun t ht => ?_
-  -- TODO: generalize to any vector space over `ℝ`
-  set g : ℝ → ℂ := fun x => w + ofReal x
-  have : Tendsto g (𝓝 0) (𝓝 w) := Continuous.tendsto' (by fun_prop) 0 w (add_zero _)
-  rcases mem_nhds_iff_exists_Ioo_subset.1 (this <| inter_mem ht <| isOpen_ball.mem_nhds hw) with
-    ⟨l, u, hlu₀, hlu_sub⟩
-  obtain ⟨x, hx⟩ : (Ioo l u \ g ⁻¹' s).Nonempty := by
-    refine diff_nonempty.2 fun hsub => ?_
-    have : (Ioo l u).Countable :=
-      (hs.preimage ((add_right_injective w).comp ofReal_injective)).mono hsub
-    rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real (hlu₀.1.trans hlu₀.2)] at this
-    exact this.not_gt Cardinal.aleph0_lt_continuum
-  exact ⟨g x, (hlu_sub hx.1).1, (hlu_sub hx.1).2, hx.2⟩
+  simpa [diff_eq, inter_comm] using
+    (hs.dense_compl (𝕜 := ℝ)).open_subset_closure_inter isOpen_ball hw
 
 /-- **Cauchy integral formula**: if `f : ℂ → E` is continuous on a closed disc of radius `R` and is
 complex differentiable at all but countably many points of its interior, then for any `w` in this
diff --git a/Mathlib/Analysis/Complex/Exponential.lean b/Mathlib/Analysis/Complex/Exponential.lean
index 885cb26e092d48..71a23ba92fdb20 100644
--- a/Mathlib/Analysis/Complex/Exponential.lean
+++ b/Mathlib/Analysis/Complex/Exponential.lean
@@ -505,18 +505,8 @@ lemma norm_exp_sub_sum_le_norm_mul_exp (x : ℂ) (n : ℕ) :
       rw [← mul_sum]
     _ = ‖x‖ ^ n * ∑ m ∈ range (j - n), (‖x‖ ^ m / m.factorial) := by
       congr 1
-      refine (sum_bij (fun m hm ↦ m + n) ?_ ?_ ?_ ?_).symm
-      · grind
-      · intro a ha b hb hab
-        simpa using hab
-      · intro b hb
-        simp only [mem_range, exists_prop]
-        simp only [mem_filter, mem_range] at hb
-        refine ⟨b - n, ?_, ?_⟩
-        · rw [tsub_lt_tsub_iff_right hb.2]
-          exact hb.1
-        · rw [tsub_add_cancel_of_le hb.2]
-      · simp
+      refine sum_nbij' (· - n) (· + n) ?_ ?_ ?_ ?_ ?_ <;>
+        simp +contextual [lt_tsub_iff_right, tsub_add_cancel_of_le]
     _ ≤ ‖x‖ ^ n * Real.exp ‖x‖ := by
       gcongr
       refine Real.sum_le_exp_of_nonneg ?_ _
diff --git a/Mathlib/Analysis/Complex/Hadamard.lean b/Mathlib/Analysis/Complex/Hadamard.lean
index 86c6f1243347e7..d87e22e88eaaad 100644
--- a/Mathlib/Analysis/Complex/Hadamard.lean
+++ b/Mathlib/Analysis/Complex/Hadamard.lean
@@ -311,31 +311,16 @@ def scale (f : ℂ → E) (l u : ℝ) : ℂ → E := fun z ↦ f (l + z • (u -
 lemma scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip {l u : ℝ} (hul : l < u) {z : ℂ}
     (hz : z ∈ verticalClosedStrip 0 1) : l + z * (u - l) ∈ verticalClosedStrip l u := by
   simp only [verticalClosedStrip, mem_preimage, add_re, ofReal_re, mul_re, sub_re, sub_im,
-    ofReal_im, sub_self, mul_zero, sub_zero, mem_Icc, le_add_iff_nonneg_right]
-  simp only [verticalClosedStrip, mem_preimage, mem_Icc] at hz
-  obtain ⟨hz₁, hz₂⟩ := hz
-  simp only [sub_pos, hul, mul_nonneg_iff_of_pos_right, hz₁, true_and]
-  rw [add_comm, ← sub_le_sub_iff_right l, add_sub_assoc, sub_self, add_zero]
-  nth_rewrite 2 [← one_mul (u - l)]
-  have := sub_nonneg.2 hul.le
-  gcongr
+    ofReal_im, sub_self, mul_zero, sub_zero, mem_Icc] at hz ⊢
+  constructor <;> nlinarith [hz.1, hz.2, hul]
 
 /-- The norm of the function `scale f l u` is bounded above on the closed strip `re⁻¹' [0, 1]`. -/
 lemma scale_bddAbove {f : ℂ → E} {l u : ℝ} (hul : l < u)
     (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip l u)) :
     BddAbove ((norm ∘ scale f l u) '' verticalClosedStrip 0 1) := by
-  obtain ⟨R, hR⟩ := bddAbove_def.mp hB
-  rw [bddAbove_def]
-  use R
-  intro r hr
-  obtain ⟨w, hw₁, hw₂, _⟩ := hr
-  simp only [comp_apply, scale, smul_eq_mul]
-  have : ‖f (↑l + w * (↑u - ↑l))‖ ∈ norm ∘ f '' verticalClosedStrip l u := by
-    simp only [comp_apply, mem_image]
-    use ↑l + w * (↑u - ↑l)
-    simp only [and_true]
-    exact scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip hul hw₁
-  exact hR ‖f (↑l + w * (↑u - ↑l))‖ this
+  refine hB.mono ?_
+  rintro _ ⟨z, hz, rfl⟩
+  exact ⟨l + z * (u - l), scale_id_mem_verticalClosedStrip_of_mem_verticalClosedStrip hul hz, rfl⟩
 
 /-- A bound to the norm of `f` on the line `z.re = l` induces a bound to the norm of
   `scale f l u z` on the line `z.re = 0`. -/
diff --git a/Mathlib/Analysis/Complex/Isometry.lean b/Mathlib/Analysis/Complex/Isometry.lean
index 2464ae8171d33a..75a1cff27abb17 100644
--- a/Mathlib/Analysis/Complex/Isometry.lean
+++ b/Mathlib/Analysis/Complex/Isometry.lean
@@ -102,17 +102,12 @@ theorem LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re {f : ℂ →ₗ
 
 theorem LinearIsometry.im_apply_eq_im {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) :
     z + conj z = f z + conj (f z) := by
-  have : ‖f z - 1‖ = ‖z - 1‖ := by rw [← f.norm_map (z - 1), f.map_sub, h]
-  apply_fun fun x => x ^ 2 at this
-  simp only [← normSq_eq_norm_sq] at this
-  rw [← ofReal_inj, ← mul_conj, ← mul_conj] at this
-  rw [map_sub, map_sub] at this
-  simp only [sub_mul, mul_sub, one_mul] at this
-  rw [mul_conj, normSq_eq_norm_sq, LinearIsometry.norm_map] at this
-  rw [mul_conj, normSq_eq_norm_sq] at this
-  simp only [sub_sub, sub_right_inj, mul_one, ofReal_pow, map_one] at this
-  simp only [add_sub, sub_left_inj] at this
-  rw [add_comm, ← this, add_comm]
+  have hdist : ‖f z - 1‖ = ‖z - 1‖ := by simpa [f.map_sub, h] using f.norm_map (z - 1)
+  have hsq : ‖f z - 1‖ ^ 2 = ‖z - 1‖ ^ 2 := congrArg (fun x : ℝ => x ^ 2) hdist
+  rw [← normSq_eq_norm_sq, ← normSq_eq_norm_sq, Complex.normSq_sub, Complex.normSq_sub,
+    normSq_eq_norm_sq, normSq_eq_norm_sq, LinearIsometry.norm_map] at hsq
+  have hre : (f z).re = z.re := by simpa [normSq_eq_norm_sq] using hsq
+  simp [Complex.add_conj, hre]
 
 theorem LinearIsometry.re_apply_eq_re {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) : (f z).re = z.re := by
   apply LinearIsometry.re_apply_eq_re_of_add_conj_eq
diff --git a/Mathlib/Analysis/Complex/OperatorNorm.lean b/Mathlib/Analysis/Complex/OperatorNorm.lean
index 45e5dec65b350e..6ed435f33afd92 100644
--- a/Mathlib/Analysis/Complex/OperatorNorm.lean
+++ b/Mathlib/Analysis/Complex/OperatorNorm.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.Complex.Basic
 public import Mathlib.Analysis.Normed.Operator.NormedSpace
+public import Mathlib.Analysis.RCLike.Lemmas
 public import Mathlib.LinearAlgebra.Complex.Determinant
 
 /-! # The basic continuous linear maps associated to `ℂ`
@@ -34,11 +35,7 @@ theorem linearEquiv_det_conjLIE : LinearEquiv.det conjLIE.toLinearEquiv = -1 :=
   linearEquiv_det_conjAe
 
 @[simp]
-theorem reCLM_norm : ‖reCLM‖ = 1 :=
-  le_antisymm (LinearMap.mkContinuous_norm_le _ zero_le_one _) <|
-    calc
-      1 = ‖reCLM 1‖ := by simp
-      _ ≤ ‖reCLM‖ := unit_le_opNorm _ _ (by simp)
+theorem reCLM_norm : ‖reCLM‖ = 1 := RCLike.reCLM_norm
 
 @[simp]
 theorem reCLM_enorm : ‖reCLM‖ₑ = 1 := by simp [← ofReal_norm]
@@ -62,8 +59,7 @@ theorem imCLM_nnnorm : ‖imCLM‖₊ = 1 :=
   Subtype.ext imCLM_norm
 
 @[simp]
-theorem conjCLE_norm : ‖(conjCLE : ℂ →L[ℝ] ℂ)‖ = 1 :=
-  conjLIE.toLinearIsometry.norm_toContinuousLinearMap
+theorem conjCLE_norm : ‖(conjCLE : ℂ →L[ℝ] ℂ)‖ = 1 := RCLike.conjCLE_norm
 
 @[simp]
 theorem conjCLE_enorm : ‖(conjCLE : ℂ →L[ℝ] ℂ)‖ₑ = 1 := by simp [← ofReal_norm]
@@ -73,8 +69,7 @@ theorem conjCLE_nnorm : ‖(conjCLE : ℂ →L[ℝ] ℂ)‖₊ = 1 :=
   Subtype.ext conjCLE_norm
 
 @[simp]
-theorem ofRealCLM_norm : ‖ofRealCLM‖ = 1 :=
-  ofRealLI.norm_toContinuousLinearMap
+theorem ofRealCLM_norm : ‖ofRealCLM‖ = 1 := RCLike.ofRealCLM_norm
 
 @[simp]
 theorem ofRealCLM_enorm : ‖ofRealCLM‖ₑ = 1 := by simp [← ofReal_norm]
diff --git a/Mathlib/Analysis/Complex/Spectrum.lean b/Mathlib/Analysis/Complex/Spectrum.lean
index 168d635d3eb05a..8abea04b731c9b 100644
--- a/Mathlib/Analysis/Complex/Spectrum.lean
+++ b/Mathlib/Analysis/Complex/Spectrum.lean
@@ -17,13 +17,9 @@ public section
 namespace SpectrumRestricts
 variable {A : Type*} [Ring A]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma real_iff [Algebra ℂ A] {a : A} :
     SpectrumRestricts a Complex.reCLM ↔ ∀ x ∈ spectrum ℂ a, x = x.re := by
-  refine ⟨fun h x hx ↦ ?_, fun h ↦ ?_⟩
-  · obtain ⟨x, -, rfl⟩ := h.algebraMap_image.symm ▸ hx
-    simp
-  · exact .of_subset_range_algebraMap Complex.ofReal_re fun x hx ↦ ⟨x.re, (h x hx).symm⟩
+  simp [spectrumRestricts_iff, Set.LeftInvOn, Function.LeftInverse, eq_comm]
 
 end SpectrumRestricts
 
diff --git a/Mathlib/Analysis/Complex/Trigonometric.lean b/Mathlib/Analysis/Complex/Trigonometric.lean
index 9d95e54fc24346..aed73f44f005ac 100644
--- a/Mathlib/Analysis/Complex/Trigonometric.lean
+++ b/Mathlib/Analysis/Complex/Trigonometric.lean
@@ -501,20 +501,11 @@ theorem tan_sq_div_one_add_tan_sq {x : ℂ} (hx : cos x ≠ 0) :
   simp only [← tan_mul_cos hx, mul_pow, ← inv_one_add_tan_sq hx, div_eq_mul_inv]
 
 theorem cos_three_mul : cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x := by
-  have h1 : x + 2 * x = 3 * x := by ring
-  rw [← h1, cos_add x (2 * x)]
-  simp only [cos_two_mul, sin_two_mul, mul_sub, mul_one, sq]
-  have h2 : 4 * cos x ^ 3 = 2 * cos x * cos x * cos x + 2 * cos x * cos x ^ 2 := by ring
-  rw [h2, cos_sq']
-  ring
+  rw [← cosh_mul_I, mul_assoc, cosh_three_mul, cosh_mul_I]
 
 theorem sin_three_mul : sin (3 * x) = 3 * sin x - 4 * sin x ^ 3 := by
-  have h1 : x + 2 * x = 3 * x := by ring
-  rw [← h1, sin_add x (2 * x)]
-  simp only [cos_two_mul, sin_two_mul, cos_sq']
-  have h2 : cos x * (2 * sin x * cos x) = 2 * sin x * cos x ^ 2 := by ring
-  rw [h2, cos_sq']
-  ring
+  rw [← two_add_one_eq_three, add_one_mul, sin_add (2 * x) x]
+  grind [cos_two_mul, sin_two_mul, cos_sq']
 
 theorem exp_mul_I : exp (x * I) = cos x + sin x * I :=
   (cos_add_sin_I _).symm
diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean
index 3b2730d8745fc2..3bdac1dcc37f1d 100644
--- a/Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean
+++ b/Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean
@@ -119,13 +119,9 @@ lemma σ_im_ne_zero {g z} : (σ g z).im ≠ 0 ↔ z.im ≠ 0 := by
   split_ifs <;> simp
 
 lemma σ_mul (g g' : GL (Fin 2) ℝ) (z : ℂ) : σ (g * g') z = σ g (σ g' z) := by
-  simp only [σ, map_mul, Units.val_mul]
-  rcases g.det_ne_zero.lt_or_gt with (h | h) <;>
-  rcases g'.det_ne_zero.lt_or_gt with (h' | h')
-  · simp [mul_pos_of_neg_of_neg h h', h.not_gt, h'.not_gt]
-  · simp [(mul_neg_of_neg_of_pos h h').not_gt, h.not_gt, h']
-  · simp [(mul_neg_of_pos_of_neg h h').not_gt, h, h'.not_gt]
-  · simp [mul_pos h h', h, h']
+  simp only [σ, map_mul, Units.val_mul, mul_pos_iff]
+  rcases g.det_ne_zero.lt_or_gt with h | h <;> rcases g'.det_ne_zero.lt_or_gt with h' | h' <;>
+    simp [h, h', h.not_gt, h'.not_gt]
 
 lemma σ_mul_comm (g h : GL (Fin 2) ℝ) (z : ℂ) : σ g (σ h z) = σ h (σ g z) := by
   simp only [σ]
@@ -154,13 +150,7 @@ def smulAux (g : GL (Fin 2) ℝ) (z : ℍ) : ℍ :=
 
 lemma denom_cocycle' (g h : GL (Fin 2) ℝ) (z : ℍ) :
     denom (g * h) z = σ h (denom g (smulAux h z)) * denom h z := by
-  simp only [smulAux, smulAux', coe_mk, map_div₀, σ_num, σ_denom, σ_sq]
-  change _ = (_ * (_ / _) + _) * _
-  field_simp [denom_ne_zero h z]
-  simp only [denom, Units.val_mul, mul_apply, Fin.sum_univ_succ, Finset.univ_unique,
-    Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one, Complex.ofReal_add,
-    Complex.ofReal_mul, num]
-  ring
+  simpa [smulAux, smulAux', denom, σ_sq] using denom_cocycle g h z.im_ne_zero
 
 theorem mul_smul' (g h : GL (Fin 2) ℝ) (z : ℍ) :
     smulAux (g * h) z = smulAux g (smulAux h z) := by
diff --git a/Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean b/Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean
index 0d572c9cf9cba0..ce797250e1aab4 100644
--- a/Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean
+++ b/Mathlib/Analysis/Complex/ValueDistribution/CharacteristicFunction.lean
@@ -97,36 +97,6 @@ theorem characteristic_eventually_nonneg :
 ## Behaviour under Arithmetic Operations
 -/
 
-/--
-For `1 ≤ r`, the characteristic function of `f + g` at `⊤` is less than or equal to the sum of the
-characteristic functions of `f` and `g`, respectively, plus `log 2` (where `2` is the number of
-summands).
--/
-theorem characteristic_add_top_le {f₁ f₂ : ℂ → E} {r : ℝ} (h₁f₁ : Meromorphic f₁)
-    (h₁f₂ : Meromorphic f₂) (hr : 1 ≤ r) :
-    characteristic (f₁ + f₂) ⊤ r ≤ characteristic f₁ ⊤ r + characteristic f₂ ⊤ r + log 2 := by
-  simp only [characteristic]
-  calc proximity (f₁ + f₂) ⊤ r + logCounting (f₁ + f₂) ⊤ r
-    _ ≤ (proximity f₁ ⊤ r + proximity f₂ ⊤ r + log 2)
-      + (logCounting f₁ ⊤ r + logCounting f₂ ⊤ r) := by
-      gcongr
-      · apply proximity_add_top_le h₁f₁ h₁f₂
-      · exact logCounting_add_top_le h₁f₁ h₁f₂ hr
-    _ = proximity f₁ ⊤ r + logCounting f₁ ⊤ r + (proximity f₂ ⊤ r + logCounting f₂ ⊤ r)
-      + log 2 := by
-      ring
-
-/--
-Asymptotically, the characteristic function of `f + g` at `⊤` is less than or equal to the sum of
-the characteristic functions of `f` and `g`, respectively.
--/
-theorem characteristic_add_top_eventuallyLE {f₁ f₂ : ℂ → E} (h₁f₁ : Meromorphic f₁)
-    (h₁f₂ : Meromorphic f₂) :
-    characteristic (f₁ + f₂) ⊤
-      ≤ᶠ[Filter.atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ + fun _ ↦ log 2 := by
-  filter_upwards [Filter.eventually_ge_atTop 1] with r hr
-    using characteristic_add_top_le h₁f₁ h₁f₂ hr
-
 /--
 For `1 ≤ r`, the characteristic function of a sum `∑ a, f a` at `⊤` is less than or equal to the sum
 of the characteristic functions of `f ·`, plus `log s.card`.
@@ -156,6 +126,27 @@ theorem characteristic_sum_top_eventuallyLE {α : Type*} (s : Finset α) (f : α
   filter_upwards [Filter.eventually_ge_atTop 1]
     using fun _ hr ↦ characteristic_sum_top_le s f hf hr
 
+/--
+For `1 ≤ r`, the characteristic function of `f + g` at `⊤` is less than or equal to the sum of the
+characteristic functions of `f` and `g`, respectively, plus `log 2` (where `2` is the number of
+summands).
+-/
+theorem characteristic_add_top_le {f₁ f₂ : ℂ → E} {r : ℝ} (h₁f₁ : Meromorphic f₁)
+    (h₁f₂ : Meromorphic f₂) (hr : 1 ≤ r) :
+    characteristic (f₁ + f₂) ⊤ r ≤ characteristic f₁ ⊤ r + characteristic f₂ ⊤ r + log 2 := by
+  simpa using characteristic_sum_top_le Finset.univ ![f₁, f₂] (by simpa using ⟨h₁f₁, h₁f₂⟩) hr
+
+/--
+Asymptotically, the characteristic function of `f + g` at `⊤` is less than or equal to the sum of
+the characteristic functions of `f` and `g`, respectively.
+-/
+theorem characteristic_add_top_eventuallyLE {f₁ f₂ : ℂ → E} (h₁f₁ : Meromorphic f₁)
+    (h₁f₂ : Meromorphic f₂) :
+    characteristic (f₁ + f₂) ⊤
+      ≤ᶠ[Filter.atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ + fun _ ↦ log 2 := by
+  filter_upwards [Filter.eventually_ge_atTop 1] with r hr
+    using characteristic_add_top_le h₁f₁ h₁f₂ hr
+
 /--
 For `1 ≤ r`, the characteristic function for the zeros of `f * g` is less than or equal to the sum
 of the characteristic functions for the zeros of `f` and `g`, respectively.
diff --git a/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Asymptotic.lean b/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Asymptotic.lean
index 2323bd2ca1b3a5..26d186a187df70 100644
--- a/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Asymptotic.lean
+++ b/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Asymptotic.lean
@@ -46,28 +46,13 @@ is little o of the logarithmic counting function attached to `single e`.
 -/
 lemma one_isLittleO_logCounting_single [DecidableEq E] [ProperSpace E] {e : E} :
     (1 : ℝ → ℝ) =o[atTop] logCounting (single e 1) := by
-  rw [isLittleO_iff]
-  intro c hc
-  simp only [Pi.one_apply, norm_eq_abs, eventually_atTop, abs_one]
-  use exp (|log ‖e‖| + c⁻¹)
-  intro b hb
-  have h₁b : 1 ≤ b := by
-    calc 1
-      _ ≤ exp (|log ‖e‖| + c⁻¹) := one_le_exp (by positivity)
-      _ ≤ b := hb
-  have h₁c : ‖e‖ ≤ exp (|log ‖e‖| + c⁻¹) := by
-    calc ‖e‖
-      _ ≤ exp (log ‖e‖) := le_exp_log ‖e‖
-      _ ≤ exp (|log ‖e‖| + c⁻¹) :=
-        exp_monotone (le_add_of_le_of_nonneg (le_abs_self _) (inv_pos.2 hc).le)
-  rw [← inv_mul_le_iff₀ hc, mul_one, abs_of_nonneg (logCounting_nonneg
-    (single_pos.2 Int.one_pos).le h₁b)]
-  calc c⁻¹
-    _ ≤ logCounting (single e 1) (exp (|log ‖e‖| + c⁻¹)) := by
-      simp [logCounting_single_eq_log_sub_const h₁c, le_sub_iff_add_le', le_abs_self (log ‖e‖)]
-    _ ≤ logCounting (single e 1) b := by
-      apply logCounting_mono (single_pos.2 Int.one_pos).le (mem_Ioi.2 (exp_pos _)) _ hb
-      simpa [mem_Ioi] using one_pos.trans_le h₁b
+  have hΘ : (fun r : ℝ ↦ log r - log ‖e‖) =Θ[atTop] log :=
+    (IsEquivalent.refl.sub_isLittleO (Real.isLittleO_const_log_atTop (c := log ‖e‖))).isTheta
+  have h₁ : (1 : ℝ → ℝ) =o[atTop] fun r : ℝ ↦ log r - log ‖e‖ :=
+    (hΘ.isLittleO_congr_right).2 Real.isLittleO_const_log_atTop
+  refine h₁.congr' EventuallyEq.rfl ?_
+  filter_upwards [eventually_ge_atTop ‖e‖] with r hr
+  simp [logCounting_single_eq_log_sub_const hr]
 
 /--
 A non-negative function with locally finite support is zero if and only if its logarithmic counting
@@ -124,16 +109,7 @@ theorem logCounting_isBigO_one_iff_analyticOnNhd {f : 𝕜 → E} (h : Meromorph
     logCounting f ⊤ =O[atTop] (1 : ℝ → ℝ) ↔ AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ := by
   simp only [logCounting, reduceDIte]
   rw [← Function.locallyFinsuppWithin.zero_iff_logCounting_bounded (negPart_nonneg _)]
-  constructor
-  · intro h₁f z hz
-    apply (meromorphicNFOn_toMeromorphicNFOn f univ
-      trivial).meromorphicOrderAt_nonneg_iff_analyticAt.1
-    rw [meromorphicOrderAt_toMeromorphicNFOn h.meromorphicOn (by trivial), ← WithTop.untop₀_nonneg,
-      ← h.meromorphicOn.divisor_apply (by trivial), ← negPart_eq_zero,
-      ← locallyFinsuppWithin.negPart_apply]
-    aesop
-  · intro h₁f
-    rwa [negPart_eq_zero, ← h.meromorphicOn.divisor_of_toMeromorphicNFOn,
-      (meromorphicNFOn_toMeromorphicNFOn _ _).divisor_nonneg_iff_analyticOnNhd]
+  rw [negPart_eq_zero, ← h.meromorphicOn.divisor_of_toMeromorphicNFOn,
+    (meromorphicNFOn_toMeromorphicNFOn _ _).divisor_nonneg_iff_analyticOnNhd]
 
 end ValueDistribution
diff --git a/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean b/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean
index 046f13fb0925fa..af43e219f0e555 100644
--- a/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean
+++ b/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean
@@ -589,13 +589,9 @@ theorem Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_c
     {f : ℂ → ℂ} (h : Meromorphic f) (hR : R ≠ 0) :
     logCounting (divisor f ⊤) R =
       circleAverage (log ‖f ·‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖ := by
-  have h₁f : MeromorphicOn f (closedBall 0 |R|) := by tauto
-  simp only [MeromorphicOn.circleAverage_log_norm hR h₁f, logCounting, top_eq_univ,
-    AddMonoidHom.coe_mk, ZeroHom.coe_mk, zero_sub, norm_neg, add_sub_cancel_right]
-  congr 1
-  · simp_all
-  · rw [divisor_apply, divisor_apply]
-    all_goals aesop
+  rw [eq_sub_iff_add_eq]
+  simpa [logCounting, top_eq_univ, locallyFinsuppWithin.toClosedBall_divisor h] using
+    (MeromorphicOn.circleAverage_log_norm hR (by tauto : MeromorphicOn f (closedBall 0 |R|))).symm
 
 /--
 Variant of `locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const`, using
diff --git a/Mathlib/Analysis/ConstantSpeed.lean b/Mathlib/Analysis/ConstantSpeed.lean
index d7ab627aaaba27..cdc430df5d4d60 100644
--- a/Mathlib/Analysis/ConstantSpeed.lean
+++ b/Mathlib/Analysis/ConstantSpeed.lean
@@ -151,19 +151,16 @@ theorem HasConstantSpeedOnWith.Icc_Icc {x y z : ℝ} (hfs : HasConstantSpeedOnWi
 
 theorem hasConstantSpeedOnWith_zero_iff :
     HasConstantSpeedOnWith f s 0 ↔ ∀ᵉ (x ∈ s) (y ∈ s), edist (f x) (f y) = 0 := by
-  dsimp [HasConstantSpeedOnWith]
-  simp only [zero_mul, ENNReal.ofReal_zero, ← eVariationOn.eq_zero_iff]
+  rw [hasConstantSpeedOnWith_iff_variationOnFromTo_eq]
   constructor
-  · by_contra! ⟨h, hfs⟩
-    simp_rw [ne_eq, eVariationOn.eq_zero_iff] at hfs h
-    push Not at hfs
-    obtain ⟨x, xs, y, ys, hxy⟩ := hfs
-    rcases le_total x y with (xy | yx)
-    · exact hxy (h xs ys x ⟨xs, le_rfl, xy⟩ y ⟨ys, xy, le_rfl⟩)
-    · rw [edist_comm] at hxy
-      exact hxy (h ys xs y ⟨ys, le_rfl, yx⟩ x ⟨xs, yx, le_rfl⟩)
-  · rintro h x _ y _
-    simpa [h] using eVariationOn.mono (s := s) f inter_subset_left
+  · intro ⟨hf, h0⟩ x xs y ys
+    exact variationOnFromTo.edist_zero_of_eq_zero hf xs ys (by simp [h0 xs ys])
+  · intro h
+    have hf : LocallyBoundedVariationOn f s := fun x y xs ys ↦
+      ((eVariationOn.eq_zero_iff f).2 fun a ha b hb ↦ h a ha.1 b hb.1).trans_lt
+        ENNReal.zero_lt_top |>.ne
+    exact ⟨hf, fun x xs y ys ↦ by
+      simpa using (variationOnFromTo.eq_zero_iff hf xs ys).2 fun a ha b hb ↦ h a ha.1 b hb.1⟩
 
 theorem HasConstantSpeedOnWith.ratio {l' : ℝ≥0} (hl' : l' ≠ 0) {φ : ℝ → ℝ} (φm : MonotoneOn φ s)
     (hfφ : HasConstantSpeedOnWith (f ∘ φ) s l) (hf : HasConstantSpeedOnWith f (φ '' s) l') ⦃x : ℝ⦄
@@ -212,14 +209,10 @@ theorem unique_unit_speed_on_Icc_zero {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t)
     EqOn φ id (Icc 0 s) := by
   rw [← φst] at hf
   convert unique_unit_speed φm hfφ hf ⟨le_rfl, hs⟩ using 1
-  have : φ 0 = 0 := by
-    have hm : 0 ∈ φ '' Icc 0 s := by simp only [φst, ht, mem_Icc, le_refl, and_self]
-    obtain ⟨x, xs, hx⟩ := hm
-    apply le_antisymm ((φm ⟨le_rfl, hs⟩ xs xs.1).trans_eq hx) _
-    have := φst ▸ mapsTo_image φ (Icc 0 s)
-    exact (mem_Icc.mp (@this 0 (by rw [mem_Icc]; exact ⟨le_rfl, hs⟩))).1
-  simp only [tsub_zero, this, add_zero]
-  rfl
+  have hφ0 : φ 0 = 0 :=
+    (φm.map_isLeast (isLeast_Icc hs)).unique <| by
+      simpa [φst] using (isLeast_Icc ht : IsLeast (Icc 0 t) 0)
+  exact funext fun y => by simp [hφ0]
 
 /-- The natural parameterization of `f` on `s`, which, if `f` has locally bounded variation on `s`,
 * has unit speed on `s` (by `has_unit_speed_naturalParameterization`).
diff --git a/Mathlib/Analysis/Convex/Basic.lean b/Mathlib/Analysis/Convex/Basic.lean
index 98f83341bcb4f5..8d9aa2b8dfc563 100644
--- a/Mathlib/Analysis/Convex/Basic.lean
+++ b/Mathlib/Analysis/Convex/Basic.lean
@@ -228,15 +228,13 @@ theorem Convex.translate (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun x => z
 
 /-- The translation of a convex set is also convex. -/
 theorem Convex.translate_preimage_right (hs : Convex 𝕜 s) (z : E) :
-    Convex 𝕜 ((fun x => z + x) ⁻¹' s) := by
-  intro x hx y hy a b ha hb hab
-  have h := hs hx hy ha hb hab
-  rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h
+    Convex 𝕜 ((fun x => z + x) ⁻¹' s) :=
+  fun x hx => (hs (show z + x ∈ s from hx)).preimage_add_right
 
 /-- The translation of a convex set is also convex. -/
 theorem Convex.translate_preimage_left (hs : Convex 𝕜 s) (z : E) :
-    Convex 𝕜 ((fun x => x + z) ⁻¹' s) := by
-  simpa only [add_comm] using hs.translate_preimage_right z
+    Convex 𝕜 ((fun x => x + z) ⁻¹' s) :=
+  fun x hx => (hs (show x + z ∈ s from hx)).preimage_add_left
 
 section OrderedAddCommMonoid
 
@@ -468,14 +466,12 @@ theorem Convex.sub (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s -
 variable [AddRightMono 𝕜]
 
 theorem Convex.add_smul_mem (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ s) {t : 𝕜}
-    (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • y ∈ s := by
-  have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> noncomm_ring
-  rw [h]
-  exact hs hx hy (sub_nonneg_of_le ht.2) ht.1 (sub_add_cancel _ _)
+    (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • y ∈ s :=
+  (hs hx).add_smul_mem hy ht.1 ht.2
 
 theorem Convex.smul_mem_of_zero_mem (hs : Convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s)
-    {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : t • x ∈ s := by
-  simpa using hs.add_smul_mem zero_mem (by simpa using hx) ht
+    {t : 𝕜} (ht : t ∈ Icc (0 : 𝕜) 1) : t • x ∈ s :=
+  (hs zero_mem).smul_mem hx ht.1 ht.2
 
 theorem Convex.mapsTo_lineMap (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
     MapsTo (AffineMap.lineMap x y) (Icc (0 : 𝕜) 1) s := by
@@ -486,9 +482,8 @@ theorem Convex.lineMap_mem (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y
   h.mapsTo_lineMap hx hy ht
 
 theorem Convex.add_smul_sub_mem (h : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {t : 𝕜}
-    (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • (y - x) ∈ s := by
-  rw [add_comm]
-  exact h.lineMap_mem hx hy ht
+    (ht : t ∈ Icc (0 : 𝕜) 1) : x + t • (y - x) ∈ s :=
+  (h hx).add_smul_sub_mem hy ht.1 ht.2
 
 end AddCommGroup
 
@@ -550,10 +545,8 @@ theorem convex_iff_div :
   forall₂_congr fun _ _ => starConvex_iff_div
 
 theorem Convex.mem_smul_of_zero_mem (h : Convex 𝕜 s) {x : E} (zero_mem : (0 : E) ∈ s) (hx : x ∈ s)
-    {t : 𝕜} (ht : 1 ≤ t) : x ∈ t • s := by
-  rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']
-  exact h.smul_mem_of_zero_mem zero_mem hx
-    ⟨inv_nonneg.2 (zero_le_one.trans ht), inv_le_one_of_one_le₀ ht⟩
+    {t : 𝕜} (ht : 1 ≤ t) : x ∈ t • s :=
+  (h zero_mem).mem_smul hx ht
 
 theorem Convex.exists_mem_add_smul_eq (h : Convex 𝕜 s) {x y : E} {p q : 𝕜} (hx : x ∈ s) (hy : y ∈ s)
     (hp : 0 ≤ p) (hq : 0 ≤ q) : ∃ z ∈ s, (p + q) • z = p • x + q • y := by
@@ -584,12 +577,8 @@ section
 
 theorem Set.OrdConnected.convex_of_chain [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E]
     [PartialOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E}
-    (hs : s.OrdConnected) (h : IsChain (· ≤ ·) s) : Convex 𝕜 s := by
-  refine convex_iff_segment_subset.mpr fun x hx y hy => ?_
-  obtain hxy | hyx := h.total hx hy
-  · exact (segment_subset_Icc hxy).trans (hs.out hx hy)
-  · rw [segment_symm]
-    exact (segment_subset_Icc hyx).trans (hs.out hy hx)
+    (hs : s.OrdConnected) (h : IsChain (· ≤ ·) s) : Convex 𝕜 s :=
+  fun x hx => hs.starConvex hx fun y hy => show x ≤ y ∨ y ≤ x from h.total hx hy
 
 theorem Set.OrdConnected.convex [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E]
     [IsOrderedAddMonoid E] [Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E} (hs : s.OrdConnected) :
diff --git a/Mathlib/Analysis/Convex/Between.lean b/Mathlib/Analysis/Convex/Between.lean
index fa7552f8864491..479efc2059a7e1 100644
--- a/Mathlib/Analysis/Convex/Between.lean
+++ b/Mathlib/Analysis/Convex/Between.lean
@@ -732,13 +732,8 @@ variable [CommRing R] [PartialOrder R] [IsStrictOrderedRing R]
 variable {R}
 
 theorem Wbtw.sameRay_vsub {x y z : P} (h : Wbtw R x y z) : SameRay R (y -ᵥ x) (z -ᵥ y) := by
-  rcases h with ⟨t, ⟨ht0, ht1⟩, rfl⟩
-  simp_rw [lineMap_apply]
-  rcases ht0.lt_or_eq with (ht0' | rfl); swap; · simp
-  rcases ht1.lt_or_eq with (ht1' | rfl); swap; · simp
-  refine Or.inr (Or.inr ⟨1 - t, t, sub_pos.2 ht1', ht0', ?_⟩)
-  simp only [vadd_vsub, smul_smul, vsub_vadd_eq_vsub_sub, smul_sub, ← sub_smul]
-  ring_nf
+  have h' := sameRay_of_mem_segment ((mem_segment_iff_wbtw).2 (by simpa using h.vsub_const x))
+  simpa [sub_zero, vsub_sub_vsub_cancel_right] using h'
 
 theorem Wbtw.sameRay_vsub_left {x y z : P} (h : Wbtw R x y z) : SameRay R (y -ᵥ x) (z -ᵥ x) := by
   rcases h with ⟨t, ⟨ht0, _⟩, rfl⟩
@@ -1041,17 +1036,7 @@ theorem Sbtw.trans_expand_right {w x y z : P} (h₁ : Sbtw R w x y) (h₂ : Sbtw
 
 omit [IsStrictOrderedRing R] in
 theorem Wbtw.collinear {x y z : P} (h : Wbtw R x y z) : Collinear R ({x, y, z} : Set P) := by
-  rw [collinear_iff_exists_forall_eq_smul_vadd]
-  refine ⟨x, z -ᵥ x, ?_⟩
-  intro p hp
-  simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at hp
-  rcases hp with (rfl | rfl | rfl)
-  · refine ⟨0, ?_⟩
-    simp
-  · rcases h with ⟨t, -, rfl⟩
-    exact ⟨t, rfl⟩
-  · refine ⟨1, ?_⟩
-    simp
+  simpa [Set.insert_comm] using collinear_insert_of_mem_affineSpan_pair h.mem_affineSpan
 
 theorem Collinear.wbtw_or_wbtw_or_wbtw {x y z : P} (h : Collinear R ({x, y, z} : Set P)) :
     Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y := by
@@ -1078,23 +1063,7 @@ theorem Collinear.wbtw_or_wbtw_or_wbtw {x y z : P} (h : Collinear R ({x, y, z} :
       exact Or.inl (wbtw_or_wbtw_smul_vadd_of_nonneg _ _ hy0.le hz0.le)
 
 theorem wbtw_iff_sameRay_vsub {x y z : P} : Wbtw R x y z ↔ SameRay R (y -ᵥ x) (z -ᵥ y) := by
-  refine ⟨Wbtw.sameRay_vsub, fun h => ?_⟩
-  rcases h with (h | h | ⟨r₁, r₂, hr₁, hr₂, h⟩)
-  · rw [vsub_eq_zero_iff_eq] at h
-    simp [h]
-  · rw [vsub_eq_zero_iff_eq] at h
-    simp [h]
-  · refine
-      ⟨r₂ / (r₁ + r₂),
-        ⟨div_nonneg hr₂.le (add_nonneg hr₁.le hr₂.le),
-          div_le_one_of_le₀ (le_add_of_nonneg_left hr₁.le) (add_nonneg hr₁.le hr₂.le)⟩,
-        ?_⟩
-    have h' : z = r₂⁻¹ • r₁ • (y -ᵥ x) +ᵥ y := by simp [h, hr₂.ne']
-    rw [eq_comm]
-    simp only [lineMap_apply, h', vadd_vsub_assoc, smul_smul, ← add_smul, eq_vadd_iff_vsub_eq,
-      smul_add]
-    convert (one_smul R (y -ᵥ x)).symm
-    field
+  simp [← wbtw_vsub_const_iff x, ← mem_segment_iff_wbtw, mem_segment_iff_sameRay]
 
 lemma wbtw_total_of_sameRay_vsub_left {x y z : P} (h : SameRay R (y -ᵥ x) (z -ᵥ x)) :
     Wbtw R x y z ∨ Wbtw R x z y := by
diff --git a/Mathlib/Analysis/Convex/BetweenList.lean b/Mathlib/Analysis/Convex/BetweenList.lean
index 0f1601ba859f89..2ffb1418b3f73e 100644
--- a/Mathlib/Analysis/Convex/BetweenList.lean
+++ b/Mathlib/Analysis/Convex/BetweenList.lean
@@ -180,20 +180,11 @@ variable [Field R] [LinearOrder R] [IsStrictOrderedRing R]
 variable {R}
 
 lemma SortedLE.wbtw {l : List R} (h : l.SortedLE) : l.Wbtw R := by
-  induction l with
-  | nil => simp
-  | cons head tail ih =>
-    rw [wbtw_cons]
-    refine ⟨?_, ih h.pairwise.of_cons.sortedLE⟩
-    clear ih
-    induction tail with
-    | nil => simp
-    | cons head' tail' ih =>
-      rw [pairwise_cons]
-      refine ⟨?_, ih (h.pairwise.sublist ?_).sortedLE⟩
-      · simp_rw [sortedLE_iff_pairwise, pairwise_cons_cons, pairwise_cons] at h
-        exact fun a ha ↦ .of_le_of_le h.1 (h.2.2.1 a ha)
-      · simp
+  rw [List.Wbtw, List.triplewise_iff_getElem]
+  intro i j k hij hjk hk
+  have hik : i < l.length := Nat.lt_trans hij (Nat.lt_trans hjk hk)
+  have hjl : j < l.length := Nat.lt_trans hjk hk
+  exact Wbtw.of_le_of_le (h.getElem_le_getElem_of_le hij.le) (h.getElem_le_getElem_of_le hjk.le)
 
 lemma SortedLT.sbtw {l : List R} (h : l.SortedLT) : l.Sbtw R :=
   ⟨h.sortedLE.wbtw, h.nodup⟩
diff --git a/Mathlib/Analysis/Convex/Birkhoff.lean b/Mathlib/Analysis/Convex/Birkhoff.lean
index 7be75ff975a0dc..2083948fd5b2da 100644
--- a/Mathlib/Analysis/Convex/Birkhoff.lean
+++ b/Mathlib/Analysis/Convex/Birkhoff.lean
@@ -11,7 +11,6 @@ public import Mathlib.Analysis.Convex.Jensen
 public import Mathlib.Analysis.Normed.Module.Convex
 public import Mathlib.Combinatorics.Hall.Basic
 public import Mathlib.Analysis.Convex.DoublyStochasticMatrix
-public import Mathlib.Tactic.Linarith
 
 /-!
 # Birkhoff's theorem
@@ -126,15 +125,11 @@ private lemma doublyStochastic_sum_perm_aux (M : Matrix n n R)
     gcongr
     rw [ssubset_iff_of_subset (monotone_filter_right _ _)]
     · simp_rw [mem_filter_univ, not_not, Prod.exists]
-      refine ⟨i, σ i, hMi'.ne', ?_⟩
-      simp [N, Equiv.toPEquiv_apply]
+      exact ⟨i, σ i, hMi'.ne', by simp [N, Equiv.toPEquiv_apply]⟩
     · rintro ⟨i', j'⟩ _ hN' hM'
-      dsimp at hN' hM'
-      simp only [sub_apply, hM', smul_apply, PEquiv.toMatrix_apply, Equiv.toPEquiv_apply,
-        Option.mem_def, Option.some.injEq, smul_eq_mul, mul_ite, mul_one, mul_zero, zero_sub,
-        neg_eq_zero, ite_eq_right_iff, Classical.not_imp, N] at hN'
-      obtain ⟨rfl, _⟩ := hN'
-      linarith [hi' i' (by simp)]
+      have hσ' : σ i' ≠ j' := by
+        simpa [Equiv.toPEquiv_apply] using hσ i' j' hM'
+      exact hN' <| by simp [N, hM', hσ', Equiv.toPEquiv_apply]
   obtain ⟨w, hw, hw'⟩ := ih _ hd' _ s' hs' this rfl
   refine ⟨w + fun σ' => if σ' = σ then M i (σ i) else 0, ?_⟩
   simp only [Pi.add_apply, add_smul, sum_add_distrib, hw', ite_smul, zero_smul,
diff --git a/Mathlib/Analysis/Convex/Body.lean b/Mathlib/Analysis/Convex/Body.lean
index 0fb195239b33c8..bfddd47b9e9065 100644
--- a/Mathlib/Analysis/Convex/Body.lean
+++ b/Mathlib/Analysis/Convex/Body.lean
@@ -213,19 +213,14 @@ theorem iInter_smul_eq_self [T2Space V] {u : ℕ → ℝ≥0} (K : ConvexBody V)
     ⋂ n : ℕ, (1 + (u n : ℝ)) • (K : Set V) = K := by
   ext x
   refine ⟨fun h => ?_, fun h => ?_⟩
-  · obtain ⟨C, hC_pos, hC_bdd⟩ := K.isBounded.exists_pos_norm_le
-    rw [← K.isClosed.closure_eq, SeminormedAddCommGroup.mem_closure_iff]
-    rw [← NNReal.tendsto_coe, NormedAddCommGroup.tendsto_atTop] at hu
-    intro ε hε
-    obtain ⟨n, hn⟩ := hu (ε / C) (div_pos hε hC_pos)
-    obtain ⟨y, hyK, rfl⟩ := Set.mem_smul_set.mp (Set.mem_iInter.mp h n)
-    refine ⟨y, hyK, ?_⟩
-    rw [show (1 + u n : ℝ) • y - y = (u n : ℝ) • y by rw [add_smul, one_smul, add_sub_cancel_left],
-      norm_smul, Real.norm_eq_abs]
-    specialize hn n le_rfl
-    rw [lt_div_iff₀' hC_pos, mul_comm, NNReal.coe_zero, sub_zero, Real.norm_eq_abs] at hn
-    refine lt_of_le_of_lt ?_ hn
-    gcongr; exact hC_bdd _ hyK
+  · have hu' : Tendsto (fun n ↦ (u n : ℝ)) atTop (𝓝 0) := NNReal.tendsto_coe.2 hu
+    have hx : ∀ᶠ n in atTop, ((1 + (u n : ℝ))⁻¹ : ℝ) • x ∈ (K : Set V) := by
+      refine Filter.Eventually.of_forall fun n => ?_
+      rw [← Set.mem_smul_set_iff_inv_smul_mem₀ (by positivity : (1 + (u n : ℝ)) ≠ 0) (K : Set V) x]
+      exact Set.mem_iInter.mp h n
+    have htx : Tendsto (fun n ↦ ((1 + (u n : ℝ))⁻¹ : ℝ) • x) atTop (𝓝 x) := by
+      simpa using ((tendsto_const_nhds.add hu').inv₀ (by norm_num : (1 + 0 : ℝ) ≠ 0)).smul_const x
+    exact K.isClosed.mem_of_tendsto htx hx
   · refine Set.mem_iInter.mpr (fun n => Convex.mem_smul_of_zero_mem K.convex h_zero h ?_)
     exact le_add_of_nonneg_right (by positivity)
 
diff --git a/Mathlib/Analysis/Convex/Cone/Extension.lean b/Mathlib/Analysis/Convex/Cone/Extension.lean
index ac70c5e315fdc3..576b10b1a409f2 100644
--- a/Mathlib/Analysis/Convex/Cone/Extension.lean
+++ b/Mathlib/Analysis/Convex/Cone/Extension.lean
@@ -121,12 +121,8 @@ theorem exists_top (p : E →ₗ.[ℝ] ℝ) (hp_nonneg : ∀ x : p.domain, (x :
     have hcd : DirectedOn (· ≤ ·) c := c_chain.directedOn
     refine ⟨LinearPMap.sSup c hcd, ?_, fun _ ↦ LinearPMap.le_sSup hcd⟩
     rintro ⟨x, hx⟩ hxs
-    have hdir : DirectedOn (· ≤ ·) (LinearPMap.domain '' c) :=
-      directedOn_image.2 (hcd.mono LinearPMap.domain_mono.monotone)
-    rcases (mem_sSup_of_directed (cne.image _) hdir).1 hx with ⟨_, ⟨f, hfc, rfl⟩, hfx⟩
-    have : f ≤ LinearPMap.sSup c hcd := LinearPMap.le_sSup _ hfc
-    convert ← hcs hfc ⟨x, hfx⟩ hxs using 1
-    exact this.2 rfl
+    obtain ⟨f, hfc, hfx⟩ := (LinearPMap.mem_domain_sSup_iff cne hcd).1 hx
+    simpa [LinearPMap.sSup_apply hcd hfc ⟨x, hfx⟩] using hcs hfc ⟨x, hfx⟩ hxs
   obtain ⟨q, hpq, hqs, hq⟩ := zorn_le_nonempty₀ S hSc p hp_nonneg
   refine ⟨q, hpq, ?_, hqs⟩
   contrapose! hq
diff --git a/Mathlib/Analysis/Convex/Continuous.lean b/Mathlib/Analysis/Convex/Continuous.lean
index 60510a54c5e82e..e09378279c0a53 100644
--- a/Mathlib/Analysis/Convex/Continuous.lean
+++ b/Mathlib/Analysis/Convex/Continuous.lean
@@ -89,22 +89,18 @@ lemma ConvexOn.isBoundedUnder_abs (hf : ConvexOn ℝ C f) {x₀ : E} (hC : C ∈
     (𝓝 x₀).IsBoundedUnder (· ≤ ·) |f| ↔ (𝓝 x₀).IsBoundedUnder (· ≤ ·) f := by
   refine ⟨fun h ↦ h.mono_le <| .of_forall fun x ↦ le_abs_self _, ?_⟩
   rintro ⟨r, hr⟩
-  refine ⟨|r| + 2 * |f x₀|, ?_⟩
-  have : (𝓝 x₀).Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) :=
+  have hflip : (𝓝 x₀).Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) :=
     tendsto_nhds_nhds.2 (⟨·, ·, by simp [two_nsmul, dist_comm]⟩)
-  simp only [Filter.eventually_map, Pi.abs_apply, abs_le'] at hr ⊢
-  filter_upwards [this.eventually_mem hC, hC, hr, this.eventually hr] with y hx hx' hfr hfr'
-  refine ⟨hfr.trans <| (le_abs_self _).trans <| by simp, ?_⟩
-  rw [← sub_le_iff_le_add, neg_sub_comm, sub_le_iff_le_add', ← abs_two, ← abs_mul]
-  calc
-    -|2 * f x₀| ≤ 2 * f x₀ := neg_abs_le _
-    _ ≤ f y + f (2 • x₀ - y) := by
-      have := hf.2 hx' hx (by positivity) (by positivity) (add_halves _)
-      simp only [one_div, ← Nat.cast_smul_eq_nsmul ℝ, Nat.cast_ofNat, smul_sub, ne_eq,
-        OfNat.ofNat_ne_zero, not_false_eq_true, inv_smul_smul₀, add_sub_cancel, smul_eq_mul] at this
-      cancel_denoms at this
-      rwa [← Nat.cast_two, Nat.cast_smul_eq_nsmul] at this
-    _ ≤ f y + |r| := by gcongr; exact hfr'.trans (le_abs_self _)
+  have hge : (𝓝 x₀).IsBoundedUnder (· ≥ ·) f := by
+    refine Filter.isBoundedUnder_of_eventually_ge (a := 2 * f x₀ - |r|) ?_
+    filter_upwards [hflip.eventually_mem hC, hC, hr, hflip.eventually hr] with y hy hy' hfy hfy'
+    have hmid := hf.2 hy' hy (show 0 ≤ (1 / 2 : ℝ) by positivity)
+      (show 0 ≤ (1 / 2 : ℝ) by positivity) (add_halves (1 : ℝ))
+    rw [show (1 / 2 : ℝ) • y + (1 / 2 : ℝ) • (2 • x₀ - y) = x₀ by module] at hmid
+    simp [smul_eq_mul, one_div] at hmid
+    nlinarith [hmid, hfy'.trans (le_abs_self r)]
+  simpa [Pi.abs_def] using
+    (Filter.isBoundedUnder_le_abs (f := 𝓝 x₀) (u := f)).2 ⟨⟨r, hr⟩, hge⟩
 
 lemma ConcaveOn.isBoundedUnder_abs (hf : ConcaveOn ℝ C f) {x₀ : E} (hC : C ∈ 𝓝 x₀) :
     (𝓝 x₀).IsBoundedUnder (· ≤ ·) |f| ↔ (𝓝 x₀).IsBoundedUnder (· ≥ ·) f := by
diff --git a/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean b/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
index 09cae9864a61a1..09f70f5d02342f 100644
--- a/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
+++ b/Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
@@ -277,12 +277,8 @@ theorem mem_adjoint_iff (g : Submodule 𝕜 (E × F)) (x : F × E) :
     LinearEquiv.trans_apply, LinearEquiv.skewSwap_symm_apply, coe_symm_linearEquiv, Prod.exists,
     prod_inner_apply, ofLp_fst, ofLp_snd, forall_exists_index, and_imp, coe_linearEquiv]
   constructor
-  · rintro ⟨y, h1, h2⟩ a b hab
-    rw [← h2, WithLp.ofLp_fst, WithLp.ofLp_snd]
-    specialize h1 (toLp 2 (b, -a)) a b hab rfl
-    dsimp at h1
-    simp only [inner_neg_left, ← sub_eq_add_neg] at h1
-    exact h1
+  · rintro ⟨_, h, rfl⟩ a b hab
+    simpa [sub_eq_add_neg] using h (toLp 2 (b, -a)) a b hab rfl
   · intro h
     refine ⟨toLp 2 x, ?_, rfl⟩
     intro u a b hab hu
@@ -296,19 +292,14 @@ theorem _root_.LinearPMap.adjoint_graph_eq_graph_adjoint (hT : Dense (T.domain :
   simp only [mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left, mem_adjoint_iff,
     forall_exists_index, forall_apply_eq_imp_iff]
   constructor
-  · rintro ⟨hx, h⟩ a ha
-    rw [← h, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩, sub_self]
+  · rintro ⟨hx, hTx⟩ a ha
+    rw [← hTx, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩, sub_self]
   · intro h
-    simp_rw [sub_eq_zero] at h
-    have hx : x.fst ∈ T†.domain := by
-      apply mem_adjoint_domain_of_exists
-      use x.snd
-      rintro ⟨a, ha⟩
-      rw [← inner_conj_symm, ← h a ha, inner_conj_symm]
-    use hx
-    apply hT.eq_of_inner_right 𝕜
-    rintro a ha
-    rw [← h a ha, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩]
+    simp only [sub_eq_zero] at h
+    refine ⟨?_, adjoint_apply_eq hT _ fun a ↦ by
+      rw [← inner_conj_symm, ← h a.1 a.2, inner_conj_symm]⟩
+    exact mem_adjoint_domain_of_exists _ ⟨x.2, fun a ↦ by
+      rw [← inner_conj_symm, ← h a.1 a.2, inner_conj_symm]⟩
 
 @[simp]
 theorem _root_.LinearPMap.graph_adjoint_toLinearPMap_eq_adjoint (hT : Dense (T.domain : Set E)) :
diff --git a/Mathlib/Analysis/Normed/Lp/SmoothApprox.lean b/Mathlib/Analysis/Normed/Lp/SmoothApprox.lean
index db401a5fba0e7a..0859333ff0af25 100644
--- a/Mathlib/Analysis/Normed/Lp/SmoothApprox.lean
+++ b/Mathlib/Analysis/Normed/Lp/SmoothApprox.lean
@@ -97,13 +97,9 @@ theorem _root_.MeasureTheory.Lp.dense_hasCompactSupport_contDiff {p : ℝ≥0∞
   refine (mem_closure_iff_nhds_basis Metric.nhds_basis_closedBall).2 fun ε hε ↦ ?_
   obtain ⟨g, hg₁, hg₂, hg₃⟩ := exist_eLpNorm_sub_le hp hp₂.out (Lp.memLp f) hε
   have hg₄ : MemLp g p μ := hg₂.continuous.memLp_of_hasCompactSupport hg₁
-  use hg₄.toLp
-  use ⟨g, hg₄.coeFn_toLp, hg₁, hg₂⟩
-  rw [Metric.mem_closedBall, dist_comm, Lp.dist_def,
-    ← le_ofReal_iff_toReal_le ((Lp.memLp f).sub (Lp.memLp hg₄.toLp)).eLpNorm_ne_top hε.le]
-  convert hg₃ using 1
-  apply eLpNorm_congr_ae
-  gcongr
-  exact hg₄.coeFn_toLp
+  refine ⟨hg₄.toLp, ⟨g, hg₄.coeFn_toLp, hg₁, hg₂⟩, ?_⟩
+  rw [Metric.mem_closedBall, dist_comm, ← Lp.toLp_coeFn f (Lp.memLp f), Lp.dist_edist,
+    Lp.edist_toLp_toLp _ _ (Lp.memLp f) hg₄]
+  exact ENNReal.toReal_le_of_le_ofReal hε.le hg₃
 
 end MeasureTheory.MemLp
diff --git a/Mathlib/Analysis/Normed/Lp/WithLp.lean b/Mathlib/Analysis/Normed/Lp/WithLp.lean
index 6eaa39716ce974..847baeb70474e4 100644
--- a/Mathlib/Analysis/Normed/Lp/WithLp.lean
+++ b/Mathlib/Analysis/Normed/Lp/WithLp.lean
@@ -177,17 +177,13 @@ end AddCommGroup
 
 @[to_additive]
 instance instIsScalarTower [SMul K K'] [SMul K V] [SMul K' V] [IsScalarTower K K' V] :
-    IsScalarTower K K' (WithLp p V) where
-  smul_assoc x y z := by
-    change toLp p ((x • y) • (ofLp z)) = toLp p (x • y • ofLp z)
-    simp
+    IsScalarTower K K' (WithLp p V) :=
+  (WithLp.equiv p V).isScalarTower K K'
 
 @[to_additive]
 instance instSMulCommClass [SMul K V] [SMul K' V] [SMulCommClass K K' V] :
-    SMulCommClass K K' (WithLp p V) where
-  smul_comm x y z := by
-    change toLp p (x • y • ofLp z) = toLp p (y • x • ofLp z)
-    rw [smul_comm]
+    SMulCommClass K K' (WithLp p V) :=
+  (WithLp.equiv p V).smulCommClass K K'
 
 variable (K V)
 
diff --git a/Mathlib/Analysis/Normed/Lp/lpSpace.lean b/Mathlib/Analysis/Normed/Lp/lpSpace.lean
index 40298d3fbf4fd9..51d46ffa1880ec 100644
--- a/Mathlib/Analysis/Normed/Lp/lpSpace.lean
+++ b/Mathlib/Analysis/Normed/Lp/lpSpace.lean
@@ -1259,17 +1259,8 @@ open scoped Topology uniformity
 
 /-- The coercion from `lp E p` to `∀ i, E i` is uniformly continuous. -/
 theorem uniformContinuous_coe [_i : Fact (1 ≤ p)] :
-    UniformContinuous (α := lp E p) ((↑) : lp E p → ∀ i, E i) := by
-  have hp : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne'
-  rw [uniformContinuous_pi]
-  intro i
-  rw [NormedAddCommGroup.uniformity_basis_dist.uniformContinuous_iff
-    NormedAddCommGroup.uniformity_basis_dist]
-  intro ε hε
-  refine ⟨ε, hε, ?_⟩
-  rintro f g (hfg : ‖f - g‖ < ε)
-  have : ‖f i - g i‖ ≤ ‖f - g‖ := norm_apply_le_norm hp (f - g) i
-  exact this.trans_lt hfg
+    UniformContinuous (α := lp E p) ((↑) : lp E p → ∀ i, E i) :=
+  uniformContinuous_pi.2 fun i => (lipschitzWith_one_eval (E := E) p i).uniformContinuous
 
 variable {ι : Type*} {l : Filter ι} [Filter.NeBot l]
 
diff --git a/Mathlib/Analysis/Normed/Module/Basic.lean b/Mathlib/Analysis/Normed/Module/Basic.lean
index f8ffe68e9838f7..5a1a8224bf56bf 100644
--- a/Mathlib/Analysis/Normed/Module/Basic.lean
+++ b/Mathlib/Analysis/Normed/Module/Basic.lean
@@ -332,12 +332,9 @@ open Filter Bornology in
 @[simp]
 theorem tendsto_algebraMap_cobounded (𝕜 𝕜' : Type*) [NormedField 𝕜] [SeminormedRing 𝕜']
     [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] :
-    Tendsto (algebraMap 𝕜 𝕜') (cobounded 𝕜) (cobounded 𝕜') := by
-  intro c hc
-  rw [mem_map]
-  rw [← isCobounded_def, ← isBounded_compl_iff, isBounded_iff_forall_norm_le] at hc ⊢
-  obtain ⟨s, hs⟩ := hc
-  exact ⟨s, fun x hx ↦ by simpa using hs (algebraMap 𝕜 𝕜' x) hx⟩
+    Tendsto (algebraMap 𝕜 𝕜') (cobounded 𝕜) (cobounded 𝕜') :=
+  ((AddMonoidHomClass.isometry_of_norm (algebraMap 𝕜 𝕜')
+    (norm_algebraMap' (𝕜' := 𝕜'))).antilipschitz).tendsto_cobounded
 
 @[deprecated (since := "2025-11-04")] alias
   algebraMap_cobounded_le_cobounded := tendsto_algebraMap_cobounded
diff --git a/Mathlib/Analysis/Normed/Module/ContinuousInverse.lean b/Mathlib/Analysis/Normed/Module/ContinuousInverse.lean
index 08fe0ab7ababd0..3ca48242396651 100644
--- a/Mathlib/Analysis/Normed/Module/ContinuousInverse.lean
+++ b/Mathlib/Analysis/Normed/Module/ContinuousInverse.lean
@@ -219,11 +219,8 @@ section
 variable [T1Space F]
 
 lemma isClosed_range (hf : f.HasLeftInverse) [IsTopologicalAddGroup F] :
-    IsClosed (range f) := by
-  -- `range f = ker (f ∘ g - id)` is closed since `f ∘ g - id` is continuous.
-  rw [← f.range_toLinearMap, ← f.coe_range,
-    f.range_eq_ker_of_leftInverse (hf.leftInverse_leftInverse)]
-  exact ((f.comp hf.leftInverse) - (ContinuousLinearMap.id R F)).isClosed_ker
+    IsClosed (range f) :=
+  hf.leftInverse_leftInverse.isClosed_range hf.leftInverse.continuous f.continuous
 
 /-- Choice of a closed complement of `range f` -/
 def complement (h : f.HasLeftInverse) : Submodule R F :=
diff --git a/Mathlib/Analysis/Normed/Module/Convex.lean b/Mathlib/Analysis/Normed/Module/Convex.lean
index e2ea87ddaa3fc8..02dfd7f2f6fd4e 100644
--- a/Mathlib/Analysis/Normed/Module/Convex.lean
+++ b/Mathlib/Analysis/Normed/Module/Convex.lean
@@ -182,13 +182,8 @@ theorem isConnected_setOf_sameRay_and_ne_zero {x : E} (hx : x ≠ 0) :
 
 lemma norm_sub_le_of_mem_segment {x y z : E} (hy : y ∈ segment ℝ x z) :
     ‖y - x‖ ≤ ‖z - x‖ := by
-  rw [segment_eq_image'] at hy
-  simp only [mem_image, mem_Icc] at hy
-  obtain ⟨u, ⟨hu_nonneg, hu_le_one⟩, rfl⟩ := hy
-  simp only [add_sub_cancel_left, norm_smul, Real.norm_eq_abs]
-  rw [abs_of_nonneg hu_nonneg]
-  conv_rhs => rw [← one_mul (‖z - x‖)]
-  gcongr
+  simpa [mem_closedBall, dist_eq_norm, dist_comm, norm_sub_rev] using
+    (segment_subset_closedBall_left x z hy)
 
 namespace Filter
 
diff --git a/Mathlib/Analysis/Normed/Module/Dual.lean b/Mathlib/Analysis/Normed/Module/Dual.lean
index 45de9937f53299..063417bde36ea3 100644
--- a/Mathlib/Analysis/Normed/Module/Dual.lean
+++ b/Mathlib/Analysis/Normed/Module/Dual.lean
@@ -117,20 +117,9 @@ theorem polar_closedBall {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [
 
 theorem polar_ball {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ}
     (hr : 0 < r) : StrongDual.polar 𝕜 (ball (0 : E) r) = closedBall (0 : StrongDual 𝕜 E) r⁻¹ := by
-  apply le_antisymm
-  · intro x hx
-    rw [mem_closedBall_zero_iff]
-    apply le_of_forall_gt_imp_ge_of_dense
-    intro a ha
-    rw [← mem_closedBall_zero_iff, ← (mul_div_cancel_left₀ a (Ne.symm (ne_of_lt hr)))]
-    rw [← RCLike.norm_of_nonneg (K := 𝕜) (le_trans zero_le_one
-      (le_of_lt ((inv_lt_iff_one_lt_mul₀' hr).mp ha)))]
-    apply polar_ball_subset_closedBall_div _ hr hx
-    rw [RCLike.norm_of_nonneg (K := 𝕜) (le_trans zero_le_one
-      (le_of_lt ((inv_lt_iff_one_lt_mul₀' hr).mp ha)))]
-    exact (inv_lt_iff_one_lt_mul₀' hr).mp ha
-  · rw [← polar_closedBall hr]
-    exact LinearMap.polar_antitone _ ball_subset_closedBall
+  letI : NormedSpace ℝ E := .restrictScalars ℝ 𝕜 E
+  rw [← polar_closure (𝕜 := 𝕜) (s := ball (0 : E) r), closure_ball (0 : E) hr.ne',
+    polar_closedBall hr]
 
 /-- Given a neighborhood `s` of the origin in a normed space `E`, the dual norms of all elements of
 the polar `polar 𝕜 s` are bounded by a constant. -/
diff --git a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
index ec4bed124b78d8..2cf27c82dbf1b5 100644
--- a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
+++ b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
@@ -259,30 +259,55 @@ theorem ContinuousLinearMap.isOpen_injective [FiniteDimensional 𝕜 E] :
   exact ⟨(K⁻¹ - ‖φ - φ₀‖₊)⁻¹, inv_pos_of_pos (tsub_pos_of_lt hφ),
     H.add_sub_lipschitzWith (φ - φ₀).lipschitz hφ⟩
 
+open ContinuousLinearMap
+
+/-- Continuous linear equivalence between continuous linear functions `𝕜ⁿ → E` and `Eⁿ`.
+The spaces `𝕜ⁿ` and `Eⁿ` are represented as `ι → 𝕜` and `ι → E`, respectively,
+where `ι` is a finite type. -/
+def ContinuousLinearEquiv.piRing (ι : Type*) [Fintype ι] [DecidableEq ι] :
+    ((ι → 𝕜) →L[𝕜] E) ≃L[𝕜] ι → E :=
+  { LinearMap.toContinuousLinearMap.symm.trans (LinearEquiv.piRing 𝕜 E ι 𝕜) with
+    continuous_toFun := by
+      refine continuous_pi fun i => ?_
+      exact (ContinuousLinearMap.apply 𝕜 E (Pi.single i 1)).continuous
+    continuous_invFun := by
+      simp_rw [LinearEquiv.invFun_eq_symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]
+      -- Note: added explicit type and removed `change` that tried to achieve the same
+      refine AddMonoidHomClass.continuous_of_bound
+        (LinearMap.toContinuousLinearMap.toLinearMap.comp
+            (LinearEquiv.piRing 𝕜 E ι 𝕜).symm.toLinearMap)
+        (Fintype.card ι : ℝ) fun g => ?_
+      rw [← nsmul_eq_mul]
+      refine opNorm_le_bound _ (nsmul_nonneg (norm_nonneg g) (Fintype.card ι)) fun t => ?_
+      simp_rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply,
+        LinearMap.coe_toContinuousLinearMap', LinearEquiv.piRing_symm_apply]
+      apply le_trans (norm_sum_le _ _)
+      rw [smul_mul_assoc]
+      refine Finset.sum_le_card_nsmul _ _ _ fun i _ => ?_
+      rw [norm_smul, mul_comm]
+      gcongr <;> apply norm_le_pi_norm }
+
 protected theorem LinearIndependent.eventually {ι} [Finite ι] {f : ι → E}
     (hf : LinearIndependent 𝕜 f) : ∀ᶠ g in 𝓝 f, LinearIndependent 𝕜 g := by
   cases nonempty_fintype ι
   classical
-  simp only [Fintype.linearIndependent_iff'] at hf ⊢
-  rcases LinearMap.exists_antilipschitzWith _ hf with ⟨K, K0, hK⟩
-  have : Tendsto (fun g : ι → E => ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 <| ∑ i, ‖f i - f i‖) :=
-    tendsto_finset_sum _ fun i _ =>
-      Tendsto.norm <| ((continuous_apply i).tendsto _).sub tendsto_const_nhds
-  simp only [sub_self, norm_zero, Finset.sum_const_zero] at this
-  refine (this.eventually (gt_mem_nhds <| inv_pos.2 K0)).mono fun g hg => ?_
-  replace hg : ∑ i, ‖g i - f i‖₊ < K⁻¹ := by
-    rw [← NNReal.coe_lt_coe]
-    push_cast
-    exact hg
-  rw [LinearMap.ker_eq_bot]
-  refine (hK.add_sub_lipschitzWith (LipschitzWith.of_dist_le_mul fun v u => ?_) hg).injective
-  simp only [dist_eq_norm, LinearMap.lsum_apply, Pi.sub_apply, LinearMap.sum_apply,
-    LinearMap.comp_apply, LinearMap.proj_apply, LinearMap.smulRight_apply, LinearMap.id_apply, ←
-    Finset.sum_sub_distrib, ← smul_sub, ← sub_smul, NNReal.coe_sum, coe_nnnorm, Finset.sum_mul]
-  refine norm_sum_le_of_le _ fun i _ => ?_
-  rw [norm_smul, mul_comm]
-  gcongr
-  exact norm_le_pi_norm (v - u) i
+  let e : ((ι → 𝕜) →L[𝕜] E) ≃L[𝕜] ι → E := ContinuousLinearEquiv.piRing (𝕜 := 𝕜) (E := E) ι
+  have hopen : IsOpen {g : ι → E | LinearIndependent 𝕜 g} := by
+    convert
+      ContinuousLinearMap.isOpen_injective (𝕜 := 𝕜) (E := ι → 𝕜) (F := E) |>.preimage
+        e.symm.continuous using 1
+    ext g
+    change LinearIndependent 𝕜 g ↔ Function.Injective ⇑(e.symm g)
+    let L : (ι → 𝕜) →ₗ[𝕜] E :=
+      LinearMap.lsum 𝕜 (fun _ ↦ 𝕜) ℕ fun i ↦ LinearMap.id.smulRight (g i)
+    have hL : (e.symm g : (ι → 𝕜) →L[𝕜] E) = L.toContinuousLinearMap := by
+      ext c
+      change (LinearEquiv.piRing 𝕜 E ι 𝕜).symm g c = _
+      rw [LinearEquiv.piRing_symm_apply]
+      simp [L]
+    rw [show LinearIndependent 𝕜 g ↔ Function.Injective L from Fintype.linearIndependent_iff'ₛ]
+    simp [hL]
+  exact IsOpen.mem_nhds hopen hf
 
 theorem isOpen_setOf_linearIndependent {ι : Type*} [Finite ι] :
     IsOpen { f : ι → E | LinearIndependent 𝕜 f } :=
@@ -355,48 +380,12 @@ end Module.Basis
 
 instance [FiniteDimensional 𝕜 E] [SecondCountableTopology F] :
     SecondCountableTopology (E →L[𝕜] F) := by
-  set d := Module.finrank 𝕜 E
-  suffices
-    ∀ ε > (0 : ℝ), ∃ n : (E →L[𝕜] F) → Fin d → ℕ, ∀ f g : E →L[𝕜] F, n f = n g → dist f g ≤ ε from
-    Metric.secondCountable_of_countable_discretization fun ε ε_pos =>
-      ⟨Fin d → ℕ, by infer_instance, this ε ε_pos⟩
-  intro ε ε_pos
-  obtain ⟨u : ℕ → F, hu : DenseRange u⟩ := exists_dense_seq F
-  let v := Module.finBasis 𝕜 E
-  obtain
-    ⟨C : ℝ, C_pos : 0 < C, hC :
-      ∀ {φ : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ‖φ (v i)‖ ≤ M) → ‖φ‖ ≤ C * M⟩ :=
-    v.exists_opNorm_le (E := E) (F := F)
-  have h_2C : 0 < 2 * C := mul_pos zero_lt_two C_pos
-  have hε2C : 0 < ε / (2 * C) := div_pos ε_pos h_2C
-  have : ∀ φ : E →L[𝕜] F, ∃ n : Fin d → ℕ, ‖φ - (v.constrL <| u ∘ n)‖ ≤ ε / 2 := by
-    intro φ
-    have : ∀ i, ∃ n, ‖φ (v i) - u n‖ ≤ ε / (2 * C) := by
-      simp only [norm_sub_rev]
-      intro i
-      have : φ (v i) ∈ closure (range u) := hu _
-      obtain ⟨n, hn⟩ : ∃ n, ‖u n - φ (v i)‖ < ε / (2 * C) := by
-        rw [mem_closure_iff_nhds_basis Metric.nhds_basis_ball] at this
-        specialize this (ε / (2 * C)) hε2C
-        simpa [dist_eq_norm]
-      exact ⟨n, le_of_lt hn⟩
-    choose n hn using this
-    use n
-    replace hn : ∀ i : Fin d, ‖(φ - (v.constrL <| u ∘ n)) (v i)‖ ≤ ε / (2 * C) := by simp [hn]
-    have : C * (ε / (2 * C)) = ε / 2 := by
-      rw [eq_div_iff (two_ne_zero : (2 : ℝ) ≠ 0), mul_comm, ← mul_assoc,
-        mul_div_cancel₀ _ (ne_of_gt h_2C)]
-    specialize hC (le_of_lt hε2C) hn
-    rwa [this] at hC
-  choose n hn using this
-  set Φ := fun φ : E →L[𝕜] F => v.constrL <| u ∘ n φ
-  simp_rw [← dist_eq_norm] at hn
-  use n
-  intro x y hxy
-  calc
-    dist x y ≤ dist x (Φ x) + dist (Φ x) y := dist_triangle _ _ _
-    _ = dist x (Φ x) + dist y (Φ y) := by simp [Φ, hxy, dist_comm]
-    _ ≤ ε := by linarith [hn x, hn y]
+  let d := Module.finrank 𝕜 E
+  let e₁ : E ≃L[𝕜] Fin d → 𝕜 :=
+    ContinuousLinearEquiv.ofFinrankEq (@Module.finrank_fin_fun 𝕜 _ _ d).symm
+  let e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
+    (e₁.arrowCongr (1 : F ≃L[𝕜] F)).trans (ContinuousLinearEquiv.piRing (Fin d))
+  exact e₂.toHomeomorph.secondCountableTopology
 
 theorem AffineSubspace.closed_of_finiteDimensional {P : Type*} [MetricSpace P]
     [NormedAddTorsor E P] (s : AffineSubspace 𝕜 P) [FiniteDimensional 𝕜 s.direction] :
@@ -510,32 +499,6 @@ end Riesz
 
 open ContinuousLinearMap
 
-/-- Continuous linear equivalence between continuous linear functions `𝕜ⁿ → E` and `Eⁿ`.
-The spaces `𝕜ⁿ` and `Eⁿ` are represented as `ι → 𝕜` and `ι → E`, respectively,
-where `ι` is a finite type. -/
-def ContinuousLinearEquiv.piRing (ι : Type*) [Fintype ι] [DecidableEq ι] :
-    ((ι → 𝕜) →L[𝕜] E) ≃L[𝕜] ι → E :=
-  { LinearMap.toContinuousLinearMap.symm.trans (LinearEquiv.piRing 𝕜 E ι 𝕜) with
-    continuous_toFun := by
-      refine continuous_pi fun i => ?_
-      exact (ContinuousLinearMap.apply 𝕜 E (Pi.single i 1)).continuous
-    continuous_invFun := by
-      simp_rw [LinearEquiv.invFun_eq_symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]
-      -- Note: added explicit type and removed `change` that tried to achieve the same
-      refine AddMonoidHomClass.continuous_of_bound
-        (LinearMap.toContinuousLinearMap.toLinearMap.comp
-            (LinearEquiv.piRing 𝕜 E ι 𝕜).symm.toLinearMap)
-        (Fintype.card ι : ℝ) fun g => ?_
-      rw [← nsmul_eq_mul]
-      refine opNorm_le_bound _ (nsmul_nonneg (norm_nonneg g) (Fintype.card ι)) fun t => ?_
-      simp_rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply,
-        LinearMap.coe_toContinuousLinearMap', LinearEquiv.piRing_symm_apply]
-      apply le_trans (norm_sum_le _ _)
-      rw [smul_mul_assoc]
-      refine Finset.sum_le_card_nsmul _ _ _ fun i _ => ?_
-      rw [norm_smul, mul_comm]
-      gcongr <;> apply norm_le_pi_norm }
-
 /-- A family of continuous linear maps is continuous within `s` at `x` iff all its applications
 are. -/
 theorem continuousWithinAt_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
diff --git a/Mathlib/Analysis/Normed/Module/HahnBanach.lean b/Mathlib/Analysis/Normed/Module/HahnBanach.lean
index 2b067977fae59b..47e3898f6b7201 100644
--- a/Mathlib/Analysis/Normed/Module/HahnBanach.lean
+++ b/Mathlib/Analysis/Normed/Module/HahnBanach.lean
@@ -94,15 +94,11 @@ theorem exists_extension_norm_eq (p : Subspace 𝕜 E) (f : StrongDual 𝕜 p) :
     rw [g.extendRCLike_apply, ← Submodule.coe_smul,
       hextends, hextends]
     simp [fr, RCLike.algebraMap_eq_ofReal, mul_comm I, RCLike.re_add_im]
-  -- And we derive the equality of the norms by bounding on both sides.
-  refine ⟨h, le_antisymm ?_ ?_⟩
-  · calc
-      ‖g.extendRCLike‖ = ‖g‖ := g.norm_extendRCLike
-      _ = ‖fr‖ := hnormeq
-      _ ≤ ‖reCLM‖ * ‖f‖ := ContinuousLinearMap.opNorm_comp_le _ _
-      _ = ‖f‖ := by rw [reCLM_norm, one_mul]
-  · exact f.opNorm_le_bound (g.extendRCLike (𝕜 := 𝕜)).opNorm_nonneg
-      fun x ↦ h x ▸ (g.extendRCLike (𝕜 := 𝕜) |>.le_opNorm x)
+  -- `StrongDual.extendRCLikeₗᵢ` is an isometric equivalence, so the norm is preserved outright.
+  refine ⟨h, by
+    rw [g.norm_extendRCLike, hnormeq]
+    change ‖reCLM.comp (f.restrictScalars ℝ)‖ = ‖f‖
+    exact (StrongDual.extendRCLikeₗᵢ (𝕜 := 𝕜)).symm.norm_map f⟩
 
 open Module
 
diff --git a/Mathlib/Analysis/Normed/Module/MStructure.lean b/Mathlib/Analysis/Normed/Module/MStructure.lean
index 6ab84d6521d7e5..93c2b9e6157737 100644
--- a/Mathlib/Analysis/Normed/Module/MStructure.lean
+++ b/Mathlib/Analysis/Normed/Module/MStructure.lean
@@ -121,18 +121,14 @@ theorem commute [FaithfulSMul M X] {P Q : M} (h₁ : IsLprojection X P) (h₂ :
             have :=
               add_le_add_left (norm_le_insert' (R • x) (R • P • R • x)) (2 • ‖(1 - R) • P • R • x‖)
             simpa only [mul_smul, sub_smul, one_smul] using this
-      rw [ge_iff_le] at e1
-      nth_rewrite 2 [← add_zero ‖R • x‖] at e1
-      rw [add_le_add_iff_left, two_smul, ← two_mul] at e1
-      rw [le_antisymm_iff]
-      refine ⟨?_, norm_nonneg _⟩
-      rwa [← mul_zero (2 : ℝ), mul_le_mul_iff_right₀ (show (0 : ℝ) < 2 by simp)] at e1
+      rw [two_smul] at e1
+      nlinarith [e1, norm_nonneg ((P * R) • x - (R * P * R) • x)]
   have QP_eq_QPQ : Q * P = Q * P * Q := by
-    have e1 : P * (1 - Q) = P * (1 - Q) - (Q * P - Q * P * Q) :=
+    have e1 : Q * P - Q * P * Q = 0 := by
       calc
-        P * (1 - Q) = (1 - Q) * P * (1 - Q) := by rw [PR_eq_RPR (1 - Q) h₂.Lcomplement]
-        _ = P * (1 - Q) - (Q * P - Q * P * Q) := by noncomm_ring
-    rwa [eq_sub_iff_add_eq, add_eq_left, sub_eq_zero] at e1
+        Q * P - Q * P * Q = P * (1 - Q) - (1 - Q) * P * (1 - Q) := by noncomm_ring
+        _ = 0 := sub_eq_zero.mpr (PR_eq_RPR (1 - Q) h₂.Lcomplement)
+    simpa [sub_eq_zero] using e1
   change P * Q = Q * P
   rw [QP_eq_QPQ, PR_eq_RPR Q h₂]
 
diff --git a/Mathlib/Analysis/Normed/Module/MultipliableUniformlyOn.lean b/Mathlib/Analysis/Normed/Module/MultipliableUniformlyOn.lean
index 2151c22bcd0467..bf791ff3f031bb 100644
--- a/Mathlib/Analysis/Normed/Module/MultipliableUniformlyOn.lean
+++ b/Mathlib/Analysis/Normed/Module/MultipliableUniformlyOn.lean
@@ -61,13 +61,9 @@ lemma hasProdUniformlyOn_of_clog (hf : SummableUniformlyOn (fun i x ↦ log (f i
     (hg : BddAbove <| (fun x ↦ (∑' i, log (f i x)).re) '' s) :
     HasProdUniformlyOn f (fun x ↦ ∏' i, f i x) s := by
   simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn]
-  obtain ⟨r, hr⟩ := hf.exists
-  suffices H : TendstoUniformlyOn (fun s x ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s by
-    refine H.congr_right (hr.tsum_eqOn.comp_left.symm.trans ?_)
-    exact fun x hx ↦ (cexp_tsum_eq_tprod (hfn x hx) (hf.summable hx))
-  refine (hr.tendstoUniformlyOn.comp_cexp ?_).congr ?_
-  · simpa +contextual [← hr.tsum_eqOn _] using hg
-  · filter_upwards with s i hi using by simp [exp_sum, fun y ↦ exp_log (hfn i hi y)]
+  refine ((hf.hasSumUniformlyOn.tendstoUniformlyOn.comp_cexp hg).congr ?_).congr_right ?_
+  · filter_upwards with t x hx using by simp [exp_sum, fun y ↦ exp_log (hfn x hx y)]
+  · exact fun x hx ↦ cexp_tsum_eq_tprod (hfn x hx) (hf.summable hx)
 
 lemma multipliableUniformlyOn_of_clog (hf : SummableUniformlyOn (fun i x ↦ log (f i x)) s)
     (hfn : ∀ x ∈ s, ∀ i, f i x ≠ 0)
diff --git a/Mathlib/Analysis/Normed/Module/RieszLemma.lean b/Mathlib/Analysis/Normed/Module/RieszLemma.lean
index 2344fefa388518..9020023265d17f 100644
--- a/Mathlib/Analysis/Normed/Module/RieszLemma.lean
+++ b/Mathlib/Analysis/Normed/Module/RieszLemma.lean
@@ -52,9 +52,7 @@ theorem riesz_lemma {F : Subspace 𝕜 E} (hFc : IsClosed (F : Set E)) (hF : ∃
     obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
     let d := Metric.infDist x F
     have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
-    have hdp : 0 < d :=
-      lt_of_le_of_ne Metric.infDist_nonneg fun heq =>
-        hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
+    have hdp : 0 < d := (hFc.notMem_iff_infDist_pos hFn).1 hx
     let r' := max r 2⁻¹
     have hr' : r' < 1 := by
       simp only [r', max_lt_iff, hr, true_and]
@@ -62,11 +60,7 @@ theorem riesz_lemma {F : Subspace 𝕜 E} (hFc : IsClosed (F : Set E)) (hF : ∃
     have hlt : 0 < r' := lt_of_lt_of_le (by simp) (le_max_right r 2⁻¹)
     have hdlt : d < d / r' := (lt_div_iff₀ hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
     obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt
-    have x_ne_y₀ : x - y₀ ∉ F := by
-      by_contra h
-      have : x - y₀ + y₀ ∈ F := F.add_mem h hy₀F
-      simp only [neg_add_cancel_right, sub_eq_add_neg] at this
-      exact hx this
+    have x_ne_y₀ : x - y₀ ∉ F := by rwa [F.sub_mem_iff_left hy₀F]
     refine ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt ?_⟩
     have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
     calc
diff --git a/Mathlib/Analysis/Normed/Operator/Bilinear.lean b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
index cc211b219e4955..1cfe2be1d895c7 100644
--- a/Mathlib/Analysis/Normed/Operator/Bilinear.lean
+++ b/Mathlib/Analysis/Normed/Operator/Bilinear.lean
@@ -205,14 +205,9 @@ variable (𝕜 E Fₗ Gₗ)
 /-- Flip the order of arguments of a continuous bilinear map.
 This is a version bundled as a `LinearIsometryEquiv`.
 For an unbundled version see `ContinuousLinearMap.flip`. -/
-def flipₗᵢ : (E →L[𝕜] Fₗ →L[𝕜] Gₗ) ≃ₗᵢ[𝕜] Fₗ →L[𝕜] E →L[𝕜] Gₗ where
-  toFun := flip
-  invFun := flip
-  map_add' := flip_add
-  map_smul' := flip_smul
-  left_inv := flip_flip
-  right_inv := flip_flip
-  norm_map' := opNorm_flip
+def flipₗᵢ : (E →L[𝕜] Fₗ →L[𝕜] Gₗ) ≃ₗᵢ[𝕜] Fₗ →L[𝕜] E →L[𝕜] Gₗ :=
+  (flipₗᵢ' E Fₗ Gₗ (RingHom.id 𝕜) (RingHom.id 𝕜) :
+    (E →L[𝕜] Fₗ →L[𝕜] Gₗ) ≃ₗᵢ[𝕜] Fₗ →L[𝕜] E →L[𝕜] Gₗ)
 
 variable {𝕜 E Fₗ Gₗ}
 
diff --git a/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean b/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
index a44502c3cae6be..8e1023910d43e0 100644
--- a/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
+++ b/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
@@ -86,12 +86,8 @@ lemma isBoundedLinearMap_iff {f : E → F} :
 
 theorem IsLinearMap.with_bound {f : E → F} (hf : IsLinearMap 𝕜 f) (M : ℝ)
     (h : ∀ x : E, ‖f x‖ ≤ M * ‖x‖) : IsBoundedLinearMap 𝕜 f :=
-  ⟨hf,
-    by_cases
-      (fun (this : M ≤ 0) =>
-        ⟨1, zero_lt_one, fun x =>
-          (h x).trans <| mul_le_mul_of_nonneg_right (this.trans zero_le_one) (norm_nonneg x)⟩)
-      fun (this : ¬M ≤ 0) => ⟨M, lt_of_not_ge this, h⟩⟩
+  ⟨hf, ⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), fun x =>
+    (h x).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg x)⟩⟩
 
 namespace IsBoundedLinearMap
 
diff --git a/Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean b/Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean
index 5eaecf831a2ed2..46f2e524d34aba 100644
--- a/Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean
+++ b/Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean
@@ -65,21 +65,14 @@ def LinearMap.mkContinuousOfExistsBound (h : ∃ C, ∀ x, ‖f x‖ ≤ C * ‖
 
 theorem continuous_of_linear_of_boundₛₗ {f : E → F} (h_add : ∀ x y, f (x + y) = f x + f y)
     (h_smul : ∀ (c : 𝕜) (x), f (c • x) = σ c • f x) {C : ℝ} (h_bound : ∀ x, ‖f x‖ ≤ C * ‖x‖) :
-    Continuous f :=
-  let φ : E →ₛₗ[σ] F :=
-    { toFun := f
-      map_add' := h_add
-      map_smul' := h_smul }
-  AddMonoidHomClass.continuous_of_bound φ C h_bound
+    Continuous f := by
+  let φ : E →ₛₗ[σ] F := LinearMap.mk ⟨f, h_add⟩ h_smul
+  exact (φ.mkContinuous C h_bound).continuous
 
 theorem continuous_of_linear_of_bound {f : E → G} (h_add : ∀ x y, f (x + y) = f x + f y)
     (h_smul : ∀ (c : 𝕜) (x), f (c • x) = c • f x) {C : ℝ} (h_bound : ∀ x, ‖f x‖ ≤ C * ‖x‖) :
-    Continuous f :=
-  let φ : E →ₗ[𝕜] G :=
-    { toFun := f
-      map_add' := h_add
-      map_smul' := h_smul }
-  AddMonoidHomClass.continuous_of_bound φ C h_bound
+    Continuous f := by
+  simpa using (continuous_of_linear_of_boundₛₗ (σ := RingHom.id 𝕜) h_add h_smul h_bound)
 
 @[simp, norm_cast]
 theorem LinearMap.mkContinuous_coe (C : ℝ) (h : ∀ x, ‖f x‖ ≤ C * ‖x‖) :
@@ -186,11 +179,7 @@ variable {σ₂₁ : 𝕜₂ →+* 𝕜} [RingHomInvPair σ σ₂₁] [RingHomIn
 theorem ContinuousLinearEquiv.homothety_inverse (a : ℝ) (ha : 0 < a) (f : E ≃ₛₗ[σ] F) :
     (∀ x : E, ‖f x‖ = a * ‖x‖) → ∀ y : F, ‖f.symm y‖ = a⁻¹ * ‖y‖ := by
   intro hf y
-  calc
-    ‖f.symm y‖ = a⁻¹ * (a * ‖f.symm y‖) := by
-      rw [← mul_assoc, inv_mul_cancel₀ (ne_of_lt ha).symm, one_mul]
-    _ = a⁻¹ * ‖f (f.symm y)‖ := by rw [hf]
-    _ = a⁻¹ * ‖y‖ := by simp
+  simpa [eq_inv_mul_iff_mul_eq₀ (ne_of_gt ha)] using (hf (f.symm y)).symm
 
 /-- A linear equivalence which is a homothety is a continuous linear equivalence. -/
 noncomputable def ContinuousLinearEquiv.ofHomothety (f : E ≃ₛₗ[σ] F) (a : ℝ) (ha : 0 < a)
diff --git a/Mathlib/Analysis/Normed/Operator/Extend.lean b/Mathlib/Analysis/Normed/Operator/Extend.lean
index 647e36ecb281b3..15638c1fbf6de9 100644
--- a/Mathlib/Analysis/Normed/Operator/Extend.lean
+++ b/Mathlib/Analysis/Normed/Operator/Extend.lean
@@ -118,15 +118,10 @@ theorem opNorm_extend_le (h_dense : DenseRange e) (h_e : ∀ x, ‖x‖ ≤ N *
     ‖f.extend e‖ ≤ N * ‖f‖ := by
   -- Add `opNorm_le_of_dense`?
   refine opNorm_le_bound _ ?_ (isClosed_property h_dense (isClosed_le ?_ (by fun_prop)) fun x ↦ ?_)
-  · cases le_total 0 N with
-    | inl hN => exact mul_nonneg hN (norm_nonneg _)
-    | inr hN =>
-      have : Unique E := ⟨⟨0⟩, fun x ↦ norm_le_zero_iff.mp <|
-        (h_e x).trans (mul_nonpos_of_nonpos_of_nonneg hN (norm_nonneg _))⟩
-      obtain rfl : f = 0 := Subsingleton.elim ..
-      simp
+  · exact mul_nonneg N.2 (norm_nonneg _)
   · exact (cont _).norm
-  · rw [extend_eq _ h_dense (isUniformEmbedding_of_bound _ h_e).isUniformInducing]
+  · rw [extend_eq _ h_dense
+      (ContinuousLinearMap.isUniformEmbedding_of_bound _ h_e).isUniformInducing]
     calc
       ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
       _ ≤ ‖f‖ * (N * ‖e x‖) := by gcongr; exact h_e x
diff --git a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
index 7da83abfe03fff..d72c6757a382ad 100644
--- a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
+++ b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
@@ -486,13 +486,7 @@ theorem toLinearEquiv_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toLinearEqui
 instance instEquivLike : EquivLike (E ≃ₛₗᵢ[σ₁₂] E₂) E E₂ where
   coe e := e.toFun
   inv e := e.invFun
-  coe_injective' f g h₁ h₂ := by
-    obtain ⟨f', _⟩ := f
-    obtain ⟨g', _⟩ := g
-    cases f'
-    cases g'
-    simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, DFunLike.coe_fn_eq] at h₁
-    congr
+  coe_injective' _ _ h _ := toLinearEquiv_injective <| DFunLike.ext' h
   left_inv e := e.left_inv
   right_inv e := e.right_inv
 
diff --git a/Mathlib/Analysis/Normed/Operator/Mul.lean b/Mathlib/Analysis/Normed/Operator/Mul.lean
index a7a789021e55a6..4ed36b9561d0f8 100644
--- a/Mathlib/Analysis/Normed/Operator/Mul.lean
+++ b/Mathlib/Analysis/Normed/Operator/Mul.lean
@@ -158,24 +158,15 @@ variable (𝕜 E)
 
 /-- If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly equivalent
 to `M`. (See `ring_lmap_equiv_self` for a stronger statement.) -/
-def ring_lmap_equiv_selfₗ : (𝕜 →L[𝕜] E) ≃ₗ[𝕜] E where
-  toFun := fun f ↦ f 1
-  invFun := (ContinuousLinearMap.id 𝕜 𝕜).smulRight
-  map_smul' := fun a f ↦ by simp only [coe_smul', Pi.smul_apply, RingHom.id_apply]
-  map_add' := fun f g ↦ by simp only [add_apply]
-  left_inv := fun f ↦ by ext; simp only [smulRight_apply, coe_id', _root_.id, one_smul]
-  right_inv := fun m ↦ by simp only [smulRight_apply, id_apply, one_smul]
+def ring_lmap_equiv_selfₗ : (𝕜 →L[𝕜] E) ≃ₗ[𝕜] E :=
+  (ContinuousLinearMap.toSpanSingletonLE 𝕜 𝕜 E).symm
 
 /-- If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly isometrically
 equivalent to `M`. -/
 def ring_lmap_equiv_self : (𝕜 →L[𝕜] E) ≃ₗᵢ[𝕜] E where
   toLinearEquiv := ring_lmap_equiv_selfₗ 𝕜 E
-  norm_map' := by
-    refine fun f ↦ le_antisymm ?_ ?_
-    · simpa only [norm_one, mul_one] using le_opNorm f 1
-    · refine opNorm_le_bound' f (norm_nonneg <| f 1) (fun x _ ↦ ?_)
-      rw [(by rw [smul_eq_mul, mul_one] : f x = f (x • 1)), map_smul,
-        norm_smul, mul_comm, (by rfl : ring_lmap_equiv_selfₗ 𝕜 E f = f 1)]
+  norm_map' f := by
+    simpa using (ContinuousLinearMap.norm_toSpanSingleton (𝕜 := 𝕜) (x := f 1)).symm
 
 end RingEquiv
 
diff --git a/Mathlib/Analysis/Normed/Operator/NNNorm.lean b/Mathlib/Analysis/Normed/Operator/NNNorm.lean
index a2353bc31cbb66..61b458e39c8318 100644
--- a/Mathlib/Analysis/Normed/Operator/NNNorm.lean
+++ b/Mathlib/Analysis/Normed/Operator/NNNorm.lean
@@ -181,14 +181,9 @@ theorem sSup_unitClosedBall_eq_norm (f : E →SL[σ₁₂] F) :
 theorem exists_nnnorm_eq_one_lt_apply_of_lt_opNNNorm [NormedAlgebra ℝ 𝕜]
     (f : E →SL[σ₁₂] F) {r : ℝ≥0} (hr : r < ‖f‖₊) :
     ∃ x : E, ‖x‖₊ = 1 ∧ r < ‖f x‖₊ := by
-  obtain ⟨x, hlt, hr⟩ := exists_lt_apply_of_lt_opNNNorm f hr
-  obtain rfl | hx0 := eq_zero_or_nnnorm_pos x
-  · simp at hr
-  use algebraMap ℝ 𝕜 ‖x‖⁻¹ • x
-  suffices r < ‖x‖₊⁻¹ * ‖f x‖₊ by simpa [nnnorm_smul, inv_mul_cancel₀ hx0.ne'] using this
-  calc
-    r < 1⁻¹ * ‖f x‖₊ := by simpa
-    _ < ‖x‖₊⁻¹ * ‖f x‖₊ := by gcongr; exact (zero_le r).trans_lt hr
+  by_contra h
+  push Not at h
+  exact not_lt_of_ge (opNNNorm_le_of_unit_nnnorm h) hr
 
 /-- When the domain is a real normed space, `ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm` can
 be tightened to take the supremum over only the `Metric.sphere`. -/
diff --git a/Mathlib/Analysis/Normed/Ring/Basic.lean b/Mathlib/Analysis/Normed/Ring/Basic.lean
index 47955ce9681e21..5631689976de81 100644
--- a/Mathlib/Analysis/Normed/Ring/Basic.lean
+++ b/Mathlib/Analysis/Normed/Ring/Basic.lean
@@ -943,10 +943,6 @@ variable {R ι ι' : Type*} [Semiring R] [Finite ι] [Finite ι']
 lemma iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg {F : Type*} [FunLike F R ℝ]
     [NonnegHomClass F R ℝ] [MulHomClass F R ℝ] (v : F) (x : ι → R) (y : ι' → R) :
     ⨆ a : ι × ι', v (x a.1 * y a.2) = (⨆ i, v (x i)) * ⨆ j, v (y j) := by
-  rcases isEmpty_or_nonempty ι
-  · simp
-  rcases isEmpty_or_nonempty ι'
-  · simp
   simp_rw [Real.iSup_mul_of_nonneg (iSup_nonneg fun i ↦ apply_nonneg v (y i)),
     Real.mul_iSup_of_nonneg (apply_nonneg v _), map_mul, Finite.ciSup_prod]
 
diff --git a/Mathlib/Analysis/Normed/Ring/Lemmas.lean b/Mathlib/Analysis/Normed/Ring/Lemmas.lean
index a775053172d046..fc9b48ce9054cb 100644
--- a/Mathlib/Analysis/Normed/Ring/Lemmas.lean
+++ b/Mathlib/Analysis/Normed/Ring/Lemmas.lean
@@ -9,6 +9,7 @@ public import Mathlib.Algebra.Order.GroupWithZero.Finset
 public import Mathlib.Analysis.Normed.Group.Bounded
 public import Mathlib.Analysis.Normed.Group.Int
 public import Mathlib.Analysis.Normed.Group.Uniform
+public import Mathlib.Analysis.Normed.MulAction
 public import Mathlib.Analysis.Normed.Ring.Basic
 public import Mathlib.Topology.MetricSpace.Dilation
 
@@ -157,22 +158,7 @@ end NormedCommRing
 -- see Note [lower instance priority]
 instance (priority := 100) NonUnitalSeminormedRing.toContinuousMul [NonUnitalSeminormedRing α] :
     ContinuousMul α :=
-  ⟨continuous_iff_continuousAt.2 fun x =>
-      tendsto_iff_norm_sub_tendsto_zero.2 <| by
-        have : ∀ e : α × α,
-            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ := by
-          intro e
-          calc
-            ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
-              rw [mul_sub, sub_mul, sub_add_sub_cancel]
-            _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
-              norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
-        refine squeeze_zero (fun e => norm_nonneg _) this ?_
-        convert
-          ((continuous_fst.tendsto x).norm.mul
-                ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm).add
-            (((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul tendsto_const_nhds)
-        simp⟩
+  ⟨show Continuous fun p : α × α => p.1 • p.2 from continuous_smul⟩
 
 -- see Note [lower instance priority]
 /-- A seminormed ring is a topological ring. -/
@@ -228,7 +214,7 @@ instance Int.instNormOneClass : NormOneClass ℤ :=
   ⟨by simp [← Int.norm_cast_real]⟩
 
 instance Int.instNormMulClass : NormMulClass ℤ :=
-  ⟨fun a b ↦ by simp [← Int.norm_cast_real, abs_mul]⟩
+  ⟨fun a b ↦ by simp [← Int.norm_cast_real]⟩
 
 section NonUnitalNormedRing
 variable [NonUnitalNormedRing α] [NormMulClass α] {a : α}
diff --git a/Mathlib/Analysis/Normed/Unbundled/AlgebraNorm.lean b/Mathlib/Analysis/Normed/Unbundled/AlgebraNorm.lean
index fe5e0f748292e6..eafa8a4c0d88bf 100644
--- a/Mathlib/Analysis/Normed/Unbundled/AlgebraNorm.lean
+++ b/Mathlib/Analysis/Normed/Unbundled/AlgebraNorm.lean
@@ -214,12 +214,8 @@ variable {R : Type*} [NonAssocRing R]
 set_option linter.style.whitespace false in -- manual alignment is not recognised
 /-- The ring norm underlying a multiplicative ring norm. -/
 def toRingNorm (f : MulRingNorm R) : RingNorm R where
-  toFun       := f
-  map_zero'   := f.map_zero'
-  add_le'     := f.add_le'
-  neg'        := f.neg'
+  __ := f
   mul_le' x y := le_of_eq (f.map_mul' x y)
-  eq_zero_of_map_eq_zero' := f.eq_zero_of_map_eq_zero'
 
 /-- A multiplicative ring norm is power-multiplicative. -/
 theorem isPowMul {A : Type*} [Ring A] (f : MulRingNorm A) : IsPowMul f := fun x n hn => by
diff --git a/Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean b/Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean
index 9c5736d180782e..752e6be1670a13 100644
--- a/Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean
+++ b/Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean
@@ -153,21 +153,11 @@ theorem norm_mul_le_const_mul_norm {i : ι} (hBi : B i = (1 : L))
 theorem norm_smul {ι : Type*} [Fintype ι] [Nonempty ι] {B : Basis ι K L} {i : ι}
     (hBi : B i = (1 : L)) (k : K) (y : L) :
     B.norm ((algebraMap K L) k * y) = B.norm ((algebraMap K L) k) * B.norm y := by
-  by_cases hk : k = 0
-  · rw [hk, map_zero, zero_mul, B.norm_zero, zero_mul]
-  · rw [norm_extends hBi]
-    obtain ⟨i, _, hi⟩ := exists_mem_eq_sup' univ_nonempty (fun i ↦ ‖B.repr y i‖)
-    obtain ⟨j, _, hj⟩ := exists_mem_eq_sup' univ_nonempty
-      (fun i ↦ ‖B.repr ((algebraMap K L) k * y) i‖)
-    have hij : ‖B.repr y i‖ = ‖B.repr y j‖ := by
-      rw [← hi]
-      apply le_antisymm _ (norm_repr_le_norm B j)
-      have hj' := Finset.le_sup' (fun i ↦ ‖B.repr ((algebraMap K L) k * y) i‖) (mem_univ i)
-      simp only [repr_smul', norm_mul, ← hi] at hj hj'
-      exact (mul_le_mul_iff_right₀ (lt_of_le_of_ne (norm_nonneg _)
-        (Ne.symm (norm_ne_zero_iff.mpr hk)))).mp (hj ▸ hj')
-    simp only [norm, hj]
-    rw [repr_smul', norm_mul, hi, hij]
+  rw [norm_extends hBi, Basis.norm, Basis.norm]
+  rw [Finset.mul₀_sup' (ha := norm_nonneg _) (f := fun j : ι ↦ ‖B.repr y j‖) (s := univ)
+    (hs := univ_nonempty)]
+  congr with j
+  rw [repr_smul', norm_mul]
 
 end Module.Basis
 
diff --git a/Mathlib/Analysis/Normed/Unbundled/SeminormFromBounded.lean b/Mathlib/Analysis/Normed/Unbundled/SeminormFromBounded.lean
index 93fd45b5db61ff..73d659d794abad 100644
--- a/Mathlib/Analysis/Normed/Unbundled/SeminormFromBounded.lean
+++ b/Mathlib/Analysis/Normed/Unbundled/SeminormFromBounded.lean
@@ -212,13 +212,9 @@ theorem seminormFromBounded_one (f_ne_zero : f ≠ 0) (f_nonneg : 0 ≤ f)
     · rw [hx, div_zero]; exact zero_le_one
     · rw [div_self hx]
   · rw [← div_self (map_one_ne_zero f_ne_zero f_nonneg f_mul)]
-    have h_bdd : BddAbove (Set.range fun y ↦ f y / f y) := by
-      use (1 : ℝ)
-      rintro r ⟨y, rfl⟩
-      by_cases hy : f y = 0
-      · simp only [hy, div_zero, zero_le_one]
-      · simp only [div_self hy, le_refl]
-    exact le_ciSup h_bdd (1 : R)
+    exact le_ciSup
+      (by simpa [one_mul] using seminormFromBounded_bddAbove_range f_nonneg f_mul (1 : R))
+      (1 : R)
 
 /-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then
   `seminormFromBounded' f 1 ≤ 1`. -/
@@ -332,11 +328,7 @@ theorem seminormFromBounded_of_mul_le (f_nonneg : 0 ≤ f) {x : R}
 theorem seminormFromBounded_nonzero (f_ne_zero : f ≠ 0) (f_nonneg : 0 ≤ f)
     (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) :
     seminormFromBounded' f ≠ 0 := by
-  obtain ⟨x, hx⟩ := Function.ne_iff.mp f_ne_zero
-  rw [Function.ne_iff]
-  use x
-  rw [ne_eq, Pi.zero_apply, seminormFromBounded_eq_zero_iff f_nonneg f_mul x]
-  exact hx
+  simpa [Function.ne_iff, seminormFromBounded_eq_zero_iff f_nonneg f_mul] using f_ne_zero
 
 /-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then the kernel of
   `seminormFromBounded' f` equals the kernel of `f`. -/
diff --git a/Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean b/Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean
index 8131a0a5890ab7..aca33dc755c3d5 100644
--- a/Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean
+++ b/Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean
@@ -151,10 +151,8 @@ def seminormFromConst : RingSeminorm R where
   mul_le' x y := by
     have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x * y) (2 * n)) atTop
         (𝓝 (seminormFromConst' c f (x * y))) := by
-      apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x * y)).comp
-        (tendsto_atTop_atTop_of_monotone (fun _ _ hnm ↦ by
-          simp only [mul_le_mul_iff_right₀, Nat.succ_pos', hnm]) _)
-      · rintro n; use n; lia
+      exact (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x * y)).comp
+        (tendsto_id.const_mul_atTop' zero_lt_two)
     refine le_of_tendsto_of_tendsto' hlim ((tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).mul
       (tendsto_seminormFromConst_seq_atTop hf1 hc hpm y)) (fun n ↦ ?_)
     simp only [seminormFromConst_seq]
@@ -186,9 +184,8 @@ theorem seminormFromConst_isPowMul : IsPowMul (seminormFromConst' c f) := fun x
   simp only [seminormFromConst']
   have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f (x ^ m) (m * n)) atTop
       (𝓝 (seminormFromConst' c f (x ^ m))) := by
-    apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x ^ m)).comp
-      (tendsto_atTop_atTop_of_monotone (fun _ _ hnk ↦ mul_le_mul_right hnk m) _)
-    rintro n; use n; exact le_mul_of_one_le_left' hm
+    exact (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (x ^ m)).comp
+      (tendsto_id.const_mul_atTop' (lt_of_lt_of_le zero_lt_one hm))
   apply tendsto_nhds_unique hlim
   convert (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).pow m using 1
   ext n
@@ -248,9 +245,7 @@ theorem seminormFromConst_const_mul (x : R) :
       seminormFromConst' c f c * seminormFromConst' c f x := by
   have hlim : Tendsto (fun n ↦ seminormFromConst_seq c f x (n + 1)) atTop
       (𝓝 (seminormFromConst' c f x)) := by
-    apply (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).comp
-      (tendsto_atTop_atTop_of_monotone add_left_mono _)
-    rintro n; use n; lia
+    exact (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x).comp (tendsto_add_atTop_nat 1)
   rw [seminormFromConst_apply_c hf1 hc hpm]
   apply tendsto_nhds_unique (tendsto_seminormFromConst_seq_atTop hf1 hc hpm (c * x))
   have hterm : seminormFromConst_seq c f (c * x) =
diff --git a/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean b/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
index c43ff4f06a2bae..aaa69fb191aba0 100644
--- a/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
+++ b/Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean
@@ -182,23 +182,14 @@ variable [NormedRing R]
 theorem spectralValue_eq_zero_iff [Nontrivial R] {p : R[X]} (hp : p.Monic) :
     spectralValue p = 0 ↔ p = X ^ p.natDegree := by
   refine ⟨fun h ↦ ?_, fun h ↦ h ▸ spectralValue_X_pow p.natDegree⟩
-  rw [spectralValue] at h
-  ext n
-  rw [coeff_X_pow]
-  split_ifs with hn
-  · rw [hn, coeff_natDegree]; exact hp
-  · by_cases hn' : n < p.natDegree
-    · have h_le : iSup (spectralValueTerms p) ≤ 0 := h.le
-      have h_exp : 0 < 1 / ((p.natDegree : ℝ) - n) := by
-        rw [one_div_pos, ← cast_sub (le_of_lt hn'), cast_pos]
-        exact Nat.sub_pos_of_lt hn'
-      have h0 : (0 : ℝ) = 0 ^ (1 / ((p.natDegree : ℝ) - n)) := by rw [zero_rpow (ne_of_gt h_exp)]
-      rw [iSup, csSup_le_iff (spectralValueTerms_bddAbove p) (Set.range_nonempty _)] at h_le
-      specialize h_le (spectralValueTerms p n) ⟨n, rfl⟩
-      simp only [spectralValueTerms, if_pos hn'] at h_le
-      rw [h0, rpow_le_rpow_iff (norm_nonneg _) (le_refl _) h_exp] at h_le
-      exact norm_eq_zero.mp (le_antisymm h_le (norm_nonneg _))
-    · exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne (le_of_not_gt hn') (ne_comm.mpr hn))
+  refine hp.eq_X_pow_iff_natDegree_le_natTrailingDegree.mpr <|
+    le_natTrailingDegree hp.ne_zero fun n hn ↦ ?_
+  have h0 : spectralValueTerms p n = 0 := by
+    apply le_antisymm ((le_ciSup (spectralValueTerms_bddAbove p) n).trans h.le)
+    exact spectralValueTerms_nonneg _ _
+  rw [spectralValueTerms_of_lt_natDegree _ hn,
+    Real.rpow_eq_zero_iff_of_nonneg (norm_nonneg _)] at h0
+  exact norm_eq_zero.mp h0.1
 
 end Normed
 
@@ -406,12 +397,9 @@ theorem spectralNorm.eq_of_normalClosure' (x : E) :
     spectralNorm K (normalClosure K E (AlgebraicClosure E))
       (algebraMap E (normalClosure K E (AlgebraicClosure E)) x) =
     spectralNorm K L (algebraMap E L x) := by
-  simp only [spectralNorm, spectralValue]
-  have h_min : minpoly K (algebraMap (↥E) (↥(normalClosure K (↥E) (AlgebraicClosure ↥E))) x) =
-      minpoly K (algebraMap (↥E) L x) := by
-    rw [minpoly.algebraMap_eq (algebraMap (↥E) ↥(normalClosure K E (AlgebraicClosure E))).injective
-      x, ← minpoly.algebraMap_eq (algebraMap (↥E) L).injective x]
-  simp_rw [h_min]
+  rw [← spectralNorm.eq_of_tower (K := K) (E := E)
+      (L := normalClosure K E (AlgebraicClosure E)) x,
+    ← spectralNorm.eq_of_tower (K := K) (E := E) (L := L) x]
 
 /-- If `L/E/K` is a tower of fields and `x = algebraMap E L g`, then the spectral norm
   of `g : E` when regarded as an element of the normal closure of `E` equals the spectral norm
@@ -703,6 +691,7 @@ universe u v
 variable {K : Type u} [NontriviallyNormedField K] {L : Type v} [Field L] [Algebra K L]
   [Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K]
 
+set_option backward.inferInstanceAs.wrap.data false in
 /-- If `K` is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and
   `L/K` is an algebraic extension, then any power-multiplicative `K`-algebra norm on `L` coincides
   with the spectral norm. -/
@@ -710,9 +699,9 @@ theorem spectralNorm_unique [CompleteSpace K] {f : AlgebraNorm K L} (hf_pm : IsP
     f = spectralAlgNorm K L := by
   apply eq_of_powMul_faithful f hf_pm _ spectralAlgNorm_isPowMul
   intro x
-  let E : Type v := id K⟮x⟯
-  let : Field E := show Field K⟮x⟯ by infer_instance
-  let : Module K E := show Module K K⟮x⟯ by infer_instance
+  set E : Type v := id K⟮x⟯
+  letI hE : Field E := inferInstanceAs (Field K⟮x⟯)
+  letI : Algebra K E := inferInstanceAs (Algebra K K⟮x⟯)
   let id1 : K⟮x⟯ →ₗ[K] E := LinearMap.id
   let id2 : E →ₗ[K] K⟮x⟯ := LinearMap.id
   set hs_norm : RingNorm E :=
@@ -728,8 +717,8 @@ theorem spectralNorm_unique [CompleteSpace K] {f : AlgebraNorm K L} (hf_pm : IsP
       eq_zero_of_map_eq_zero' a ha := by
         simpa [id_eq, eq_mpr_eq_cast, cast_eq, LinearMap.coe_mk, ← spectralAlgNorm_def,
           map_eq_zero_iff_eq_zero, ZeroMemClass.coe_eq_zero] using ha }
-  let n1 : NormedRing E := RingNorm.toNormedRing hs_norm
-  let N1 : NormedSpace K E :=
+  letI n1 : NormedRing E := RingNorm.toNormedRing hs_norm
+  letI N1 : NormedSpace K E :=
     { one_smul e := by simp [one_smul]
       mul_smul k1 k2 e := by simp [mul_smul]
       smul_zero e := by simp
@@ -748,8 +737,8 @@ theorem spectralNorm_unique [CompleteSpace K] {f : AlgebraNorm K L} (hf_pm : IsP
       mul_le' a b := map_mul_le_mul _ _ _
       eq_zero_of_map_eq_zero' a ha := by
         simpa [map_eq_zero_iff_eq_zero, map_eq_zero] using ha }
-  let n2 : NormedRing K⟮x⟯ := RingNorm.toNormedRing hf_norm
-  let N2 : NormedSpace K K⟮x⟯ :=
+  letI n2 : NormedRing K⟮x⟯ := RingNorm.toNormedRing hf_norm
+  letI N2 : NormedSpace K K⟮x⟯ :=
     { one_smul e := by simp [one_smul]
       mul_smul k1 k2 e := by simp [mul_smul]
       smul_zero e := by simp
@@ -761,9 +750,9 @@ theorem spectralNorm_unique [CompleteSpace K] {f : AlgebraNorm K L} (hf_pm : IsP
         have : (algebraMap (↥K⟮x⟯) L) (k • y) = k • algebraMap (↥K⟮x⟯) L y := by
           simp [IntermediateField.algebraMap_apply]
         rw [this, map_smul_eq_mul] }
-  have hKx_fin : FiniteDimensional K ↥K⟮x⟯ :=
+  haveI hKx_fin : FiniteDimensional K ↥K⟮x⟯ :=
     IntermediateField.adjoin.finiteDimensional (Algebra.IsAlgebraic.isAlgebraic x).isIntegral
-  have : FiniteDimensional K E := hKx_fin
+  haveI : FiniteDimensional K E := hKx_fin
   set Id1 : K⟮x⟯ →L[K] E := ⟨id1, id1.continuous_of_finiteDimensional⟩
   set Id2 : E →L[K] K⟮x⟯ := ⟨id2, id2.continuous_of_finiteDimensional⟩
   obtain ⟨C1, hC1_pos, hC1⟩ : ∃ C1 : ℝ, 0 < C1 ∧ ∀ y : K⟮x⟯, ‖id1 y‖ ≤ C1 * ‖y‖ :=
diff --git a/Mathlib/Analysis/ODE/Transform.lean b/Mathlib/Analysis/ODE/Transform.lean
index 67c3e7922fd91c..3812b9890840be 100644
--- a/Mathlib/Analysis/ODE/Transform.lean
+++ b/Mathlib/Analysis/ODE/Transform.lean
@@ -154,13 +154,9 @@ lemma IsIntegralCurve.comp_mul (hγ : IsIntegralCurve γ v) (a : ℝ) :
 
 lemma isIntegralCurve_comp_mul_ne_zero {a : ℝ} (ha : a ≠ 0) :
     IsIntegralCurve (γ ∘ (· * a)) (a • v ∘ (· * a)) ↔ IsIntegralCurve γ v := by
-  refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_mul _⟩
-  convert hγ.comp_mul a⁻¹
-  · ext t
-    simp only [comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]
-  · ext t
-    simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
-      smul_smul, one_smul]
+  have huniv : a⁻¹ • (univ : Set ℝ) = univ := by ext t; simp [Set.mem_inv_smul_set_iff₀, ha]
+  simpa [← isIntegralCurveOn_univ, huniv] using
+    (isIntegralCurveOn_comp_mul_ne_zero (γ := γ) (v := v) (s := (univ : Set ℝ)) ha)
 
 /-- If the vector field `v` vanishes at `x₀` for all times, then the constant curve at `x₀`
 is a global integral curve of `v`. -/
diff --git a/Mathlib/Analysis/PSeries.lean b/Mathlib/Analysis/PSeries.lean
index ffdf8264c6785e..39c8120face63a 100644
--- a/Mathlib/Analysis/PSeries.lean
+++ b/Mathlib/Analysis/PSeries.lean
@@ -5,10 +5,12 @@ Authors: Yury Kudryashov
 -/
 module
 
-public import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
 public import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
 public import Mathlib.Analysis.SumOverResidueClass
 
+import Mathlib.Analysis.Asymptotics.SpecificAsymptotics
+import Mathlib.Analysis.Normed.Module.FiniteDimension
+
 /-!
 # Convergence of `p`-series
 
@@ -444,32 +446,17 @@ section shifted
 
 open Filter Asymptotics Topology
 
--- see https://github.com/leanprover-community/mathlib4/issues/29041
-set_option linter.unusedSimpArgs false in
 lemma Real.summable_one_div_nat_add_rpow (a : ℝ) (s : ℝ) :
     Summable (fun n : ℕ ↦ 1 / |n + a| ^ s) ↔ 1 < s := by
-  suffices ∀ (b c : ℝ), Summable (fun n : ℕ ↦ 1 / |n + b| ^ s) →
-      Summable (fun n : ℕ ↦ 1 / |n + c| ^ s) by
-    simp_rw [← summable_one_div_nat_rpow, Iff.intro (this a 0) (this 0 a), add_zero, Nat.abs_cast]
-  refine fun b c h ↦ summable_of_isBigO_nat h (isBigO_of_div_tendsto_nhds ?_ 1 ?_)
-  · filter_upwards [eventually_gt_atTop (Nat.ceil |b|)] with n hn hx
-    have hna : 0 < n + b := by linarith [lt_of_abs_lt ((abs_neg b).symm ▸ Nat.lt_of_ceil_lt hn)]
-    exfalso
-    revert hx
-    positivity
-  · simp_rw [Pi.div_def, div_div, mul_one_div, one_div_div]
-    refine (?_ : Tendsto (fun x : ℝ ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)).comp
-      tendsto_natCast_atTop_atTop
-    have : Tendsto (fun x : ℝ ↦ 1 + (b - c) / x) atTop (𝓝 1) := by
-      simpa using tendsto_const_nhds.add ((tendsto_const_nhds (X := ℝ)).div_atTop tendsto_id)
-    have : Tendsto (fun x ↦ (x + b) / (x + c)) atTop (𝓝 1) := by
-      refine (this.comp (tendsto_id.atTop_add (tendsto_const_nhds (x := c)))).congr' ?_
-      filter_upwards [eventually_gt_atTop (-c)] with x hx
-      simp [field, (by linarith : 0 < x + c).ne']
-    apply (one_rpow s ▸ (continuousAt_rpow_const _ s (by simp)).tendsto.comp this).congr'
-    filter_upwards [eventually_gt_atTop (-b), eventually_gt_atTop (-c)] with x hb hc
-    rw [neg_lt_iff_pos_add] at hb hc
-    rw [Function.comp_apply, div_rpow hb.le hc.le, abs_of_pos hb, abs_of_pos hc]
+  have hnorm : Tendsto (fun n : ℕ ↦ ‖(n : ℝ)‖) atTop atTop :=
+    Tendsto.congr' (by simp) tendsto_natCast_atTop_atTop
+  have h_abs : (fun n : ℕ ↦ |n + a|) ~[atTop] (·) := by
+    apply (IsEquivalent.add_const_of_norm_tendsto_atTop IsEquivalent.refl hnorm).congr_left
+    · filter_upwards [eventually_gt_atTop (Nat.ceil |a|)] with _ hn
+      rw [abs_of_pos]
+      linarith [lt_of_abs_lt ((abs_neg a).symm ▸ Nat.lt_of_ceil_lt hn)]
+  rw [← summable_one_div_nat_rpow, Asymptotics.IsEquivalent.summable_iff_nat]
+  simpa [one_div] using (IsEquivalent.rpow (fun n ↦ by positivity) h_abs).inv
 
 lemma Real.summable_one_div_int_add_rpow (a : ℝ) (s : ℝ) :
     Summable (fun n : ℤ ↦ 1 / |n + a| ^ s) ↔ 1 < s := by
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
index 051504c48d205e..8d1b4db879ce2d 100644
--- a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
@@ -325,16 +325,12 @@ theorem arg_inv (x : ℂ) : arg x⁻¹ = if arg x = π then π else -arg x := by
 
 -- TODO: Replace the next two lemmas by general facts about periodic functions
 lemma norm_eq_one_iff' : ‖x‖ = 1 ↔ ∃ θ ∈ Set.Ioc (-π) π, exp (θ * I) = x := by
-  rw [norm_eq_one_iff]
   constructor
-  · rintro ⟨θ, rfl⟩
-    refine ⟨toIocMod (mul_pos two_pos Real.pi_pos) (-π) θ, ?_, ?_⟩
-    · convert toIocMod_mem_Ioc _ _ _
-      ring
-    · rw [eq_sub_of_add_eq <| toIocMod_add_toIocDiv_zsmul _ _ θ, ofReal_sub,
-      ofReal_zsmul, ofReal_mul, ofReal_ofNat, exp_mul_I_periodic.sub_zsmul_eq]
+  · intro hx
+    refine ⟨arg x, arg_mem_Ioc x, ?_⟩
+    simpa [hx] using norm_mul_exp_arg_mul_I x
   · rintro ⟨θ, _, rfl⟩
-    exact ⟨θ, rfl⟩
+    exact Complex.norm_exp_ofReal_mul_I θ
 
 lemma image_exp_Ioc_eq_sphere : (fun θ : ℝ ↦ exp (θ * I)) '' Set.Ioc (-π) π = sphere 0 1 := by
   ext; simpa using norm_eq_one_iff'.symm
diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean b/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
index 73583e431cf8f6..9306b58f0281a7 100644
--- a/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
@@ -211,20 +211,15 @@ lemma norm_log_one_add_le {z : ℂ} (hz : ‖z‖ < 1) :
 
 /-- For `‖z‖ ≤ 1/2`, the complex logarithm is bounded by `(3/2) * ‖z‖`. -/
 lemma norm_log_one_add_half_le_self {z : ℂ} (hz : ‖z‖ ≤ 1 / 2) : ‖log (1 + z)‖ ≤ (3 / 2) * ‖z‖ := by
-  apply le_trans (norm_log_one_add_le (lt_of_le_of_lt hz one_half_lt_one))
-  have hz3 : (1 - ‖z‖)⁻¹ ≤ 2 := by
-    rw [inv_eq_one_div, div_le_iff₀]
-    · linarith
-    · linarith
-  have hz4 : ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2 * 2 / 2 := by
-    gcongr
-    · rw [inv_nonneg]
-      linarith
-    · rw [sq, div_eq_mul_one_div]
-      gcongr
-  simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
-    IsUnit.div_mul_cancel] at hz4
-  linarith
+  refine (norm_log_one_add_le (lt_of_le_of_lt hz one_half_lt_one)).trans ?_
+  have hz0 : 0 ≤ ‖z‖ := norm_nonneg z
+  have hdiv : (1 - ‖z‖)⁻¹ / 2 ≤ (1 : ℝ) := by
+    have h1 : (1 - ‖z‖)⁻¹ ≤ 2 := by
+      rw [inv_eq_one_div, div_le_iff₀] <;> linarith
+    linarith
+  have hquad : ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ ^ 2 := by
+    nlinarith [sq_nonneg ‖z‖, hdiv]
+  nlinarith [hz, hz0, hquad]
 
 /-- The difference of `log (1-z)⁻¹` and its `(n+1)`st Taylor polynomial can be bounded in
 terms of `‖z‖`. -/
diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Order.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Order.lean
index 26af4b4eabcfc6..6bf23f409bd6e2 100644
--- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Order.lean
+++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Order.lean
@@ -56,31 +56,27 @@ lemma CFC.log_monotoneOn : MonotoneOn log {a : A | IsStrictlyPositive a} := by
   by the continuity of the continuous functional calculus (`tendsto_cfc_fun`). Then, we use the
   fact that `x^p` is monotone for `p ∈ [0,1]` (`CFC.monotone_nnrpow`) and that the set of
   monotone functions is closed (`isClosed_monotoneOn`) to conclude the proof. -/
-  let s := {a : A | IsStrictlyPositive a}
-  let f (p : ℝ) := fun a => if a ∈ s then cfc (A := A) (fun x => p⁻¹ * (x ^ p - 1)) a else 0
-  let g := fun a => if a ∈ s then log (A := A) a else 0
-  have hg : s.EqOn g (log (A := A)) := by simp +contextual [g, Set.EqOn]
-  refine MonotoneOn.congr ?_ hg
-  refine isClosed_monotoneOn.mem_of_tendsto (f := f) (b := (𝓝[>] 0)) ?tendsto ?eventually
+  rw [Set.monotoneOn_iff_monotone]
+  let f (p : ℝ) (a : {a : A | IsStrictlyPositive a}) :=
+    cfc (A := A) (fun x => p⁻¹ * (x ^ p - 1)) a
+  refine isClosed_monotone.mem_of_tendsto (f := f) (b := 𝓝[>] 0) ?tendsto ?eventually
   case tendsto =>
     rw [tendsto_pi_nhds]
     intro a
-    by_cases ha : a ∈ s
-    · have hf : ∀ p, cfc (fun x => p⁻¹ * (x ^ p - 1)) a = f p a := by simp [f, ha]
-      exact (hg ha ▸ tendsto_cfc_rpow_sub_one_log ha).congr hf
-    · simp [g, f, ha]
+    simpa [f] using (tendsto_cfc_rpow_sub_one_log (A := A) (a := a) a.2)
   case eventually =>
-    have h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < 1 := nhdsGT_basis 0 |>.mem_of_mem zero_lt_one
-    filter_upwards [h₁] with p ⟨hp, hp'⟩
-    have hf : s.EqOn (fun a : A => p⁻¹ • (a ^ p - 1)) (f p) := by
-      intro a ha
-      simp only [ha, ↓reduceIte, f, ← smul_eq_mul]
+    filter_upwards [nhdsGT_basis 0 |>.mem_of_mem zero_lt_one] with p hp
+    have hf (a : {a : A | IsStrictlyPositive a}) : f p a = p⁻¹ • ((a : A) ^ p - 1) := by
+      simp only [f, ← smul_eq_mul]
       rw [cfc_smul _ (hf := by fun_prop (disch := grind -abstractProof)),
         cfc_sub _ _ (hf := by fun_prop (disch := grind -abstractProof)),
         cfc_const_one .., rpow_eq_cfc_real ..]
-    refine MonotoneOn.congr (fun a ha b hb hab ↦ ?_) hf
-    gcongr
-    grind
+    intro a b hab
+    rw [hf a, hf b]
+    have hp0 : 0 ≤ p⁻¹ := by simpa [one_div] using (_root_.inv_nonneg.mpr hp.1.le)
+    exact smul_le_smul_of_nonneg_left
+      (sub_le_sub_right (CFC.monotone_rpow ⟨hp.1.le, hp.2.le⟩ (show (a : A) ≤ b from hab)) (1 : A))
+      hp0
 
 @[gcongr]
 lemma CFC.log_le_log {a b : A} (hab : a ≤ b) (ha : IsStrictlyPositive a := by cfc_tac) :
diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean
index df50737a2cf908..ca08e2ff009a26 100644
--- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean
+++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean
@@ -391,23 +391,16 @@ lemma monotoneOn_rpowIntegrand₁₂ (hp : p ∈ Ioo 1 2) (ht : 0 < t) :
 
 lemma integrableOn_rpowIntegrand₁₂ (hp : p ∈ Ioo 1 2) (hx : 0 ≤ x) :
     IntegrableOn (rpowIntegrand₁₂ p · x) (Ioi 0) := by
-  have hmain : (rpowIntegrand₁₂ p · x)
-      =ᵐ[volume.restrict (Ioi 0)] (x * rpowIntegrand₀₁ (p-1) · x) := by
-    filter_upwards [ae_restrict_mem measurableSet_Ioi] with a ha
-    rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ha]
-  rw [integrableOn_congr_fun_ae hmain]
-  refine Integrable.const_mul ?_ _
-  exact integrableOn_rpowIntegrand₀₁_Ioi (by grind) hx
+  exact (integrableOn_congr_fun (fun t ht ↦ rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht)
+    measurableSet_Ioi).2 <|
+      Integrable.const_mul (integrableOn_rpowIntegrand₀₁_Ioi (by grind) hx) _
 
 /-- The integral representation of the function `x ↦ x^p` (where `p ∈ (1, 2)`) . -/
 lemma rpow_eq_const_mul_integral_rpowIntegrand₁₂ (hp : p ∈ Ioo 1 2) (hx : 0 ≤ x) :
     x ^ p
       = (∫ t in Ioi 0, rpowIntegrand₀₁ (p - 1) t 1)⁻¹ * ∫ t in Ioi 0, rpowIntegrand₁₂ p t x := by
-  have hmain : (rpowIntegrand₁₂ p · x)
-      =ᵐ[volume.restrict (Ioi 0)] (x * rpowIntegrand₀₁ (p-1) · x) := by
-    filter_upwards [ae_restrict_mem measurableSet_Ioi] with a ha
-    rw [rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ha]
-  rw [integral_congr_ae hmain, integral_const_mul_of_integrable
+  rw [setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦
+      rpowIntegrand₁₂_eq_mul_rpowIntegrand₀₁ hx ht), integral_const_mul_of_integrable
       (integrableOn_rpowIntegrand₀₁_Ioi (by grind) hx)]
   have h₁ : x ^ p = x * x ^ (p - 1) := by
     rw [mul_comm, ← rpow_add_one' hx (by grind)]
diff --git a/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean b/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean
index cc0c17dd90b56f..b5f0a06ff844c4 100644
--- a/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Elliptic/Weierstrass.lean
@@ -479,19 +479,13 @@ private lemma weierstrassP_add_coe_aux (z : ℂ) (l : L.lattice) (hl : l.1 / 2 
 
 @[simp]
 lemma weierstrassP_add_coe (z : ℂ) (l : L.lattice) : ℘[L] (z + l) = ℘[L] z := by
-  let G : AddSubgroup ℂ :=
-    { carrier := { z | (℘[L] <| · + z) = ℘[L] }
-      add_mem' := by simp_all [funext_iff, ← add_assoc]
-      zero_mem' := by simp
-      neg_mem' {z} hz := funext fun i ↦ by conv_lhs => rw [← hz]; simp }
-  have : L.lattice ≤ G.toIntSubmodule := by
-    rw [lattice, Submodule.span_le]
-    rintro _ (rfl | rfl)
-    · ext i
-      exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₁_mem_lattice⟩ L.ω₁_div_two_notMem_lattice
-    · ext i
-      exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₂_mem_lattice⟩ L.ω₂_div_two_notMem_lattice
-  exact congr_fun (this l.2) _
+  obtain ⟨m, n, hmn⟩ := L.mem_lattice.mp l.2
+  have hω₁ : ℘[L].Periodic L.ω₁ := fun w ↦
+    L.weierstrassP_add_coe_aux w ⟨_, L.ω₁_mem_lattice⟩ L.ω₁_div_two_notMem_lattice
+  have hω₂ : ℘[L].Periodic L.ω₂ := fun w ↦
+    L.weierstrassP_add_coe_aux w ⟨_, L.ω₂_mem_lattice⟩ L.ω₂_div_two_notMem_lattice
+  rw [← hmn]
+  simpa [add_assoc] using (hω₁.int_mul m).add_period (hω₂.int_mul n) z
 
 lemma periodic_weierstrassP (l : L.lattice) : ℘[L].Periodic l :=
   (L.weierstrassP_add_coe · l)
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
index 14d25fb22eb80f..77e13d24a2726b 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
@@ -408,18 +408,8 @@ def Gamma (s : ℝ) : ℝ :=
 set_option backward.isDefEq.respectTransparency false in
 theorem Gamma_eq_integral {s : ℝ} (hs : 0 < s) :
     Gamma s = ∫ x in Ioi 0, exp (-x) * x ^ (s - 1) := by
-  rw [Gamma, Complex.Gamma_eq_integral (by rwa [Complex.ofReal_re] : 0 < Complex.re s)]
-  dsimp only [Complex.GammaIntegral]
-  simp_rw [← Complex.ofReal_one, ← Complex.ofReal_sub]
-  suffices ∫ x : ℝ in Ioi 0, ↑(exp (-x)) * (x : ℂ) ^ ((s - 1 : ℝ) : ℂ) =
-      ∫ x : ℝ in Ioi 0, ((exp (-x) * x ^ (s - 1) : ℝ) : ℂ) by
-    have cc : ∀ r : ℝ, Complex.ofReal r = @RCLike.ofReal ℂ _ r := fun r => rfl
-    conv_lhs => rw [this]; enter [1, 2, x]; rw [cc]
-    rw [_root_.integral_ofReal, ← cc, Complex.ofReal_re]
-  refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_
-  push_cast
-  rw [Complex.ofReal_cpow (le_of_lt hx)]
-  push_cast; rfl
+  rw [Gamma, Complex.Gamma_eq_integral (RCLike.ofReal_pos.mp hs), Complex.GammaIntegral_ofReal,
+    Complex.ofReal_re]
 
 theorem Gamma_add_one {s : ℝ} (hs : s ≠ 0) : Gamma (s + 1) = s * Gamma s := by
   simp_rw [Gamma]
@@ -521,7 +511,7 @@ theorem Gamma_ne_zero {s : ℝ} (hs : ∀ m : ℕ, s ≠ -m) : Gamma s ≠ 0 :=
       apply n_ih
       · intro m
         specialize hs (1 + m)
-        contrapose hs
+        contrapose! hs
         rw [← eq_sub_iff_add_eq] at hs
         rw [hs]
         push_cast
diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
index 53ea0ff4d7ae44..eee1e639cc2855 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean
@@ -271,21 +271,13 @@ theorem tendsto_logGammaSeq (hf_conv : ConvexOn ℝ (Ioi 0) f)
       rw [sub_add_cancel, Nat.sub_add_cancel hn] at this
       rw [this]
       ring
-    replace hm :=
-      ((Tendsto.congr' this hm).add (tendsto_const_nhds : Tendsto (fun _ => log (x - 1)) _ _)).comp
-        (tendsto_add_atTop_nat 1)
-    have :
-      ((fun x_1 : ℕ =>
-            (fun n : ℕ =>
-                  logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1))
-                x_1 +
-              (fun b : ℕ => log (x - 1)) x_1) ∘
-          fun a : ℕ => a + 1) =
-        fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n) := by
-      ext1 n
-      dsimp only [Function.comp_apply]
-      rw [sub_add_cancel, Nat.add_sub_cancel]
-    rw [this] at hm
+    replace hm :
+        Tendsto (fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n)) atTop
+          (𝓝 (f (x - 1) - f 1 + log (x - 1))) := by
+      simpa [Function.comp_def, Nat.add_sub_cancel] using
+        (((Tendsto.congr' this hm).add
+          (tendsto_const_nhds : Tendsto (fun _ => log (x - 1)) _ _)).comp
+          (tendsto_add_atTop_nat 1))
     convert hm.sub (tendsto_log_nat_add_one_sub_log.const_mul x) using 2
     · ring
     · have := hf_feq ((Nat.cast_nonneg m).trans_lt hy)
diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
index f6c3cacfd22085..3f43294b09daeb 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
@@ -97,13 +97,7 @@ theorem verticalIntegral_norm_le (hb : 0 < b.re) (c : ℝ) {T : ℝ} (hT : 0 ≤
       rw [mul_assoc]
   · intro y hy
     have absy : |y| ≤ |c| := by
-      rcases le_or_gt 0 c with (h | h)
-      · rw [uIoc_of_le h] at hy
-        rw [abs_of_nonneg h, abs_of_pos hy.1]
-        exact hy.2
-      · rw [uIoc_of_ge h.le] at hy
-        rw [abs_of_neg h, abs_of_nonpos hy.2, neg_le_neg_iff]
-        exact hy.1.le
+      simpa using Set.abs_sub_left_of_mem_uIcc (Set.uIoc_subset_uIcc hy)
     rw [norm_mul, norm_I, one_mul, two_mul]
     refine (norm_sub_le _ _).trans (add_le_add (vert_norm_bound hT absy) ?_)
     rw [← abs_neg y] at absy
diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
index 9337e217183da0..36369ef668f727 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
@@ -288,27 +288,20 @@ theorem integral_gaussian_complex {b : ℂ} (hb : 0 < re b) :
 -- The Gaussian integral on the half-line, `∫ x in Ioi 0, exp (-b * x^2)`, for complex `b`.
 theorem integral_gaussian_complex_Ioi {b : ℂ} (hb : 0 < re b) :
     ∫ x : ℝ in Ioi 0, cexp (-b * (x : ℂ) ^ 2) = (π / b) ^ (1 / 2 : ℂ) / 2 := by
+  let f : ℝ → ℂ := fun x => cexp (-b * (x : ℂ) ^ 2)
   have full_integral := integral_gaussian_complex hb
-  have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi
-  rw [← integral_add_compl this (integrable_cexp_neg_mul_sq hb), compl_Ioi] at full_integral
-  suffices ∫ x : ℝ in Iic 0, cexp (-b * (x : ℂ) ^ 2) = ∫ x : ℝ in Ioi 0, cexp (-b * (x : ℂ) ^ 2) by
-    rw [this, ← mul_two] at full_integral
-    rwa [eq_div_iff]; exact two_ne_zero
-  have : ∀ c : ℝ, ∫ x in (0 : ℝ)..c, cexp (-b * (x : ℂ) ^ 2) =
-      ∫ x in -c..0, cexp (-b * (x : ℂ) ^ 2) := by
-    intro c
-    have := intervalIntegral.integral_comp_sub_left (a := 0) (b := c)
-      (fun x => cexp (-b * (x : ℂ) ^ 2)) 0
-    simpa [zero_sub, neg_sq, neg_zero] using this
-  have t1 :=
-    intervalIntegral_tendsto_integral_Ioi 0 (integrable_cexp_neg_mul_sq hb).integrableOn tendsto_id
-  have t2 :
-    Tendsto (fun c : ℝ => ∫ x : ℝ in (0 : ℝ)..c, cexp (-b * (x : ℂ) ^ 2)) atTop
-      (𝓝 (∫ x : ℝ in Iic 0, cexp (-b * (x : ℂ) ^ 2))) := by
-    simp_rw [this]
-    refine intervalIntegral_tendsto_integral_Iic _ ?_ tendsto_neg_atTop_atBot
-    apply (integrable_cexp_neg_mul_sq hb).integrableOn
-  exact tendsto_nhds_unique t2 t1
+  have h_eq : ∫ x : ℝ in Iic 0, f x = ∫ x : ℝ in Ioi 0, f x := by
+    calc
+      ∫ x : ℝ in Iic 0, f x = ∫ x : ℝ in Ioi 0, f (-x) := by
+        simpa [f] using (integral_comp_neg_Ioi (c := 0) (f := f)).symm
+      _ = ∫ x : ℝ in Ioi 0, f x := by
+        refine setIntegral_congr_fun measurableSet_Ioi ?_
+        intro x hx
+        simp [f]
+  have hmeas : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi
+  rw [← integral_add_compl hmeas (integrable_cexp_neg_mul_sq hb), compl_Ioi, h_eq, ← mul_two]
+    at full_integral
+  exact (eq_div_iff two_ne_zero).2 (by simpa [mul_comm] using full_integral)
 
 -- The Gaussian integral on the half-line, `∫ x in Ioi 0, exp (-b * x^2)`, for real `b`.
 theorem integral_gaussian_Ioi (b : ℝ) :
diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
index 8289d76547c935..a63812929e6ee4 100644
--- a/Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
@@ -88,22 +88,14 @@ theorem Complex.tsum_exp_neg_quadratic {a : ℂ} (ha : 0 < a.re) (b : ℂ) :
       1 / a ^ (1 / 2 : ℂ) * ∑' n : ℤ, cexp (-π / a * (n + I * b) ^ 2) := by
   let f : ℝ → ℂ := fun x ↦ cexp (-π * a * x ^ 2 + 2 * π * b * x)
   have hCf : Continuous f := by
-    refine Complex.continuous_exp.comp (Continuous.add ?_ ?_)
-    · exact continuous_const.mul (Complex.continuous_ofReal.pow 2)
-    · exact continuous_const.mul Complex.continuous_ofReal
+    fun_prop
   have hFf : 𝓕 f = fun x : ℝ ↦ 1 / a ^ (1 / 2 : ℂ) * cexp (-π / a * (x + I * b) ^ 2) :=
     fourier_gaussian_pi' ha b
-  have h1 : 0 < (↑π * a).re := by
-    rw [re_ofReal_mul]
-    exact mul_pos pi_pos ha
-  have h2 : 0 < (↑π / a).re := by
-    rw [div_eq_mul_inv, re_ofReal_mul, inv_re]
-    refine mul_pos pi_pos (div_pos ha <| normSq_pos.mpr ?_)
-    contrapose! ha
-    rw [ha, zero_re]
   have f_bd : f =O[cocompact ℝ] (fun x => |x| ^ (-2 : ℝ)) := by
-    convert (cexp_neg_quadratic_isLittleO_abs_rpow_cocompact ?_ _ (-2)).isBigO
-    rwa [neg_mul, neg_re, neg_lt_zero]
+    convert
+      (cexp_neg_quadratic_isLittleO_abs_rpow_cocompact (a := -π * a) (b := 2 * π * b)
+        (by simpa [neg_mul, neg_re, re_ofReal_mul, neg_lt_zero] using mul_pos pi_pos ha)
+        (-2)).isBigO
   have Ff_bd : (𝓕 f) =O[cocompact ℝ] (fun x => |x| ^ (-2 : ℝ)) := by
     rw [hFf]
     have : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 =
@@ -111,9 +103,13 @@ theorem Complex.tsum_exp_neg_quadratic {a : ℂ} (ha : 0 < a.re) (b : ℂ) :
       intro x; ring_nf; rw [I_sq]; ring
     simp_rw [this]
     conv => enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]
-    refine ((cexp_neg_quadratic_isLittleO_abs_rpow_cocompact
-      (?_) (-2 * ↑π * I * b / a) (-2)).isBigO.const_mul_left _).const_mul_left _
-    rwa [neg_div, neg_re, neg_lt_zero]
+    refine ((cexp_neg_quadratic_isLittleO_abs_rpow_cocompact (a := -π / a)
+      (b := (-2 * ↑π * I * b) / a)
+      (by
+        rw [neg_div, neg_re, neg_lt_zero, div_eq_mul_inv, re_ofReal_mul, inv_re]
+        refine mul_pos pi_pos (div_pos ha <| normSq_pos.mpr ?_)
+        contrapose! ha
+        rw [ha, zero_re]) (-2)).isBigO.const_mul_left _).const_mul_left _
   convert Real.tsum_eq_tsum_fourier_of_rpow_decay hCf one_lt_two f_bd Ff_bd 0 using 1
   · simp only [f, zero_add, ofReal_intCast]
   · rw [← tsum_mul_left]
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean b/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
index 5be24a87bf35ec..23552b861040a9 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
@@ -151,27 +151,19 @@ theorem log_mul_add {x y : ℝ≥0∞} : log (x * y) = log x + log y := by
       positivity
 
 theorem log_rpow {x : ℝ≥0∞} {y : ℝ} : log (x ^ y) = y * log x := by
-  rcases lt_trichotomy y 0 with (y_neg | rfl | y_pos)
-  · rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
-    · simp only [ENNReal.zero_rpow_def y, not_lt_of_gt y_neg, y_neg.ne, if_false, log_top,
-        log_zero, EReal.coe_mul_bot_of_neg y_neg]
-    · rw [ENNReal.top_rpow_of_neg y_neg, log_zero, log_top, EReal.coe_mul_top_of_neg y_neg]
-    · have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'
-      have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne
-      simp only [log, rpow_eq_zero_iff, x_ne_zero, false_and, x_ne_top, or_self, ↓reduceIte,
-        rpow_eq_top_iff]
-      norm_cast
-      exact ENNReal.toReal_rpow x y ▸ Real.log_rpow x_real y
-  · simp
-  · rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
-    · rw [ENNReal.zero_rpow_of_pos y_pos, log_zero, EReal.mul_bot_of_pos]; norm_cast
-    · rw [ENNReal.top_rpow_of_pos y_pos, log_top, EReal.mul_top_of_pos]; norm_cast
-    · have x_ne_zero := (ENNReal.toReal_pos_iff.1 x_real).1.ne'
-      have x_ne_top := (ENNReal.toReal_pos_iff.1 x_real).2.ne
-      simp only [log, rpow_eq_zero_iff, x_ne_zero, false_and, x_ne_top, or_self, ↓reduceIte,
-        rpow_eq_top_iff]
-      norm_cast
-      exact ENNReal.toReal_rpow x y ▸ Real.log_rpow x_real y
+  rcases ENNReal.trichotomy x with (rfl | rfl | x_real)
+  · rcases lt_trichotomy y 0 with (y_neg | rfl | y_pos)
+    · simp [y_neg, EReal.coe_mul_bot_of_neg]
+    · simp
+    · simp [y_pos, EReal.coe_mul_bot_of_pos]
+  · rcases lt_trichotomy y 0 with (y_neg | rfl | y_pos)
+    · simp [y_neg, EReal.coe_mul_top_of_neg]
+    · simp
+    · simp [y_pos, EReal.coe_mul_top_of_pos]
+  · rw [log_pos_real' (by rw [← ENNReal.toReal_rpow]; positivity), log_pos_real' x_real]
+    norm_cast
+    rw [← ENNReal.toReal_rpow]
+    exact Real.log_rpow x_real y
 
 theorem log_pow {x : ℝ≥0∞} {n : ℕ} : log (x ^ n) = n * log x := by
   rw [← rpow_natCast, log_rpow, EReal.coe_natCast]
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean b/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
index 1040d2f6ccd5c3..412d2657479703 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
@@ -54,6 +54,13 @@ theorem log_div_self_antitoneOn : AntitoneOn (fun x : ℝ => log x / x) { x | ex
 theorem log_div_self_rpow_antitoneOn {a : ℝ} (ha : 0 < a) :
     AntitoneOn (fun x : ℝ => log x / x ^ a) { x | exp (1 / a) ≤ x } := by
   simp only [AntitoneOn, mem_setOf_eq]
+  have hbound : ∀ {z : ℝ}, exp (1 / a) ≤ z → exp 1 ≤ z ^ a := by
+    intro z hz
+    convert rpow_le_rpow _ hz (le_of_lt ha) using 1
+    · rw [← exp_mul]
+      simp only [Real.exp_eq_exp]
+      field
+    · positivity
   intro x hex y _ hxy
   have x_pos : 0 < x := lt_of_lt_of_le (exp_pos (1 / a)) hex
   have y_pos : 0 < y := by linarith
@@ -62,19 +69,7 @@ theorem log_div_self_rpow_antitoneOn {a : ℝ} (ha : 0 < a) :
   rw [← div_self (ne_of_lt ha).symm, div_eq_mul_one_div a a, rpow_mul y_pos.le, rpow_mul x_pos.le,
     log_rpow (rpow_pos_of_pos y_pos a), log_rpow (rpow_pos_of_pos x_pos a), mul_div_assoc,
     mul_div_assoc, mul_le_mul_iff_right₀ (one_div_pos.mpr ha)]
-  refine log_div_self_antitoneOn ?_ ?_ ?_
-  · simp only [Set.mem_setOf_eq]
-    convert rpow_le_rpow _ hex (le_of_lt ha) using 1
-    · rw [← exp_mul]
-      simp only [Real.exp_eq_exp]
-      field
-    positivity
-  · simp only [Set.mem_setOf_eq]
-    convert rpow_le_rpow _ (_root_.trans hex hxy) (le_of_lt ha) using 1
-    · rw [← exp_mul]
-      simp only [Real.exp_eq_exp]
-      field
-    positivity
+  refine log_div_self_antitoneOn (hbound hex) (hbound (_root_.trans hex hxy)) ?_
   gcongr
 
 theorem log_div_sqrt_antitoneOn : AntitoneOn (fun x : ℝ => log x / √x) { x | exp 2 ≤ x } := by
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean b/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
index afeed57a6af872..b83c1ef068f222 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
@@ -47,10 +47,7 @@ theorem posLog_def : log⁺ x = max 0 (log x) := rfl
 
 /-- Presentation of `log` in terms of its positive part. -/
 theorem posLog_sub_posLog_inv : log⁺ x - log⁺ x⁻¹ = log x := by
-  rw [posLog_def, posLog_def, log_inv]
-  by_cases! h : 0 ≤ log x
-  · simp [h]
-  · simp [neg_nonneg.1 (Left.nonneg_neg_iff.2 h.le)]
+  simpa [posLog_def, log_inv, max_comm] using max_zero_sub_eq_self (log x)
 
 /-- Presentation of `log⁺` in terms of `log`. -/
 theorem half_mul_log_add_log_abs : 2⁻¹ * (log x + |log x|) = log⁺ x := by
@@ -79,9 +76,7 @@ theorem posLog_eq_zero_iff (x : ℝ) : log⁺ x = 0 ↔ |x| ≤ 1 := by
 
 /-- The function `log⁺` equals `log` outside of the interval (-1,1). -/
 theorem posLog_eq_log (hx : 1 ≤ |x|) : log⁺ x = log x := by
-  simp only [posLog, sup_eq_right]
-  rw [← log_abs]
-  apply log_nonneg hx
+  simpa [posLog_def, ← log_abs] using max_eq_right (log_nonneg hx)
 
 /-- The function `log⁺` equals `log` for all natural numbers. -/
 theorem log_of_nat_eq_posLog {n : ℕ} : log⁺ n = log n := by
@@ -96,13 +91,8 @@ theorem posLog_eq_log_max_one (hx : 0 ≤ x) : log⁺ x = log (max 1 x) := by
 /-- The function `log⁺` is monotone on the positive axis. -/
 theorem monotoneOn_posLog : MonotoneOn log⁺ (Set.Ici 0) := by
   intro x hx y hy hxy
-  simp only [posLog, le_sup_iff, sup_le_iff, le_refl, true_and]
-  by_cases! h : log x ≤ 0
-  · tauto
-  · right
-    have := log_le_log (lt_trans Real.zero_lt_one ((log_pos_iff hx).1 h)) hxy
-    simp only [this, and_true, ge_iff_le]
-    linarith
+  rw [posLog_eq_log_max_one hx, posLog_eq_log_max_one hy]
+  exact log_le_log (by positivity) (max_le_max le_rfl hxy)
 
 @[gcongr]
 lemma posLog_le_posLog (hx : 0 ≤ x) (hxy : x ≤ y) : log⁺ x ≤ log⁺ y :=
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/RpowTendsto.lean b/Mathlib/Analysis/SpecialFunctions/Log/RpowTendsto.lean
index b0a5a23a3c0171..20fd4d039e15f2 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/RpowTendsto.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/RpowTendsto.lean
@@ -50,43 +50,32 @@ lemma Real.tendstoLocallyUniformlyOn_rpow_sub_one_log :
   intro s hs hs'
   rw [Metric.uniformity_basis_dist_le.tendstoUniformlyOn_iff_of_uniformity]
   intro ε hε
-  let pbound : ℝ := ε / (sSup ((fun x => ‖log x‖ ^ 2) '' s) + 1)
-  have hxs : ∀ x ∈ s, x ≠ 0 := by grind
-  have sSup_nonneg : 0 ≤ sSup ((fun x => ‖log x‖ ^ 2) '' s) := by
-    refine Real.sSup_nonneg ?_
-    grind [← sq_nonneg]
-  have sSup_nonneg' : 0 ≤ sSup ((fun x => ‖log x‖) '' s) := by
-    refine Real.sSup_nonneg ?_
-    grind [← sq_nonneg]
+  obtain ⟨logbound, hlogbound⟩ := hs'.exists_bound_of_continuousOn (f := Real.log)
+    (Real.continuousOn_log.mono fun _ hx => ne_of_gt (hs hx))
+  let logbound : ℝ := max logbound 0
+  let pbound : ℝ := ε / (logbound ^ 2 + 1)
   have pbound_pos : 0 < pbound := by positivity
   have h₁ : ∀ᶠ p : ℝ in 𝓝[>] 0, 0 < p ∧ p < pbound := nhdsGT_basis 0 |>.mem_of_mem pbound_pos
-  have h₂ : ∀ᶠ p : ℝ in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x => ‖log x‖) '' s) + 1) :=
+  have h₂ : ∀ᶠ p : ℝ in 𝓝[>] 0, p ≤ 1 / (logbound + 1) :=
     Eventually.filter_mono nhdsWithin_le_nhds <| eventually_le_nhds (by positivity)
-  have hcont : ContinuousOn (fun x => ‖log x‖ ^ 2) s := by
-    fun_prop (disch := assumption)
-  have hcont' : ContinuousOn (fun x => ‖log x‖) s := by
-    fun_prop (disch := assumption)
   filter_upwards [h₁, h₂] with p ⟨hp₁,hp₂⟩ hp₃
   intro x hx
+  have hxlog : ‖log x‖ ≤ logbound := (hlogbound x hx).trans (le_max_left _ _)
   have hx' : ‖p * log x‖ ≤ 1 := calc
     _ = p * ‖log x‖ := by grind [norm_mul, Real.norm_of_nonneg]
-    _ ≤ 1 / (sSup ((fun y => ‖log y‖) '' s) + 1) * ‖log x‖ := by gcongr
+    _ ≤ 1 / (logbound + 1) * ‖log x‖ := by gcongr
     _ ≤ 1 / (‖log x‖ + 1) * ‖log x‖ := by
         gcongr
-        refine le_csSup ?_ (by grind)
-        grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]
     _ = ‖log x‖ / (‖log x‖ + 1) := by grind
     _ ≤ 1 := by rw [div_le_one₀] <;> grind [norm_nonneg]
-  have pinv_nonneg : 0 ≤ p⁻¹ := by grind [_root_.inv_nonneg]
   rw [dist_eq_norm']
   calc
     _ ≤ p * ‖log x‖ ^ 2 := Real.norm_inv_mul_rpow_sub_one_sub_log_le hp₁ (hs hx) hx'
-    _ ≤ p * sSup ((fun x => ‖log x‖ ^ 2) '' s) := by
-          gcongr
-          refine le_csSup ?_ (by grind)
-          grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]
-    _ ≤ pbound * (sSup ((fun x => ‖log x‖ ^ 2) '' s) + 1) := by gcongr; grind
-    _ = ε := by grind
+    _ ≤ p * logbound ^ 2 := by gcongr
+    _ ≤ pbound * (logbound ^ 2 + 1) := by gcongr; grind
+    _ = ε := by
+      dsimp [pbound]
+      field_simp
 
 lemma tendsto_rpow_sub_one_log {x : ℝ} (hx : 0 < x) :
     Tendsto (fun p => p⁻¹ * (x ^ p - 1)) (𝓝[>] 0) (𝓝 (log x)) :=
diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Summable.lean b/Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
index 607d174bc9b38a..b058d52dec6308 100644
--- a/Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
@@ -158,43 +158,18 @@ lemma prod_vanishing_of_summable_norm (hf : Summable fun i ↦ ‖f i‖) {ε :
   have : Set.Iio ε ∈ nhds (f 0) := by simpa [f] using Iio_mem_nhds hε
   exact ContinuousAt.preimage_mem_nhds (by fun_prop) this
 
-open Finset in
-/-- In a complete normed ring, `∏' i, (1 + f i)` is convergent if the sum of real numbers
-`∑' i, ‖f i‖` is convergent. -/
-lemma multipliable_one_add_of_summable [CompleteSpace R]
-    (hf : Summable fun i ↦ ‖f i‖) : Multipliable fun i ↦ (1 + f i) := by
-  classical
-  refine CompleteSpace.complete <| Metric.cauchy_iff.mpr ⟨by infer_instance, fun ε hε ↦ ?_⟩
-  obtain ⟨r₁, hr₁, s₁, hs₁⟩ :=
-    (multipliable_norm_one_add_of_summable_norm hf).eventually_bounded_finset_prod
-  obtain ⟨s₂, hs₂⟩ := prod_vanishing_of_summable_norm hf (show 0 < ε / (2 * r₁) by positivity)
-  simp only [unconditional, Filter.mem_map, mem_atTop_sets, ge_iff_le, le_eq_subset,
-    Set.mem_preimage]
-  let s := s₁ ∪ s₂
-  -- The idea here is that if `s` is a large enough finset, then the product over `s` is bounded
-  -- by some `r`, and the product over finsets disjoint from `s` is within `ε / (2 * r)` of 1.
-  -- From this it follows that the products over any two finsets containing `s` are within `ε` of
-  -- each other.
-  -- Here `s₁ ⊆ s` guarantees that the product over `s` is bounded, and `s₂ ⊆ s` guarantees that
-  -- the product over terms not in `s` is small.
-  refine ⟨Metric.ball (∏ i ∈ s, (1 + f i)) (ε / 2), ⟨s, fun b hb ↦ ?_⟩, ?_⟩
-  · rw [← union_sdiff_of_subset hb, prod_union sdiff_disjoint.symm,
-      Metric.mem_ball, dist_eq_norm_sub, ← mul_sub_one,
-      show ε / 2 = r₁ * (ε / (2 * r₁)) by field]
-    apply (norm_mul_le _ _).trans_lt
-    refine lt_of_le_of_lt (b := r₁ * ‖∏ x ∈ b \ s, (1 + f x) - 1‖) ?_ ?_
-    · refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
-      exact (Finset.norm_prod_le _ _).trans (hs₁ _ subset_union_left)
-    · refine mul_lt_mul_of_pos_left (hs₂ _ ?_) hr₁
-      simp [s, sdiff_union_distrib, disjoint_iff_inter_eq_empty]
-  · intro x hx y hy
-    exact (dist_triangle_right _ _ (∏ i ∈ s, (1 + f i))).trans_lt (add_halves ε ▸ add_lt_add hx hy)
-
 lemma summable_finset_prod_of_summable_norm [CompleteSpace R] (hf : Summable (fun i ↦ ‖f i‖)) :
     Summable (fun s ↦ ∏ i ∈ s, f i) :=
   (summable_finset_prod_of_summable_nonneg (fun _ ↦ norm_nonneg _) hf).of_norm_bounded
     fun _ ↦ Finset.norm_prod_le _ _
 
+open Finset in
+/-- In a complete normed ring, `∏' i, (1 + f i)` is convergent if the sum of real numbers
+`∑' i, ‖f i‖` is convergent. -/
+lemma multipliable_one_add_of_summable [CompleteSpace R]
+    (hf : Summable fun i ↦ ‖f i‖) : Multipliable fun i ↦ (1 + f i) :=
+  multipliable_one_add_of_summable_prod (summable_finset_prod_of_summable_norm hf)
+
 lemma Summable.summable_log_norm_one_add (hu : Summable fun n ↦ ‖f n‖) :
     Summable fun i ↦ Real.log ‖1 + f i‖ := by
   suffices Summable (‖1 + f ·‖ - 1) from
diff --git a/Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean b/Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean
index d4077946464477..b9902482119075 100644
--- a/Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean
+++ b/Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean
@@ -175,18 +175,13 @@ theorem dist_integral_mulExpNegMulSq_comp_le (f : E →ᵇ ℝ)
         (toReal_pos ((Measure.measure_univ_ne_zero).mpr hP'0) (by finiteness))
   -- obtain K, a compact and closed set, which covers E up to a small area of measure at most ε
   -- w.r.t. both P and P'
-  obtain ⟨KP, _, hKPco, hKPcl, hKP⟩ := MeasurableSet.exists_isCompact_isClosed_diff_lt
-    (MeasurableSet.univ) (measure_ne_top P Set.univ) (ofReal_pos.mpr hε).ne'
-  obtain ⟨KP', _, hKP'co, hKP'cl, hKP'⟩ := MeasurableSet.exists_isCompact_isClosed_diff_lt
-    (MeasurableSet.univ) (measure_ne_top P' Set.univ) (ofReal_pos.mpr hε).ne'
-  let K := KP ∪ KP'
-  have hKco := IsCompact.union hKPco hKP'co
-  have hKcl := IsClosed.union hKPcl hKP'cl
-  simp only [← Set.compl_eq_univ_diff] at hKP hKP'
-  have hKPbound : P (KP ∪ KP')ᶜ < ε.toNNReal := lt_of_le_of_lt
-        (measure_mono (Set.compl_subset_compl_of_subset (Set.subset_union_left))) hKP
-  have hKP'bound : P' (KP ∪ KP')ᶜ < ε.toNNReal := lt_of_le_of_lt
-        (measure_mono (Set.compl_subset_compl_of_subset (Set.subset_union_right))) hKP'
+  obtain ⟨K, _, hKco, hKcl, hK⟩ := MeasurableSet.exists_isCompact_isClosed_diff_lt
+    (μ := P + P') (MeasurableSet.univ) (measure_ne_top (P + P') Set.univ) (ofReal_pos.mpr hε).ne'
+  simp only [← Set.compl_eq_univ_diff] at hK
+  have hKPbound : P Kᶜ < ε.toNNReal :=
+    lt_of_le_of_lt ((Measure.le_add_right (ν := P) (ν' := P') le_rfl) _) hK
+  have hKP'bound : P' Kᶜ < ε.toNNReal :=
+    lt_of_le_of_lt ((Measure.le_add_left (ν := P') (ν' := P) le_rfl) _) hK
   -- Stone-Weierstrass approximation of f on K
   obtain ⟨g', hg'A, hg'approx⟩ :=
       ContinuousMap.exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints
diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
index b87c2190a169b8..d632e86a22a4bd 100644
--- a/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
@@ -53,18 +53,13 @@ theorem cpow_eq_nhds' {p : ℂ × ℂ} (hp_fst : p.fst ≠ 0) :
     this.mono fun x hx ↦ by
       dsimp only
       rw [cpow_def_of_ne_zero hx]
-  refine IsOpen.eventually_mem ?_ hp_fst
-  change IsOpen { x : ℂ × ℂ | x.1 = 0 }ᶜ
-  rw [isOpen_compl_iff]
-  exact isClosed_eq continuous_fst continuous_const
+  exact (isOpen_ne.preimage continuous_fst).eventually_mem hp_fst
 
 -- Continuity of `fun x => a ^ x`: union of these two lemmas is optimal.
 theorem continuousAt_const_cpow {a b : ℂ} (ha : a ≠ 0) : ContinuousAt (fun x : ℂ => a ^ x) b := by
-  have cpow_eq : (fun x : ℂ => a ^ x) = fun x => exp (log a * x) := by
-    ext1 b
-    rw [cpow_def_of_ne_zero ha]
-  rw [cpow_eq]
-  exact continuous_exp.continuousAt.comp (ContinuousAt.mul continuousAt_const continuousAt_id)
+  simpa [cpow_def_of_ne_zero ha] using
+    (Complex.continuous_exp.continuousAt.comp
+      (ContinuousAt.mul continuousAt_const continuousAt_id))
 
 theorem continuousAt_const_cpow' {a b : ℂ} (h : b ≠ 0) : ContinuousAt (fun x : ℂ => a ^ x) b := by
   by_cases ha : a = 0
@@ -345,12 +340,9 @@ theorem continuousAt_ofReal_cpow (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0)
     refine (continuousAt_cpow (Or.inl ?_)).comp this
     rwa [ofReal_re]
   · -- x = 0 : reduce to continuousAt_cpow_zero_of_re_pos
-    have A : ContinuousAt (fun p => p.1 ^ p.2 : ℂ × ℂ → ℂ) ⟨↑(0 : ℝ), y⟩ := by
-      rw [ofReal_zero]
-      apply continuousAt_cpow_zero_of_re_pos
-      tauto
-    have B : ContinuousAt (fun p => ⟨↑p.1, p.2⟩ : ℝ × ℂ → ℂ × ℂ) ⟨0, y⟩ := by fun_prop
-    exact A.comp_of_eq B rfl
+    have hcoe : ContinuousAt (fun p : ℝ × ℂ => (↑p.1, p.2) : ℝ × ℂ → ℂ × ℂ) (0, y) := by
+      fun_prop
+    exact (continuousAt_cpow_zero_of_re_pos (z := y) (by tauto)).comp_of_eq hcoe rfl
   · -- x < 0 : difficult case
     suffices ContinuousAt (fun p => (-(p.1 : ℂ)) ^ p.2 * exp (π * I * p.2) : ℝ × ℂ → ℂ) (x, y) by
       refine this.congr (eventually_of_mem (prod_mem_nhds (Iio_mem_nhds hx) univ_mem) ?_)
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
index af25e8269cbe74..a9b844a4d204ea 100644
--- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
+++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
@@ -545,12 +545,7 @@ theorem abs_toReal_coe_eq_self_iff {θ : ℝ} : |(θ : Angle).toReal| = θ ↔ 0
       abs_eq_self.2 h.1⟩
 
 theorem abs_toReal_neg_coe_eq_self_iff {θ : ℝ} : |(-θ : Angle).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π := by
-  refine ⟨fun h => h ▸ ⟨abs_nonneg _, abs_toReal_le_pi _⟩, fun h => ?_⟩
-  by_cases hnegpi : θ = π; · simp [hnegpi, Real.pi_pos.le]
-  rw [← coe_neg,
-    toReal_coe_eq_self_iff.2
-      ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩,
-    abs_neg, abs_eq_self.2 h.1]
+  simpa [coe_neg] using (abs_toReal_coe_eq_self_iff (θ := θ))
 
 theorem abs_toReal_eq_pi_div_two_iff {θ : Angle} :
     |θ.toReal| = π / 2 ↔ θ = (π / 2 : ℝ) ∨ θ = (-π / 2 : ℝ) := by
@@ -862,15 +857,12 @@ theorem two_zsmul_eq_iff_eq {a b : Real.Angle} (ha : a.sign ≠ 0) (h : a.sign =
     (2 : ℤ) • a = (2 : ℤ) • b ↔ a = b := by
   rw [Real.Angle.two_zsmul_eq_iff]
   constructor
-  · intro h
-    rcases h with h1 | h2
-    · exact h1
-    · have : a.sign = (b + π).sign := by aesop
-      rw [Real.Angle.sign_add_pi] at this
-      have := congr_arg (· = b.sign) this
-      aesop
-  · intro h
-    aesop
+  · intro h'
+    have hb : b.sign ≠ 0 := by simpa [h] using ha
+    exact h'.resolve_right <| by
+      simpa [sub_eq_iff_eq_add, add_comm] using sub_ne_pi_of_sign_eq_of_sign_ne_zero a b h hb
+  · rintro rfl
+    exact Or.inl rfl
 
 lemma abs_toReal_add_abs_toReal_eq_pi_of_two_nsmul_add_eq_zero_of_sign_eq {θ ψ : Angle}
     (h : (2 : ℕ) • (θ + ψ) = 0) (hs : θ.sign = ψ.sign) (h0 : θ.sign ≠ 0) :