mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case succ
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
hzero : f z₀ = 0
n : ℕ
h : ∀ i < n, iteratedDeriv (i + 1) f z₀ = 0
k : ℕ
hk : k + 1 < n + 1
⊢ iteratedDeriv (k + 1) f z₀ = 0

Tactic:
exact h k <| by lia

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ball x δ
this :
  ∀
    p ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s) ×ˢ
        closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s),
    ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
y : E
y_in : y ∈ B ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ‖f y - f x - (f' y - f' x)‖ ≤ ε * ‖y - x‖

Tactic:
apply this ⟨x, y⟩

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
hx : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
δ : ℝ
δ_pos : δ > 0
hδ : ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε
B : Set E := ⋯
this :
  ∀
    p ∈
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s) ×ˢ
        closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s),
    ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖
y : E
y_in : y ∈ B ∩ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ (x, y) ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s) ×ˢ
      closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B ∩ s)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
⊢ AnalyticAt 𝕜 f y

Tactic:
have := ((analyticAt_id (𝕜 := 𝕜).sub analyticAt_const).pow n).inv
      (pow_ne_zero _ (sub_ne_zero_of_ne hy))

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
x : 𝕜
inst✝ : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ n • f z) y
this : AnalyticAt 𝕜 ((_root_.id - fun x_1 ↦ x) ^ n)⁻¹ y
⊢ AnalyticAt 𝕜 f y
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: r : ℤ
k : ℕ
⊢ k.factorial • r.multichoose k = (ascPochhammer ℕ k).smeval r

Tactic:
Int.multichoose.eq_def,

Goal state after:
r : ℤ
k : ℕ
⊢ (k.factorial •
      match r with
      | ofNat n => ↑((n + k - 1).choose k)
      | -[n+1] => ↑(↑k).negOnePow * ↑((n + 1).choose k)) =
    (ascPochhammer ℕ k).smeval r
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case succ
a : ℂ
B : Set ℂ := ⋯
n : ℕ
ih :
  Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n))
    B
this✝ :
  iteratedDerivWithin (n + 1) (fun x ↦ (1 + x) ^ a) B = derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B
this :
  Set.EqOn (derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B
z : ℂ
hz : z ∈ B
⊢ ‖z‖ < 1

Tactic:
simpa [B] using hz

Goal state after:
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: X : Type u_3
inst✝ : EMetricSpace X
s : Set X
⊢ IsSeparated 0 s

Tactic:
by
  simp [IsSeparated, Set.Pairwise]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : EReal
⊢ x.exp.log = x

Tactic:
induction x
  · simp
  · rw [exp_coe, log_ofReal, if_neg (not_le.mpr (Real.exp_pos _)), Real.log_exp]
  · simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : EReal
y : ℝ
⊢ (x * ↑y).exp = x.exp ^ y

Tactic:
by
  rw [← log_eq_iff, log_rpow, log_exp, log_exp, mul_comm]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ (∞ ^ y).log = ↑y * ∞.log

Tactic:
ENNReal.top_rpow_of_pos y_pos,

Goal state after:
case inr.inr.inr.inl
y : ℝ
y_pos : 0 < y
⊢ ∞.log = ↑y * ∞.log
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthInf (u + v) ≤ linearGrowthInf u + linearGrowthSup v

Tactic:
rw [add_comm u v, add_comm (linearGrowthInf u) (linearGrowthSup v)]

Goal state after:
u v : ℕ → EReal
h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthInf (v + u) ≤ linearGrowthSup v + linearGrowthInf u
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ linearGrowthInf u + linearGrowthSup v ≤ linearGrowthSup (u + v)

Tactic:
rw [add_comm u v, add_comm (linearGrowthInf u) (linearGrowthSup v)]

Goal state after:
u v : ℕ → EReal
⊢ linearGrowthSup v + linearGrowthInf u ≤ linearGrowthSup (v + u)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
⊢ a ≤ expGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * ↑n).exp ≤ u n

