mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case 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 : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
⊢ ∃ a' ∈ A, m / τ ≤ δ a'

Tactic:
rcases exists_lt_of_lt_csSup (Anonempty.image _) I with ⟨x, xA, hx⟩

Goal state after:
case 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 : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
x : ℝ
xA : x ∈ δ '' A
hx : m / τ < x
⊢ ∃ a' ∈ A, m / τ ≤ δ a'
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u

Tactic:
have hv₁ : 0 < liminf (fun n ↦ (v n : EReal) / n) atTop := by
    rw [← hv.liminf_eq] at ha
    exact ha.symm.lt_of_le (linearGrowthInf_natCast_nonneg v)

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u
Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
s t : Set α
ht : MeasurableSet t
⊢ ↑((μ (s ∩ t)).toNNReal + (μ (s \ t)).toNNReal) - ↑((ν (s ∩ t)).toNNReal + (ν (s \ t)).toNNReal) =
    ↑(μ (s \ t)).toNNReal - ↑(ν (s \ t)).toNNReal + (↑(μ (s ∩ t)).toNNReal - ↑(ν (s ∩ t)).toNNReal)

Tactic:
NNReal.coe_add,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
d : Set α → ℝ := fun s ↦ ↑(μ s).toNNReal - ↑(ν s).toNNReal
c : Set ℝ := d '' {s | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), μ s ≠ ∞
hν : ∀ (s : Set α), ν s ≠ ∞
to_nnreal_μ : ∀ (s : Set α), ↑(μ s).toNNReal = μ s
to_nnreal_ν : ∀ (s : Set α), ↑(ν s).toNNReal = ν s
s t : Set α
ht : MeasurableSet t
⊢ ↑(μ (s ∩ t)).toNNReal + ↑(μ (s \ t)).toNNReal - ↑((ν (s ∩ t)).toNNReal + (ν (s \ t)).toNNReal) =
    ↑(μ (s \ t)).toNNReal - ↑(ν (s \ t)).toNNReal + (↑(μ (s ∩ t)).toNNReal - ↑(ν (s ∩ t)).toNNReal)
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u

Tactic:
have hv₁ : 0 < liminf (fun n ↦ (v n : EReal) / n) atTop := by
    rw [← hv.liminf_eq] at ha
    exact ha.symm.lt_of_le (linearGrowthInf_natCast_nonneg v)

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun n ↦ ↑(v n) / ↑n) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : 0 < liminf (fun n ↦ ↑(v n) / ↑n) atTop
⊢ linearGrowthSup (u ∘ v) = a * linearGrowthSup u
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
this : f =ᵐ[μ.restrict (s ∪ t)] g
h1 : f =ᵐ[μ.restrict sᶜ] 0
h2 : g =ᵐ[μ.restrict tᶜ] 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x

Tactic:
EventuallyEq,

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
this : f =ᵐ[μ.restrict (s ∪ t)] g
h1 : ∀ᵐ (x : α) ∂μ.restrict sᶜ, f x = 0 x
h2 : g =ᵐ[μ.restrict tᶜ] 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x
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
this : f =ᵐ[μ.restrict (s ∪ t)] g
h1 : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : g =ᵐ[μ.restrict tᶜ] 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x

Tactic:
EventuallyEq,

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
this : f =ᵐ[μ.restrict (s ∪ t)] g
h1 : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : ∀ᵐ (x : α) ∂μ.restrict tᶜ, g x = 0 x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
⊢ ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0

Tactic:
have u_count : u.Countable := u_disj.countable_of_nonempty_interior fun a ha => ht a (ut ha)

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set ι
C : ℝ≥0
r : ι → ℝ
c : ι → α
B : ι → Set α
hB : ∀ a ∈ t, B a ⊆ closedBall (c a) (r a)
μB : ∀ a ∈ t, μ (closedBall (c a) (3 * r a)) ≤ ↑C * μ (B a)
ht : ∀ a ∈ t, (interior (B a)).Nonempty
h't : ∀ a ∈ t, IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B a)
hf : ∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x
R : α → ℝ
hR0 : ∀ (x : α), 0 < R x
hR1 : ∀ (x : α), R x ≤ 1
hRμ : ∀ (x : α), μ (closedBall x (20 * R x)) < ∞
t' : Set ι := {a | a ∈ t ∧ r a ≤ R (c a)}
u : Set ι
ut' : u ⊆ t'
u_disj : u.PairwiseDisjoint B
hu : ∀ a ∈ t', ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ r a ≤ 2 * r b
ut : u ⊆ t
u_count : u.Countable
⊢ ∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ μ (s \ ⋃ a ∈ u, B a) = 0
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
⊢ f =ᵐ[μ] g

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf hg fun s hs _ ↦ ?_
    rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
