mathlib-initiative/mathlib-tactics huggingface dataset:
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) ≤ eVariationOn f (s ∩ Icc a b)

Tactic:
]

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) ≤ eVariationOn f (s ∩ Icc a b)
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ρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in v.filterAt x, ↑q < ρ a / μ a
a : Set α
ha : ↑q < ρ a / μ a
⊢ ↑q * μ a ≤ ρ a

Tactic:
]

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in v.filterAt x, ↑q < ρ a / μ a
a : Set α
ha : ↑q < ρ a / μ a
⊢ ↑q * μ a ≤ ρ a
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 α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ab : a ≤ b
⊢ (∀ x ∈ s ∩ Icc a b, ∀ y ∈ s ∩ Icc a b, edist (f x) (f y) = 0) ↔
    ∀ ⦃x : α⦄, x ∈ s ∩ Icc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Icc a b → edist (f x) (f y) = 0

Tactic:
]

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

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
⊢ μ = (μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
⊢ μ = (μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2
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 α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ba : b ≤ a
⊢ (∀ x ∈ s ∩ Icc b a, ∀ y ∈ s ∩ Icc b a, edist (f x) (f y) = 0) ↔
    ∀ ⦃x : α⦄, x ∈ s ∩ Icc b a → ∀ ⦃y : α⦄, y ∈ s ∩ Icc b a → edist (f x) (f y) = 0

Tactic:
]

Goal state after:
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 ∩ Icc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Icc a b → edist (f x) (f y) = 0

Tactic:
]

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.VariationOnFromTo

Goal state before:
pp: case inr
α : 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
ba : b ≤ a
⊢ variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Icc b a → ∀ ⦃y : α⦄, y ∈ s ∩ Icc b a → edist (f x) (f y) = 0

Tactic:
]

Goal state after:
case inr
α : 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
ba : b ≤ a
⊢ variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Icc b a → ∀ ⦃y : α⦄, y ∈ s ∩ Icc b a → edist (f x) (f y) = 0
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 α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ variationOnFromTo f s a b ≤ variationOnFromTo f s a b + variationOnFromTo f s b c

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ variationOnFromTo f s a b ≤ variationOnFromTo f s a b + variationOnFromTo f s b c
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 α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
a : α
as : a ∈ s
c : α
cs : c ∈ s
ac : a ≤ c
⊢ variationOnFromTo f s c b ≤ variationOnFromTo f s a c + variationOnFromTo f s c b

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
a : α
as : a ∈ s
c : α
cs : c ∈ s
ac : a ≤ c
⊢ variationOnFromTo f s c b ≤ variationOnFromTo f s a c + variationOnFromTo f s c b
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
as : a ∈ s
bs : b ∈ s
cs : c ∈ s
bc : b ≤ c
⊢ |f c - f b| = |f c - f b|

Tactic:
]

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

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
hξle : ∀ (A : Set α), MeasurableSet A → ∫⁻ (a : α) in A, ξ a ∂ν ≤ μ A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
A : Set α
hA : MeasurableSet A
⊢ μ A = μ A

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
as : a ∈ s
bs : b ∈ s
cs : c ∈ s
bc : b ≤ c
⊢ (edist (f b) (f c)).toReal ≤ (eVariationOn f (s ∩ Icc b c)).toReal

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
as : a ∈ s
bs : b ∈ s
cs : c ∈ s
bc : b ≤ c
⊢ (edist (f b) (f c)).toReal ≤ (eVariationOn f (s ∩ Icc b c)).toReal
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
as : a ∈ s
bs : b ∈ s
cs : c ∈ s
bc : b ≤ c
⊢ variationOnFromTo f s b c = variationOnFromTo f s b c

Tactic:
]

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
p : (n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }
hp :
  ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
    ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))
⊢ ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i)) ≤
    ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))

Tactic:
]

Goal state after:
case a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
n : ℕ
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
p : (n : ℕ) × { u // StrictMonoOn u (Iic n) ∧ ∀ i ∈ Iic n, u i ∈ s }
hp :
  ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
    ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))
