mathlib-initiative/mathlib-tactics huggingface dataset:
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:
]

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))
⊢ ∑ 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))

α : 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 ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {∞}) ≤ (t • ν) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
x : α
hx : x ∈ s ∩ f ⁻¹' I
⊢ ↑t * f x ≤ ↑t * f 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ρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
t_ne_zero' : t ≠ 0
t_ne_zero : ↑t ≠ 0
ν : Measure α := μ.withDensity (v.limRatioMeas hρ)
f : α → ℝ≥0∞ := v.limRatioMeas hρ
f_meas : Measurable f
A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0})
B : ρ (s ∩ f ⁻¹' {∞}) ≤ (t • ν) (s ∩ f ⁻¹' {∞})
n : ℤ
I : Set ℝ≥0∞ := Ico (↑t ^ n) (↑t ^ (n + 1))
M : MeasurableSet (s ∩ f ⁻¹' I)
⊢ ∫⁻ (x : α) in s ∩ f ⁻¹' I, ↑t ^ (n + 1) ∂μ ≤ ∫⁻ (x : α) in s ∩ f ⁻¹' I, ↑t * f x ∂μ

Tactic:
by
        apply lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => ?_))
        grw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one, hx.2.1]

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 t : Set α
x✝ : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t }
n : ℕ
u : ℕ → α
hu : Monotone u
ust : ∀ (i : ℕ), u i ∈ s ∪ t
v : ℕ → α
m : ℕ
hv : Monotone v
vst : ∀ (i : ℕ), v i ∈ s ∪ t
huv : ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
N : ℕ
hN : N ∈ Iio m
hs : IsGreatest s (v N)
ht : IsLeast t (v N)
⊢ ∑ i ∈ Finset.Ico 0 N, edist (f (v (i + 1))) (f (v i)) + ∑ i ∈ Finset.Ico N m, edist (f (v (i + 1))) (f (v i)) ≤
    eVariationOn f s + eVariationOn f t

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
x✝ : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s ∪ t }
n : ℕ
u : ℕ → α
hu : Monotone u
ust : ∀ (i : ℕ), u i ∈ s ∪ t
v : ℕ → α
m : ℕ
hv : Monotone v
vst : ∀ (i : ℕ), v i ∈ s ∪ t
huv : ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
N : ℕ
hN : N ∈ Iio m
hs : IsGreatest s (v N)
ht : IsLeast t (v N)
⊢ ∑ i ∈ Finset.Ico 0 N, edist (f (v (i + 1))) (f (v i)) + ∑ i ∈ Finset.Ico N m, edist (f (v (i + 1))) (f (v i)) ≤
    eVariationOn f s + eVariationOn f t
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 α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hb : b ∈ s
A : IsGreatest (s ∩ Icc a b) b
B : IsLeast (s ∩ Icc b c) b
⊢ eVariationOn f (s ∩ Icc a c) = eVariationOn f (s ∩ Icc a c)

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ρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᵐ[μ] v.limRatioMeas hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))

Tactic:
]

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᵐ[μ] v.limRatioMeas hρ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
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ρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᵐ[μ] v.limRatioMeas hρ
a✝¹ : α
a✝ : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a✝¹) (𝓝 (v.limRatioMeas hρ a✝¹))
h'x : ρ.rnDeriv μ a✝¹ = v.limRatioMeas hρ a✝¹
⊢ Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a✝¹) (𝓝 (v.limRatioMeas hρ 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ρ : ρ ≪ μ
A : ρ.rnDeriv μ =ᵐ[μ] v.limRatioMeas hρ
a✝¹ : α
a✝ : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a✝¹) (𝓝 (v.limRatioMeas hρ a✝¹))
h'x : ρ.rnDeriv μ a✝¹ = v.limRatioMeas hρ a✝¹
⊢ Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a✝¹) (𝓝 (v.limRatioMeas hρ a✝¹))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
E✝ : Type u_2
inst✝ : PseudoEMetricSpace E✝
f : α → E✝
s : Set α
E : ℕ → α
hE : Monotone E
n : ℕ
ih :
  (∀ (i : ℕ), 0 < i → i < n → E i ∈ s) →
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E n))
hn : ∀ (i : ℕ), 0 < i → i < n + 1 → E i ∈ s
hn₀ : ¬n = 0
⊢ ∑ x ∈ Finset.range n, eVariationOn f (s ∩ Icc (E x) (E (x + 1))) + eVariationOn f (s ∩ Icc (E n) (E (n + 1))) =
    ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Icc (E i) (E (i + 1))) + eVariationOn f (s ∩ Icc (E n) (E (n + 1)))

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
I : ℕ → α
hI : Monotone I
n i✝ : ℕ
a✝¹ : 0 < i✝
a✝ : i✝ < n
⊢ I 0 ≤ I i✝ ∧ I i✝ ≤ I n

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i✝ : ℕ
a✝¹ : 0 < i✝
a✝ : i✝ < n
⊢ I 0 ≤ I i✝ ∧ I i✝ ≤ I n
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case ha
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i < n
⊢ 0 ≤ i

