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/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/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`).