by_cases h : HaveLebesgueDecomposition μ ν
  · exact (haveLebesgueDecomposition_spec μ ν).2.1
  · rw [singularPart_of_not_haveLebesgueDecomposition h]
    exact MutuallySingular.zero_left

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

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

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

Tactic:
· refine (eq_singularPart ((measurable_rnDeriv μ ν).const_smul r⁻¹) ?_ ?_).symm
    · exact (mutuallySingular_singularPart μ ν).mono_ac AbsolutelyContinuous.rfl
        smul_absolutelyContinuous
    · rw [ENNReal.smul_def r, withDensity_smul_measure, ← withDensity_smul]
      swap; · exact (measurable_rnDeriv _ _).const_smul _
      convert! haveLebesgueDecomposition_add μ ν
      ext x
      simp only [Pi.smul_apply]
      rw [← ENNReal.smul_def, smul_inv_smul₀ hr]

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
L0 : Tendsto (fun i ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)
⊢ Tendsto (fun i ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)

Tactic:
have := L0.add (hg.smul_const c)

Goal state after:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (fun i ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (fun i ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I : ∀ᶠ (i : ι) in l, ∫ (y : α), g i y • (f y - c) ∂μ + (∫ (y : α), g i y ∂μ) • c = ∫ (y : α), g i y • f y ∂μ
L0 : Tendsto (fun i ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)
this : Tendsto (fun x ↦ ∫ (y : α), g x y • (f y - c) ∂μ + (∫ (y : α), g x y ∂μ) • c) l (𝓝 (0 + 1 • c))
⊢ Tendsto (fun i ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)
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 : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
⊢ Tendsto (fun j ↦ closedBall (w j) (δ j)) l ((vitaliFamily μ K).filterAt x)

Tactic:
refine (vitaliFamily μ K).tendsto_filterAt_iff.mpr ⟨?_, fun ε hε => ?_⟩
  · filter_upwards [xmem, δlim self_mem_nhdsWithin] with j hj h'j
    exact closedBall_mem_vitaliFamily_of_dist_le_mul μ hj h'j
  · rcases l.eq_or_neBot with rfl | h
    · simp
    have hK : 0 ≤ K := by
      rcases (xmem.and (δlim self_mem_nhdsWithin)).exists with ⟨j, hj, h'j⟩
      have : 0 ≤ K * δ j := nonempty_closedBall.1 ⟨x, hj⟩
      exact (mul_nonneg_iff_left_nonneg_of_pos (mem_Ioi.1 h'j)).1 this
    have δpos := eventually_mem_of_tendsto_nhdsWithin δlim
    replace δlim := tendsto_nhds_of_tendsto_nhdsWithin δlim
    replace hK : 0 < K + 1 := by linarith
    apply (((Metric.tendsto_nhds.mp δlim _ (div_pos hε hK)).and δpos).and xmem).mono
    rintro j ⟨⟨hjε, hj₀ : 0 < δ j⟩, hx⟩ y hy
    replace hjε : (K + 1) * δ j < ε := by
      simpa [abs_eq_self.mpr hj₀.le] using (lt_div_iff₀' hK).mp hjε
    simp only [mem_closedBall] at hx hy ⊢
    linarith [dist_triangle_right y x (w j)]

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

Goal state before:
pp: f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
L1 : Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L2 : Tendsto (fun y ↦ (leftLim (↑f) y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
L3 :
  Tendsto (fun y ↦ (leftLim (↑f) (y + 1 * (y - x) ^ 2) - ↑f x) / (y - x)) (𝓝[<] x)
    (𝓝 (f.measure.rnDeriv volume x).toReal)
L4 : Tendsto (fun y ↦ (↑f y - ↑f x) / (y - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal)
⊢ Tendsto (fun b ↦ (↑f b - ↑f x) / (b - x)) (𝓝[<] x) (𝓝 (f.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑f b - ↑f x) / (b - x)) (𝓝[>] x) (𝓝 (f.measure.rnDeriv volume x).toReal)

Tactic:
exact ⟨L4, L1⟩

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

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
a✝ : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
h'x : x ∈ s ∩ Ioo a b
⊢ f =ᶠ[𝓝[s] x] g

Tactic:
have : Ioo a b ∈ 𝓝[s] x := nhdsWithin_le_nhds (Ioo_mem_nhds h'x.2.1 h'x.2.2)

Goal state after:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
a✝ : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
h'x : x ∈ s ∩ Ioo a b
this : Ioo a b ∈ 𝓝[s] x
⊢ f =ᶠ[𝓝[s] x] g
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 α✝
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
h : variationOnFromTo f s a b = 0
h' : a ≤ b
⊢ edist (f a) (f b) ≤ 0

Tactic:
← ENNReal.ofReal_zero,

Goal state after:
α✝ : Type u_1
inst✝³ : LinearOrder α✝
E✝ : Type u_2
inst✝² : PseudoEMetricSpace E✝
f✝ : α✝ → E✝
s✝ : Set α✝
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
h : variationOnFromTo f s a b = 0
h' : a ≤ b
⊢ edist (f a) (f b) ≤ ENNReal.ofReal 0
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ab : a ≤ b
⊢ variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ uIcc a b → edist (f x) (f y) = 0

Tactic:
rw [uIcc_of_le ab]

Goal state after:
case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ab : a ≤ b
⊢ variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Icc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Icc a b → edist (f x) (f y) = 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 t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : ℕ → α := fun i ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ ∑ x ∈ Finset.range n ∪ Finset.Ico (n + 1) (n + 1 + m), edist (f (w (x + 1))) (f (w x)) ≤
    ∑ i ∈ Finset.range (n + 1 + m), edist (f (w (i + 1))) (f (w i))

pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : ℕ → α := fun i ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ Disjoint (Finset.range n) (Finset.Ico (n + 1) (n + 1 + m))

Tactic:
· gcongr; grind

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y
hs : ¬s = ∅
this✝ : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
ht : ¬t = ∅
this : Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
m : ℕ
v : ℕ → α
hv : Monotone v
vt : ∀ (i : ℕ), v i ∈ t
w : ℕ → α := fun i ↦ if i ≤ n then u i else v (i - (n + 1))
⊢ Disjoint (Finset.range n) (Finset.Ico (n + 1) (n + 1 + m))
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 ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
A : ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ (ρ.singularPart μ) a / μ a) (v.filterAt x) (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x
C : ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ t a / μ a) (v.filterAt x) (𝓝 (t.rnDeriv μ x))
a✝ : α
Ax : Tendsto (fun a ↦ (ρ.singularPart μ) a / μ a) (v.filterAt a✝) (𝓝 0)
Bx : t.rnDeriv μ a✝ = ρ.rnDeriv μ a✝
Cx : Tendsto (fun a ↦ t a / μ a) (v.filterAt a✝) (𝓝 (t.rnDeriv μ a✝))
⊢ Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a✝) (𝓝 (ρ.rnDeriv μ a✝))

Tactic:
convert! Ax.add Cx using 1

Goal state after:
case e'_3
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
A : ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ (ρ.singularPart μ) a / μ a) (v.filterAt x) (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x
C : ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ t a / μ a) (v.filterAt x) (𝓝 (t.rnDeriv μ x))
a✝ : α
Ax : Tendsto (fun a ↦ (ρ.singularPart μ) a / μ a) (v.filterAt a✝) (𝓝 0)
Bx : t.rnDeriv μ a✝ = ρ.rnDeriv μ a✝
Cx : Tendsto (fun a ↦ t a / μ a) (v.filterAt a✝) (𝓝 (t.rnDeriv μ a✝))
⊢ (fun a ↦ ρ a / μ a) = fun x ↦ (ρ.singularPart μ) x / μ x + t x / μ x

case e'_5
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
t : Measure α := μ.withDensity (ρ.rnDeriv μ)
eq_add : ρ = ρ.singularPart μ + t
A : ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ (ρ.singularPart μ) a / μ a) (v.filterAt x) (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, t.rnDeriv μ x = ρ.rnDeriv μ x
C : ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ t a / μ a) (v.filterAt x) (𝓝 (t.rnDeriv μ x))
a✝ : α
Ax : Tendsto (fun a ↦ (ρ.singularPart μ) a / μ a) (v.filterAt a✝) (𝓝 0)
Bx : t.rnDeriv μ a✝ = ρ.rnDeriv μ a✝
Cx : Tendsto (fun a ↦ t a / μ a) (v.filterAt a✝) (𝓝 (t.rnDeriv μ a✝))
⊢ 𝓝 (ρ.rnDeriv μ a✝) = 𝓝 (0 + t.rnDeriv μ a✝)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n : ℕ
⊢ ∀ (i : ℕ), 0 < i → i < n → I i ∈ Icc (I 0) (I n)

Tactic:
by intros; rw [mem_Icc]; constructor <;> (apply hI; lia)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
u : ℕ → α
hu : Monotone u
n : ℕ
ih : eVariationOn f (u '' Iic n) = ∑ i ∈ Finset.range n, edist (f (u i)) (f (u (i + 1)))
⊢ eVariationOn f (u '' Iic (n + 1)) = ∑ i ∈ Finset.range (n + 1), edist (f (u i)) (f (u (i + 1)))

Tactic:
rw [(by grind : u '' Iic (n + 1) = u '' Iic n ∪ {u n, u (n + 1)}), union f]

Goal state after:
case succ
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
u : ℕ → α
hu : Monotone u
n : ℕ
ih : eVariationOn f (u '' Iic n) = ∑ i ∈ Finset.range n, edist (f (u i)) (f (u (i + 1)))
⊢ eVariationOn f (u '' Iic n) + eVariationOn f {u n, u (n + 1)} =
    ∑ i ∈ Finset.range (n + 1), edist (f (u i)) (f (u (i + 1)))

case succ.hs
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
u : ℕ → α
hu : Monotone u
n : ℕ
ih : eVariationOn f (u '' Iic n) = ∑ i ∈ Finset.range n, edist (f (u i)) (f (u (i + 1)))
⊢ IsGreatest (u '' Iic n) ?m.77

case succ.ht
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
u : ℕ → α
hu : Monotone u
n : ℕ
ih : eVariationOn f (u '' Iic n) = ∑ i ∈ Finset.range n, edist (f (u i)) (f (u (i + 1)))
⊢ IsLeast {u n, u (n + 1)} ?m.77

α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
u : ℕ → α
hu : Monotone u
n : ℕ
ih : eVariationOn f (u '' Iic n) = ∑ i ∈ Finset.range n, edist (f (u i)) (f (u (i + 1)))
⊢ α
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case e'_3.a.inl.inr
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
t : Set β
φ : β → α
hφ : MonotoneOn φ t
x y : β
hx : x ∈ t
hy : y ∈ t
h : x ≤ y
u : β
us : u ∈ t
vφx : φ x ≤ φ u
vφy : φ u ≤ φ y
xu : x ≤ u
yu : y ≤ u
⊢ φ y ∈ φ '' (t ∩ Icc x y)

Tactic:
exact ⟨y, ⟨hy, ⟨h, le_rfl⟩⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
E : Type u_2
inst✝³ : PseudoEMetricSpace E
inst✝² : CompleteSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
hf : BoundedVariationOn f univ
x : α
⊢ ∃ y, Tendsto f (𝓝[<] x) (𝓝 y)

Tactic:
convert! hf.exists_tendsto_left x

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
E : Type u_2
inst✝³ : PseudoEMetricSpace E
inst✝² : CompleteSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
hf : BoundedVariationOn f univ
x : α
x✝ : E
⊢ Iio x = univ ∩ Iio x