mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: case hfh
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y ↦ (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x, (f b - f x) / (b - x) ≤ (↑hf.stieltjesFunction (b + -1 * (b - x) ^ 2) - f x) / (b - x)

Tactic:
·

Goal state after:
case hfh
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx :
  Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[<] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal) ∧
    Tendsto (fun b ↦ (↑hf.stieltjesFunction b - f x) / (b - x)) (𝓝[>] x)
      (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
h'x : ¬¬ContinuousAt f x
A : ↑hf.stieltjesFunction x = f x
L1 : Tendsto (fun y ↦ (f y - f x) / (y - x)) (𝓝[>] x) (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
this :
  Tendsto (fun y ↦ (↑hf.stieltjesFunction (y + -1 * (y - x) ^ 2) - f x) / (y - x)) (𝓝[<] x)
    (𝓝 (hf.stieltjesFunction.measure.rnDeriv volume x).toReal)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x, (f b - f x) / (b - x) ≤ (↑hf.stieltjesFunction (b + -1 * (b - x) ^ 2) - f x) / (b - x)
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 α
a b : α
ab : a < b
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

pp: case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ variationOnFromTo f s a a = -variationOnFromTo f s a a

pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ba : b < a
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ab : a < b
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ variationOnFromTo f s a a = -variationOnFromTo f s a a

pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ba : b < a
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a : α
⊢ variationOnFromTo f s a a = -variationOnFromTo f s a a
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ba : b < a
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
ba : b < a
⊢ variationOnFromTo f s a b = -variationOnFromTo f s b a
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : a ≤ b
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal

pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : ¬a ≤ b
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : a ≤ b
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : ¬a ≤ b
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : ¬a ≤ b
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
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 : BoundedVariationOn f s
a b : α
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal

Tactic:
by
  by_cases hab : a ≤ b
  · simp only [variationOnFromTo, hab, ↓reduceIte, ENNReal.abs_toReal]
    exact ENNReal.toReal_mono hf (eVariationOn.mono _ inter_subset_left)
  · simp only [variationOnFromTo, hab, ↓reduceIte, abs_neg, ENNReal.abs_toReal]
    exact ENNReal.toReal_mono hf (eVariationOn.mono _ inter_subset_left)

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ ∀ {a b : α}, a ∈ s → b ∈ s → variationOnFromTo f s a b + variationOnFromTo f s b a = 0

pp: case refine_2
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ ∀ {a b c : α},
    a ≤ b →
      b ≤ c → a ∈ s → b ∈ s → c ∈ s → variationOnFromTo f s a c = variationOnFromTo f s a b + variationOnFromTo f s b c

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ ∀ {a b : α}, a ∈ s → b ∈ s → variationOnFromTo f s a b + variationOnFromTo f s b a = 0
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ ∀ {a b c : α},
    a ≤ b →
      b ≤ c → a ∈ s → b ∈ s → c ∈ s → variationOnFromTo f s a c = variationOnFromTo f s a b + variationOnFromTo f s b c

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ ∀ {a b c : α},
    a ≤ b →
      b ≤ c → a ∈ s → b ∈ s → c ∈ s → variationOnFromTo f s a c = variationOnFromTo f s a b + variationOnFromTo f s b c
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
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hnm : n ≤ m
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

pp: case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hmn : m ≤ n
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
m n : ℕ
u : ℕ → α
hu : MonotoneOn u (Icc m n)
us : ∀ i ∈ Icc m n, u i ∈ s
hnm : n ≤ m
⊢ ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
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 c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ variationOnFromTo f s a c + variationOnFromTo f s c b - variationOnFromTo f s a c = variationOnFromTo f s c b

Tactic:
add_sub_cancel_left

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
⊢ variationOnFromTo f s c b = variationOnFromTo f s c b
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
h : variationOnFromTo f s a b = 0
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
    LocallyBoundedVariationOn f s →
      ∀ {a b : α}, a ∈ s → b ∈ s → variationOnFromTo f s a b = 0 → a ≤ b → edist (f a) (f b) = 0
h' : ¬a ≤ b
⊢ edist (f a) (f b) = 0

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

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
h : variationOnFromTo f s a b = 0
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
    LocallyBoundedVariationOn f s →
      ∀ {a b : α}, a ∈ s → b ∈ s → variationOnFromTo f s a b = 0 → a ≤ b → edist (f a) (f b) = 0
h' : ¬a ≤ b
⊢ edist (f a) (f b) = 0
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 α
⊢ eVariationOn f s ≤ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))

pp: case a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i)) ≤ eVariationOn f s

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ eVariationOn f s ≤ ⨆ 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 α✝
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:
·

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

Goal state before:
pp: case succ.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv : ↑⟨m, ⟨v, ⋯⟩⟩.snd ⟨m, ⟨v, ⋯⟩⟩.fst = u n
h'v :
  ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
    ∑ i ∈ Finset.range ⟨m, ⟨v, ⋯⟩⟩.fst, edist (f (↑⟨m, ⟨v, ⋯⟩⟩.snd (i + 1))) (f (↑⟨m, ⟨v, ⋯⟩⟩.snd i))
hn : u n = u (n + 1)
⊢ ∃ a a_1,
    a_1 a = u (n + 1) ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) + edist (f (u (n + 1))) (f (u n)) =
          ∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x))