⊢ ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i)) ≤
    ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ |f c - f b| ≤ |f c - f b|

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ f c - f b ≤ variationOnFromTo f s a c - variationOnFromTo f s a b

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
bc : b ≤ c
⊢ f c - f b ≤ variationOnFromTo f s a c - variationOnFromTo f s a b
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝¹ : SigmaFinite ν
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (ν (s n) < ∞)
ξ : ℕ → Measure α := fun n ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun n ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
⊢ ξ n ⟂ₘ ν.restrict (s n) + ν.restrict (s n)ᶜ

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝¹ : SigmaFinite ν
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (ν (s n) < ∞)
ξ : ℕ → Measure α := fun n ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun n ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
⊢ ξ n ⟂ₘ ν.restrict (s n) + ν.restrict (s n)ᶜ
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inl
α : 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
⊢ (eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))).toReal = (eVariationOn f (φ '' t ∩ Icc (φ x) (φ y))).toReal

Tactic:
]

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

Goal state before:
pp: case 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 : y ≤ x
⊢ -(eVariationOn f (φ '' t ∩ Icc (φ y) (φ x))).toReal = -(eVariationOn f (φ '' t ∩ Icc (φ y) (φ x))).toReal

Tactic:
]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝¹ : SigmaFinite ν
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (ν (s n) < ∞)
ξ : ℕ → Measure α := fun n ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun n ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
hξ : sum ξ ⟂ₘ ν
⊢ (sum fun n ↦ ξ n + ν.withDensity (f n)) = sum fun n ↦ ξ n + ν.withDensity (f n)

Tactic:
]

Goal state after:
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 α
⊢ ⨆ p, ∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) ≤
    ⨆ p ∈ {p | p.1 ∈ s ∧ p.2 ∈ s ∧ p.1 ≤ p.2}, eVariationOn f (s ∩ Icc p.1 p.2)

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ ⨆ p, ∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i)) ≤
    ⨆ p ∈ {p | p.1 ∈ s ∧ p.2 ∈ s ∧ p.1 ≤ p.2}, eVariationOn f (s ∩ Icc p.1 p.2)
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
H :
  Tendsto (fun x ↦ variationOnFromTo f s a b - variationOnFromTo f s x b) (𝓝[s ∩ Iio b] b)
    (𝓝 (variationOnFromTo f s a b - dist (f b) l))
x : α
hx : x ∈ s ∩ Iio b
⊢ variationOnFromTo f s a x = variationOnFromTo f s a x

Tactic:
]

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
⊢ ↑q * μ s ≤ ρ s

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
⊢ ↑q ≠ 0 ∨ ρ s ≠ 0

Tactic:
]

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
⊢ ↑q * μ s ≤ ρ s

α : 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
⊢ ↑q ≠ 0 ∨ ρ s ≠ 0
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
this : ∀ {x y : α}, x ∈ s → y ∈ s → y ≤ x → edist (f x) (f y) ≤ eVariationOn f s
hxy : ¬y ≤ x
⊢ edist (f y) (f x) ≤ eVariationOn f s

Tactic:
]

Goal state after:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
this : ∀ {x y : α}, x ∈ s → y ∈ s → y ≤ x → edist (f x) (f y) ≤ eVariationOn f s
hxy : ¬y ≤ x
⊢ edist (f y) (f x) ≤ eVariationOn f s
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

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

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

Tactic:
]

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
⊢ μ.withDensity ((↑r • ν).rnDeriv μ) = ↑r • μ.withDensity (ν.rnDeriv μ)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
⊢ Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc x b)).toReal) (𝓝[s ∩ Iio b] b) (𝓝 (edist (f b) l).toReal)

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
⊢ Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc x b)).toReal) (𝓝[s ∩ Iio b] b) (𝓝 (edist (f b) l).toReal)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

Tactic:
]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
h : eVariationOn f s = 0
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s

Tactic:
]

Goal state after:
case mp
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
h : eVariationOn f s = 0
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ edist (f x) (f y) ≤ eVariationOn f s
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0
⊢ r • ν = r • ν

Tactic:
]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
    ∑ i_1 ∈ Finset.range i.1, edist (f (↑i.2 (i_1 + 1))) (f (↑i.2 i_1)) = 0

Tactic:
]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
    ∑ i_1 ∈ Finset.range i.1, edist (f (↑i.2 (i_1 + 1))) (f (↑i.2 i_1)) = 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 α
hf : (f '' s).Subsingleton
⊢ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : (f '' s).Subsingleton
⊢ ∀ x ∈ s, ∀ y ∈ s, 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 : Set α
hf : (f '' s).Subsingleton
x : α
xs : x ∈ s
y : α
ys : y ∈ s
⊢ 0 = 0

Tactic:
]

Goal state after:
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
⊢ (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)

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

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

Tactic:
]

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 • μ)