mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case h₂
α : 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 : ℕ
hi : i ∈ Icc N m
⊢ v i ∈ t

Tactic:
·

Goal state after:
case h₂
α : 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 : ℕ
hi : i ∈ Icc N m
⊢ v i ∈ t
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case pos
α : 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
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))

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
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))

Tactic:
·

Goal state after:
case pos
α : 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
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) = eVariationOn f (s ∩ Icc (E 0) (E (n + 1)))
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
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) =
    eVariationOn f (s ∩ Icc (E 0) (E n)) + eVariationOn f (s ∩ Icc (E n) (E (n + 1)))

pp: case neg.hab
α : 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
⊢ E 0 ≤ E n

pp: case neg.hbc
α : 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
⊢ E n ≤ E (n + 1)

pp: case neg.hb
α : 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
⊢ E n ∈ s

Tactic:
·

Goal state after:
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
⊢ ∑ i ∈ Finset.range (n + 1), eVariationOn f (s ∩ Icc (E i) (E (i + 1))) =
    eVariationOn f (s ∩ Icc (E 0) (E n)) + eVariationOn f (s ∩ Icc (E n) (E (n + 1)))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case neg.hab
α : 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
⊢ E 0 ≤ E n

pp: case neg.hbc
α : 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
⊢ E n ≤ E (n + 1)

pp: case neg.hb
α : 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
⊢ E n ∈ s

Tactic:
·

Goal state after:
case neg.hab
α : 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
⊢ E 0 ≤ E n
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case neg.hbc
α : 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
⊢ E n ≤ E (n + 1)

pp: case neg.hb
α : 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
⊢ E n ∈ s

Tactic:
·

Goal state after:
case neg.hbc
α : 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
⊢ E n ≤ E (n + 1)
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: 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

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

Tactic:
·

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
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case neg.hb
α : 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
⊢ E n ∈ s

Tactic:
·

Goal state after:
case neg.hb
α : 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
⊢ E n ∈ s
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case e'_2.a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i ∈ Finset.range n
⊢ Icc (I i) (I (i + 1)) = Icc (I 0) (I n) ∩ Icc (I i) (I (i + 1))

pp: case e'_3
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n : ℕ
⊢ Icc (I 0) (I n) = Icc (I 0) (I n) ∩ Icc (I 0) (I n)

Tactic:
·

Goal state after:
case e'_2.a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n i : ℕ
hi : i ∈ Finset.range n
⊢ Icc (I i) (I (i + 1)) = Icc (I 0) (I n) ∩ Icc (I i) (I (i + 1))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case e'_3
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n : ℕ
⊢ Icc (I 0) (I n) = Icc (I 0) (I n) ∩ Icc (I 0) (I n)

Tactic:
·

Goal state after:
case e'_3
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
I : ℕ → α
hI : Monotone I
n : ℕ
⊢ Icc (I 0) (I n) = Icc (I 0) (I n) ∩ Icc (I 0) (I n)
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
a b : α
this : ∀ (a b : α), a ≤ b → eVariationOn f {a, b} = edist (f a) (f b)
hab : ¬a ≤ b
⊢ eVariationOn f {a, b} = edist (f a) (f b)

pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
⊢ eVariationOn f {a, b} = edist (f a) (f b)

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
this : ∀ (a b : α), a ≤ b → eVariationOn f {a, b} = edist (f a) (f b)
hab : ¬a ≤ b
⊢ eVariationOn f {a, b} = edist (f a) (f b)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
⊢ eVariationOn f {a, b} = edist (f a) (f b)

Tactic:
·

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
⊢ eVariationOn f {a, b} = edist (f a) (f b)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
u : ℕ → α
hmono : StrictMonoOn u (Iic 0)
hi : ∀ i ∈ Iic 0, u i ∈ {a, b}
⊢ ∑ i ∈ Finset.range ⟨0, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨0, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨0, ⟨u, ⋯⟩⟩.snd i)) ≤ edist (f a) (f b)

pp: case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
u : ℕ → α
hmono : StrictMonoOn u (Iic 1)
hi : ∀ i ∈ Iic 1, u i ∈ {a, b}
⊢ ∑ i ∈ Finset.range ⟨1, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨1, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨1, ⟨u, ⋯⟩⟩.snd i)) ≤ edist (f a) (f b)

pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
n : ℕ
u : ℕ → α
hmono : StrictMonoOn u (Iic n)
hi : ∀ i ∈ Iic n, u i ∈ {a, b}
hn : 2 ≤ n
⊢ ∑ i ∈ Finset.range ⟨n, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n, ⟨u, ⋯⟩⟩.snd i)) ≤ edist (f a) (f b)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
u : ℕ → α
hmono : StrictMonoOn u (Iic 0)
hi : ∀ i ∈ Iic 0, u i ∈ {a, b}
⊢ ∑ i ∈ Finset.range ⟨0, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨0, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨0, ⟨u, ⋯⟩⟩.snd i)) ≤ edist (f a) (f b)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
u : ℕ → α
hmono : StrictMonoOn u (Iic 1)
hi : ∀ i ∈ Iic 1, u i ∈ {a, b}
⊢ ∑ i ∈ Finset.range ⟨1, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨1, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨1, ⟨u, ⋯⟩⟩.snd i)) ≤ edist (f a) (f b)

pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
n : ℕ
u : ℕ → α
hmono : StrictMonoOn u (Iic n)
hi : ∀ i ∈ Iic n, u i ∈ {a, b}
hn : 2 ≤ n
⊢ ∑ i ∈ Finset.range ⟨n, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n, ⟨u, ⋯⟩⟩.snd i)) ≤ edist (f a) (f b)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
u : ℕ → α
hmono : StrictMonoOn u (Iic 1)
hi : ∀ i ∈ Iic 1, u i ∈ {a, b}
⊢ ∑ i ∈ Finset.range ⟨1, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨1, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨1, ⟨u, ⋯⟩⟩.snd i)) ≤ edist (f a) (f b)
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: 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✝)

Tactic:
·

Goal state after:
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: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
n : ℕ
u : ℕ → α
hmono : StrictMonoOn u (Iic n)
hi : ∀ i ∈ Iic n, u i ∈ {a, b}
hn : 2 ≤ n
⊢ ∑ i ∈ Finset.range ⟨n, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n, ⟨u, ⋯⟩⟩.snd i)) ≤ edist (f a) (f b)

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
a b : α
hab : a ≤ b
n : ℕ
u : ℕ → α
hmono : StrictMonoOn u (Iic n)
hi : ∀ i ∈ Iic n, u i ∈ {a, b}
hn : 2 ≤ n
⊢ ∑ i ∈ Finset.range ⟨n, ⟨u, ⋯⟩⟩.fst, edist (f (↑⟨n, ⟨u, ⋯⟩⟩.snd (i + 1))) (f (↑⟨n, ⟨u, ⋯⟩⟩.snd i)) ≤ edist (f a) (f b)
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)))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

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

Goal state before:
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)} (u n)

Tactic:
·

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
⊢ BoundedVariationOn f ↑∅

pp: case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
⊢ BoundedVariationOn f ↑s

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
⊢ BoundedVariationOn f ↑∅
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this : 0 < s.card
u : ℕ → α := ⋯
x✝ : α
⊢ (∃ y, (s.orderEmbOfFin ⋯) y = x✝) → ∃ x ≤ s.card - 1, (s.orderEmbOfFin ⋯) ⟨min x (s.card - 1), ⋯⟩ = x✝

pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this : 0 < s.card
u : ℕ → α := ⋯
x✝ : α
⊢ (∃ x ≤ s.card - 1, (s.orderEmbOfFin ⋯) ⟨min x (s.card - 1), ⋯⟩ = x✝) → ∃ y, (s.orderEmbOfFin ⋯) y = x✝

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this : 0 < s.card
u : ℕ → α := ⋯
x✝ : α
⊢ (∃ y, (s.orderEmbOfFin ⋯) y = x✝) → ∃ x ≤ s.card - 1, (s.orderEmbOfFin ⋯) ⟨min x (s.card - 1), ⋯⟩ = x✝
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this : 0 < s.card
u : ℕ → α := ⋯
x✝ : α
⊢ (∃ x ≤ s.card - 1, (s.orderEmbOfFin ⋯) ⟨min x (s.card - 1), ⋯⟩ = x✝) → ∃ y, (s.orderEmbOfFin ⋯) y = x✝

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_3
inst✝ : PseudoMetricSpace E
f : α → E
s : Finset α
hne : s.Nonempty
this : 0 < s.card
u : ℕ → α := ⋯
x✝ : α
⊢ (∃ x ≤ s.card - 1, (s.orderEmbOfFin ⋯) ⟨min x (s.card - 1), ⋯⟩ = x✝) → ∃ y, (s.orderEmbOfFin ⋯) y = x✝