pp: case succ.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv : ↑⟨m, ⟨v, ⋯⟩⟩.snd ⟨m, ⟨v, ⋯⟩⟩.fst = u n
h'v :
  ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
    ∑ i ∈ Finset.range ⟨m, ⟨v, ⋯⟩⟩.fst, edist (f (↑⟨m, ⟨v, ⋯⟩⟩.snd (i + 1))) (f (↑⟨m, ⟨v, ⋯⟩⟩.snd i))
hn : u n < u (n + 1)
⊢ ∃ a a_1,
    a_1 a = u (n + 1) ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) + edist (f (u (n + 1))) (f (u n)) =
          ∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x))

Tactic:
·

Goal state after:
case succ.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv : ↑⟨m, ⟨v, ⋯⟩⟩.snd ⟨m, ⟨v, ⋯⟩⟩.fst = u n
h'v :
  ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
    ∑ i ∈ Finset.range ⟨m, ⟨v, ⋯⟩⟩.fst, edist (f (↑⟨m, ⟨v, ⋯⟩⟩.snd (i + 1))) (f (↑⟨m, ⟨v, ⋯⟩⟩.snd i))
hn : u n = u (n + 1)
⊢ ∃ a a_1,
    a_1 a = u (n + 1) ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) + edist (f (u (n + 1))) (f (u n)) =
          ∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case succ.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv : ↑⟨m, ⟨v, ⋯⟩⟩.snd ⟨m, ⟨v, ⋯⟩⟩.fst = u n
h'v :
  ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
    ∑ i ∈ Finset.range ⟨m, ⟨v, ⋯⟩⟩.fst, edist (f (↑⟨m, ⟨v, ⋯⟩⟩.snd (i + 1))) (f (↑⟨m, ⟨v, ⋯⟩⟩.snd i))
hn : u n < u (n + 1)
⊢ ∃ a a_1,
    a_1 a = u (n + 1) ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) + edist (f (u (n + 1))) (f (u n)) =
          ∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x))

Tactic:
·

Goal state after:
case succ.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
u : ℕ → α
u_mono : Monotone u
u_mem : ∀ (i : ℕ), u i ∈ s
n m : ℕ
v : ℕ → α
v_mono : StrictMonoOn v (Iic m)
v_mem : ∀ i ∈ Iic m, v i ∈ s
hv : ↑⟨m, ⟨v, ⋯⟩⟩.snd ⟨m, ⟨v, ⋯⟩⟩.fst = u n
h'v :
  ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) =
    ∑ i ∈ Finset.range ⟨m, ⟨v, ⋯⟩⟩.fst, edist (f (↑⟨m, ⟨v, ⋯⟩⟩.snd (i + 1))) (f (↑⟨m, ⟨v, ⋯⟩⟩.snd i))
hn : u n < u (n + 1)
⊢ ∃ a a_1,
    a_1 a = u (n + 1) ∧
      (StrictMonoOn a_1 (Iic a) ∧ ∀ i ≤ a, a_1 i ∈ s) ∧
        ∑ x ∈ Finset.range n, edist (f (u (x + 1))) (f (u x)) + edist (f (u (n + 1))) (f (u n)) =
          ∑ x ∈ Finset.range a, edist (f (a_1 (x + 1))) (f (a_1 x))
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 ξ
⊢ μ = (μ₁, ξ).1 + ν.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 ξ
⊢ μ = (μ₁, ξ).1 + ν.withDensity (μ₁, ξ).2
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

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 ∩ uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ uIcc 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 ∩ uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ uIcc 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 ∩ uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ uIcc a b → 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 ∩ uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ uIcc a b → edist (f x) (f y) = 0
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 a b + variationOnFromTo f s b c - variationOnFromTo f s a b

Tactic:
add_sub_cancel_left

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
⊢ variationOnFromTo f s b c = variationOnFromTo f s b c
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SigmaFinite ν
this : ∀ (μ : Measure α) [SFinite μ], IsFiniteMeasure μ → μ.HaveLebesgueDecomposition ν
hμ : ¬IsFiniteMeasure μ
⊢ μ.HaveLebesgueDecomposition ν

pp: α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝¹ : SigmaFinite ν
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
·

Goal state after:
case inr
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SFinite μ
inst✝ : SigmaFinite ν
this : ∀ (μ : Measure α) [SFinite μ], IsFiniteMeasure μ → μ.HaveLebesgueDecomposition ν
hμ : ¬IsFiniteMeasure μ
⊢ μ.HaveLebesgueDecomposition ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝¹ : SigmaFinite ν
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
set s : ℕ → Set α := disjointed (spanningSets ν)

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst✝¹ : SigmaFinite ν
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
⊢ μ.HaveLebesgueDecomposition ν
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 α
⊢ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i)) ≤ eVariationOn f s

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
⊢ ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i)) ≤ eVariationOn f s
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
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

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
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

Tactic:
·

Goal state after:
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
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
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
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)

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
x y : β
hx : x ∈ t
hy : y ∈ t
h : y ≤ x
⊢ variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ 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
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 x) (f y) ≤ eVariationOn f s

pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
hxy : y ≤ x
⊢ edist (f x) (f y) ≤ 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 x) (f y) ≤ eVariationOn f s