Tactic:
rw [expGrowthSup, le_limsup_iff']
  refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)
  nth_rw 1 [le_div_iff_mul_le (by norm_cast) (natCast_ne_top n), ← log_exp (b * n)]
  exact logOrderIso.le_iff_le

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)

Tactic:
by
  refine ⟨fun h z => ?_, fun h n => by simpa only [zpow_natCast] using! h (n : ℤ)⟩
  by_cases! hz : 0 ≤ z
  · unfold Tendsto
    lift z to ℕ using hz
    simpa using! h z
  · have : Tendsto (fun a => k a ^ z) l (𝓝 0) :=
      Tendsto.comp (tendsto_zpow_atTop_zero hz) hk
    have h : Tendsto f l (𝓝 0) := by simpa using! h 0
    exact zero_mul (0 : β) ▸ this.mul h

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: a b : ℝ
h : a < b
⊢ ∀ᶠ (x : ℝ) in atTop, ∃ n, a * x ≤ ↑n ∧ ↑n ≤ b * x

Tactic:
refine (eventually_ge_atTop (b - a)⁻¹).mono fun x ab_x ↦ ?_
  rw [inv_le_iff_one_le_mul₀ (sub_pos_of_lt h), mul_comm, sub_mul, le_sub_iff_add_le'] at ab_x
  exact ⟨_, le_of_add_le_add_right (ab_x.trans (Int.lt_floor_add_one _).le), Int.floor_le _⟩

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * ↑(v a) ≤ u (v a)
n : ℕ
b_uvn : b * ↑(v n) ≤ u (v n)
a_vn : a < ↑(v n) / ↑n
n_0 : 0 < n
⊢ a * b * ↑n ≤ (u ∘ v) n

Tactic:
replace a_vn := ((lt_div_iff (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 a_vn).le

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * ↑(v a) ≤ u (v a)
n : ℕ
b_uvn : b * ↑(v n) ≤ u (v n)
n_0 : 0 < n
a_vn : a * ↑n ≤ ↑(v n)
⊢ a * b * ↑n ≤ (u ∘ v) n
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: b : ℝ≥0∞
⊢ (expGrowthSup fun n ↦ b ^ n) = b.log

Tactic:
rw [expGrowthSup, ← limsup_const (f := atTop (α := ℕ)) (log b)]

Goal state after:
b : ℝ≥0∞
⊢ limsup (fun n ↦ (b ^ n).log / ↑n) atTop = limsup (fun x ↦ b.log) atTop
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
⊢ expGrowthSup u⁻¹ = -expGrowthInf u

Tactic:
by
  rw [expGrowthInf, ← limsup_neg]
  refine limsup_congr (Eventually.of_forall fun n ↦ ?_)
  rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case neg.inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : (B c ∩ B b).Nonempty
H : ∀ d ∈ u, Disjoint (B c) (B d)
H' : b ∈ u
⊢ ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1

Tactic:
← not_disjoint_iff_nonempty_inter

Goal state after:
case neg.inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
a' : ι
a'A : a' ∈ A
ha' : m / τ ≤ δ a'
a'_ne_u : a' ∉ u
c : ι
ct : c ∈ t
b : ι
ba'u : b ∈ insert a' u
hcb : ¬Disjoint (B c) (B b)
H : ∀ d ∈ u, Disjoint (B c) (B d)
H' : b ∈ u
⊢ ∃ c_1 ∈ insert a' u, (B c ∩ B c_1).Nonempty ∧ δ c ≤ τ * δ c_1
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hs₀ : μ s ≠ 0
ht₀ : μ t ≠ 0
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in t, f x ∂μ)

Tactic:
refine
    ⟨μ s / (μ s + μ t), μ t / (μ s + μ t), ENNReal.div_pos hs₀ <| add_ne_top.2 ⟨hsμ, htμ⟩,
      ENNReal.div_pos ht₀ <| add_ne_top.2 ⟨hsμ, htμ⟩, ?_, (laverage_union hd ht).symm⟩
  rw [← ENNReal.add_div,
    ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
u : Set α
hu : MeasurableSet u
huμ : (μ.restrict (s ∪ t)) u < ∞
⊢ ∫⁻ (x : α) in u, f x ∂μ.restrict (s ∪ t) = ∫⁻ (x : α) in u, g x ∂μ.restrict (s ∪ t)

Tactic:
Measure.restrict_restrict hu

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
u : Set α
hu : MeasurableSet u
huμ : (μ.restrict (s ∪ t)) u < ∞
⊢ ∫⁻ (x : α) in u ∩ (s ∪ t), f x ∂μ = ∫⁻ (x : α) in u ∩ (s ∪ t), g x ∂μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν

Tactic:
· rw [singularPart, singularPart, dif_neg hl, dif_neg]
    refine fun hl' ↦ hl ?_
    rw [← inv_smul_smul₀ hr ν]
    infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case hfi
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝⁴ : IsFiniteMeasure ν₁
inst✝³ : IsFiniteMeasure ν₂
inst✝² : ν₁.HaveLebesgueDecomposition μ
inst✝¹ : ν₂.HaveLebesgueDecomposition μ
inst✝ : (ν₁ + ν₂).HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), (ν₁ + ν₂).rnDeriv μ x ∂μ ≠ ∞

Tactic:
exact (lintegral_rnDeriv_lt_top (ν₁ + ν₂) μ).ne

Goal state after:
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x y : α
r : ℝ
h : dist x y ≤ K * r
rpos : 0 < r
⊢ closedBall y r ∈ (vitaliFamily μ K).setsAt x

Tactic:
by
  let R := scalingScaleOf μ (max (4 * K + 3) 3)
  simp only [vitaliFamily, VitaliFamily.enlarge, Vitali.vitaliFamily, mem_union, mem_ofPred_eq,
    isClosed_closedBall, true_and, (nonempty_ball.2 rpos).mono ball_subset_interior_closedBall,
    measurableSet_closedBall]
  /- The measure is doubling on scales smaller than `R`. Therefore, we treat differently small
    and large balls. For large balls, this follows directly from the enlargement we used in the
    definition. -/
  by_cases H : closedBall y r ⊆ closedBall x (R / 4)
  swap; · exact Or.inr H
  left
  /- For small balls, there is the difficulty that `r` could be large but still the ball could be
    small, if the annulus `{y | ε ≤ dist y x ≤ R/4}` is empty. We split between the cases `r ≤ R`
    and `r > R`, and use the doubling for the former and rough estimates for the latter. -/
  rcases le_or_gt r R with (hr | hr)
  · refine ⟨(K + 1) * r, ?_⟩
    constructor
    · apply closedBall_subset_closedBall'
      rw [dist_comm]
      linarith
    · have I1 : closedBall x (3 * ((K + 1) * r)) ⊆ closedBall y ((4 * K + 3) * r) := by
        apply closedBall_subset_closedBall'
        linarith
      have I2 : closedBall y ((4 * K + 3) * r) ⊆ closedBall y (max (4 * K + 3) 3 * r) := by
        gcongr
        exact le_max_left ..
      apply (measure_mono (I1.trans I2)).trans
      exact measure_mul_le_scalingConstantOf_mul _
        ⟨zero_lt_three.trans_le (le_max_right _ _), le_rfl⟩ hr
  · refine ⟨_, H, ?_⟩
    grw [scalingConstantOf, ← le_max_right, ENNReal.coe_one, one_mul,
      closedBall_subset_closedBall' (y := y)]
    have A : y ∈ closedBall y r := mem_closedBall_self rpos.le
    have B := mem_closedBall'.1 (H A)
    linarith

Goal state after:
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
⊢ HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x

Tactic:
have L1 : Tendsto (fun y => (f y - f x) / (y - x)) (𝓝[>] x)
      (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by
    -- limit of a helper function, with a small shift compared to `g`
    have : Tendsto (fun y => (hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[>] x)
        (𝓝 (rnDeriv hf.stieltjesFunction.measure volume x).toReal) := by
      apply tendsto_apply_add_mul_sq_div_sub (nhdsGT_le_nhdsNE x) hx.2
      apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
      · apply Tendsto.mono_left _ nhdsWithin_le_nhds
        have : Tendsto (fun y : ℝ => y + -↑1 * (y - x) ^ 2) (𝓝 x) (𝓝 (x + -↑1 * (x - x) ^ 2)) :=
          tendsto_id.add (((tendsto_id.sub_const x).pow 2).const_mul (-1))
        simpa using this
      · filter_upwards [Ioo_mem_nhdsGT <| show x < x + 1 by simp]
        rintro y ⟨hy : x < y, h'y : y < x + 1⟩
        rw [mem_Ioi]
        nlinarith
    -- apply the sandwiching argument, with the helper function and `g`
    apply tendsto_of_tendsto_of_tendsto_of_le_of_le' this hx.2
    · filter_upwards [self_mem_nhdsWithin] with y hy
      rw [mem_Ioi, ← sub_pos] at hy
      gcongr
      exact hf.rightLim_le (by nlinarith)
    · filter_upwards [self_mem_nhdsWithin] with y hy
      rw [mem_Ioi, ← sub_pos] at hy
      gcongr
      exact hf.le_rightLim le_rfl

Goal state after:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y ↦ (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
⊢ HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : b ≤ a
⊢ variationOnFromTo f s a b ≤ 0

Tactic:
rw [variationOnFromTo.eq_neg_swap]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : b ≤ a
⊢ -variationOnFromTo f s b a ≤ 0
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
u_mono : StrictMonoOn u (Iic n)
u_mem : ∀ i ∈ Iic n, u i ∈ s
⊢ MonotoneOn (↑⟨n, ⟨u, ⋯⟩⟩.snd) (Iic ⟨n, ⟨u, ⋯⟩⟩.fst)

Tactic:
grind [MonotoneOn, StrictMonoOn]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = ∞}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : ρ o < ∞
s : Set α := {x | v.limRatioMeas hρ x = ∞} ∩ o
ρs : ρ s ≠ ∞
q : ℝ≥0
hq : 1 ≤ q
⊢ μ s ≤ ρ s * (↑q)⁻¹

Tactic:
← div_eq_mul_inv,

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
x✝ : x ∈ {x | v.limRatioMeas hρ x = ∞}
o : Set α
xo : x ∈ o
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
μo : ρ o < ∞
s : Set α := {x | v.limRatioMeas hρ x = ∞} ∩ o
ρs : ρ s ≠ ∞
q : ℝ≥0
hq : 1 ≤ q
⊢ μ s ≤ ρ s / ↑q
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
⊢ (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff_of_sigmaFinite]

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
⊢ μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)

case hf
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
⊢ AEMeasurable ((r • ν).rnDeriv μ) μ

case hg
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
⊢ AEMeasurable (r • ν.rnDeriv μ) μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.rnDeriv (r • μ) =ᵐ[r • μ] r⁻¹ • ν.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff_of_sigmaFinite]

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)

case hf
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)

case hg
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[singleton '' s] E
⊢ SemicontinuousAt (fun x1 x2 ↦ (fun f ↦ eVariationOn f s) x1 > x2) f

Tactic:
by
  apply @lowerSemicontinuous_aux _ _ _ _ (UniformOnFun α E (s.image singleton)) id (𝓝 f) f s _
  simpa only [UniformOnFun.tendsto_iff_tendstoUniformlyOn, mem_image, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, tendstoUniformlyOn_singleton_iff_tendsto] using! @tendsto_id _ (𝓝 f)

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
⊢ (ν₁ + ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ

Tactic:
rw [← withDensity_eq_iff_of_sigmaFinite]

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)

case hf
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
⊢ AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ

case hg
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst✝² : SigmaFinite ν₁
inst✝¹ : SigmaFinite ν₂
inst✝ : SigmaFinite μ
⊢ AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