Tactic:
]

Goal state after:
case ha
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i < n
⊢ 0 ≤ i
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case hb
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i < n
⊢ i + 1 ≤ n

Tactic:
]

Goal state after:
case hb
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i < n
⊢ i + 1 ≤ n
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 α
x y : α
hs : IsGreatest s x
ht : IsLeast t y
hxy : x ≤ y
⊢ eVariationOn f s + eVariationOn f {x, y} + eVariationOn f t = eVariationOn f s + edist (f x) (f y) + eVariationOn f t

pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
x y : α
hs : IsGreatest s x
ht : IsLeast t y
hxy : x ≤ y
⊢ IsLeast {x, y} x

pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
x y : α
hs : IsGreatest s x
ht : IsLeast t y
hxy : x ≤ y
⊢ IsGreatest (s ∪ {x, y}) y

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
x y : α
hs : IsGreatest s x
ht : IsLeast t y
hxy : x ≤ y
⊢ eVariationOn f s + eVariationOn f {x, y} + eVariationOn f t = eVariationOn f s + edist (f x) (f y) + eVariationOn f t

α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
x y : α
hs : IsGreatest s x
ht : IsLeast t y
hxy : x ≤ y
⊢ IsLeast {x, y} x

α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
x y : α
hs : IsGreatest s x
ht : IsLeast t y
hxy : x ≤ y
⊢ IsGreatest (s ∪ {x, y}) y
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) + eVariationOn f {u n, u (n + 1)} =
    ∑ i ∈ Finset.range (n + 1), edist (f (u i)) (f (u (i + 1)))

pp: 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

pp: 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

pp: α : 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)))
⊢ α

Tactic:
]

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.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a ↦ μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1
x : α
hx : Tendsto (fun a ↦ μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 1)
h'x : t.indicator 1 x = 1
⊢ Tendsto (fun a ↦ μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
s : Set α
t : Set α := toMeasurable μ s
A : ∀ᵐ (x : α) ∂μ.restrict s, Tendsto (fun a ↦ μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 (t.indicator 1 x))
B : ∀ᵐ (x : α) ∂μ.restrict s, t.indicator 1 x = 1
x : α
hx : Tendsto (fun a ↦ μ (t ∩ a) / μ a) (v.filterAt x) (𝓝 1)
h'x : t.indicator 1 x = 1
⊢ Tendsto (fun a ↦ μ (s ∩ a) / μ a) (v.filterAt x) (𝓝 1)
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 μ
f : α → ℝ≥0∞
hf : Measurable f
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
ρ : Measure α := μ.withDensity f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
h'x : (μ.withDensity f).rnDeriv μ x = f x
⊢ Tendsto (fun a ↦ (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 ((μ.withDensity f).rnDeriv μ x))

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : Measurable f
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
ρ : Measure α := μ.withDensity f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
h'x : (μ.withDensity f).rnDeriv μ x = f x
⊢ Tendsto (fun a ↦ (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 ((μ.withDensity f).rnDeriv μ x))
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 μ
f : α → ℝ≥0∞
hf : Measurable f
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
ρ : Measure α := μ.withDensity f
this : IsFiniteMeasure ρ
x : α
hx : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (ρ.rnDeriv μ x))
h'x : (μ.withDensity f).rnDeriv μ x = f x
a : Set α
ha : MeasurableSet a
⊢ ρ a / μ a = (μ.withDensity f) a / μ a

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 μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx : Tendsto (fun a ↦ (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ Tendsto (fun a ↦ (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h'f : ∫⁻ (y : α), f y ∂μ ≠ ∞
A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ∞
x : α
hx : Tendsto (fun a ↦ (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
h'x : f x = AEMeasurable.mk f hf x
⊢ Tendsto (fun a ↦ (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
⊢ ∑ j ∈ Finset.range (n, ⟨u, ⋯⟩).1,
      edist ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - j + 1))) ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - j))) ≤
    eVariationOn f s

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
⊢ ∑ j ∈ Finset.range (n, ⟨u, ⋯⟩).1,
      edist ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - j + 1))) ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - j))) ≤
    eVariationOn f s
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, ⟨u, ⋯⟩).1
⊢ edist ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - x + 1))) ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - x))) =
    edist (f (↑(n, ⟨fun i ↦ φ (u (n - i)), ⋯⟩).2 (x + 1))) (f (↑(n, ⟨fun i ↦ φ (u (n - i)), ⋯⟩).2 x))

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, ⟨u, ⋯⟩).1
⊢ edist ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - x + 1))) ((f ∘ φ) (↑(n, ⟨u, ⋯⟩).2 ((n, ⟨u, ⋯⟩).1 - 1 - x))) =
    edist (f (↑(n, ⟨fun i ↦ φ (u (n - i)), ⋯⟩).2 (x + 1))) (f (↑(n, ⟨fun i ↦ φ (u (n - i)), ⋯⟩).2 x))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, ⟨u, ⋯⟩).1
⊢ edist (f (φ (u (n - 1 - x)))) (f (φ (u (n - 1 - x + 1)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
β : Type u_3
inst✝ : LinearOrder β
f : α → E
s : Set α
t : Set β
φ : β → α
hφ : AntitoneOn φ t
φst : MapsTo φ t s
n : ℕ
u : ℕ → β
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
x : ℕ
hx : x < (n, ⟨u, ⋯⟩).1
⊢ edist (f (φ (u (n - 1 - x)))) (f (φ (u (n - 1 - x + 1)))) = edist (f (φ (u (n - (x + 1))))) (f (φ (u (n - x))))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

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
h✝ : Nonempty β
ψ : α → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo ψ (φ '' t) t
hψ : MonotoneOn ψ (φ '' t)
⊢ eVariationOn (f ∘ φ ∘ ψ) (φ '' t) ≤ eVariationOn (f ∘ φ) t

Tactic:
]

Goal state after:
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
h✝ : Nonempty β
ψ : α → β := Function.invFunOn φ t
ψφs : EqOn (φ ∘ ψ) id (φ '' t)
ψts : MapsTo ψ (φ '' t) t
hψ : MonotoneOn ψ (φ '' t)
⊢ eVariationOn (f ∘ φ ∘ ψ) (φ '' t) ≤ eVariationOn (f ∘ φ) t
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:
]

Goal state after:
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)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case e'_3.a.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
ux : u ≤ x
⊢ φ x ∈ φ '' (t ∩ Icc x y)

Tactic:
]

Goal state after:
case e'_3.a.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
ux : u ≤ x
⊢ φ x ∈ φ '' (t ∩ Icc x y)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

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
⊢ 0 = 0

pp: case inr.hs
α : 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
⊢ (φ '' t ∩ Icc (φ x) (φ y)).Subsingleton

pp: case inr.hs
α : 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
⊢ (t ∩ Icc x y).Subsingleton

Tactic:
]

Goal state after:
case inr.hs
α : 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
⊢ (φ '' t ∩ Icc (φ x) (φ y)).Subsingleton

case inr.hs
α : 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
⊢ (t ∩ Icc x y).Subsingleton