awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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
inr :
  ∀
    (this :
      ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_2 : 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)
    (h' : ¬a ≤ b), edist (f a) (f b) = 0
⊢ edist (f a) (f b) = 0
have wlog : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_2 : 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: wlog h' : a ≤ b
Cleared hypotheses: hf, a, b, ha, hb, h
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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_2 : 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
h' : ¬a ≤ b
⊢ edist (f a) (f b) = 0
have inr : edist (f b) (f a) = 0
Tactic: rw [edist_comm]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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_2 : 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
h' : ¬a ≤ b
⊢ edist (f b) (f a) = 0
have apply : variationOnFromTo f s b a = 0
Tactic: apply this hf hb ha _ (le_of_not_ge h')
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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_2 : 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
h' : ¬a ≤ b
⊢ variationOnFromTo f s b a = 0
have rw : -variationOnFromTo f s a b = 0
Tactic: rw [variationOnFromTo.eq_neg_swap, h, neg_zero]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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_2 : 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
h' : ¬a ≤ b
rw : -variationOnFromTo f s a b = 0
⊢ variationOnFromTo f s b a = 0
have rw₁ : Eq (α := ℝ) (-0) 0
Tactic: rw [variationOnFromTo.eq_neg_swap, h, neg_zero]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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_2 : 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
h' : ¬a ≤ b
rw : -variationOnFromTo f s a b = 0
rw₁ : Eq (α := ℝ) (-0) 0
⊢ variationOnFromTo f s b a = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [variationOnFromTo.eq_neg_swap, h, neg_zero]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f_1 : α_1 → E_1
s_1 : Set α_1
α : Type u_1
inst_2 : LinearOrder α
E : Type u_2
inst_3 : 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
have rw : edist (f a) (f b) ≤ eVariationOn f (s ∩ Icc a b)
Tactic: rw [← nonpos_iff_eq_zero, ← ENNReal.ofReal_zero, ← h, variationOnFromTo.eq_of_le f s h',
      ENNReal.ofReal_toReal (hf a b ha hb)]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f_1 : α_1 → E_1
s_1 : Set α_1
α : Type u_1
inst_2 : LinearOrder α
E : Type u_2
inst_3 : 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)
have hx : a ∈ s ∩ Icc a b
Tactic: apply eVariationOn.edist_le
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α_1 : Type u_1
inst : LinearOrder α_1
E_1 : Type u_2
inst_1 : PseudoEMetricSpace E_1
f_1 : α_1 → E_1
s_1 : Set α_1
α : Type u_1
inst_2 : LinearOrder α
E : Type u_2
inst_3 : 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
hx : a ∈ s ∩ Icc a b
⊢ edist (f a) (f b) ≤ eVariationOn f (s ∩ Icc a b)
have hy : b ∈ s ∩ Icc a b
Tactic: apply eVariationOn.edist_le
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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 : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
have rw : (eVariationOn f (s ∩ Icc a b)).toReal = 0 ↔
  ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
Tactic: rw [variationOnFromTo.eq_of_le _ _ ab, ENNReal.toReal_eq_zero_iff, or_iff_left (hf a b ha hb),
    eVariationOn.eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ab : a ≤ b
rw :
  (eVariationOn f (s ∩ Icc a b)).toReal = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
⊢ variationOnFromTo f s a b = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
have rw₁ : eVariationOn f (s ∩ Icc a b) = 0 ∨ eVariationOn f (s ∩ Icc a b) = ∞ ↔
  ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
Tactic: rw [variationOnFromTo.eq_of_le _ _ ab, ENNReal.toReal_eq_zero_iff, or_iff_left (hf a b ha hb),
    eVariationOn.eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ab : a ≤ b
rw :
  (eVariationOn f (s ∩ Icc a b)).toReal = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
rw₁ :
  eVariationOn f (s ∩ Icc a b) = 0 ∨ eVariationOn f (s ∩ Icc a b) = ∞ ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
⊢ variationOnFromTo f s a b = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
have rw₂ : eVariationOn f (s ∩ Icc a b) = 0 ↔
  ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
Tactic: rw [variationOnFromTo.eq_of_le _ _ ab, ENNReal.toReal_eq_zero_iff, or_iff_left (hf a b ha hb),
    eVariationOn.eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ab : a ≤ b
rw :
  (eVariationOn f (s ∩ Icc a b)).toReal = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
rw₁ :
  eVariationOn f (s ∩ Icc a b) = 0 ∨ eVariationOn f (s ∩ Icc a b) = ∞ ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
rw₂ :
  eVariationOn f (s ∩ Icc a b) = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
⊢ variationOnFromTo f s a b = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
have rw₃ : (∀ x ∈ s ∩ Icc a b, ∀ y ∈ s ∩ Icc a b, edist (f x) (f y) = 0) ↔
  ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
Tactic: rw [variationOnFromTo.eq_of_le _ _ ab, ENNReal.toReal_eq_zero_iff, or_iff_left (hf a b ha hb),
    eVariationOn.eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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 : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
have rw : -(eVariationOn f (s ∩ Icc b a)).toReal = 0 ↔
  ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
Tactic: rw [variationOnFromTo.eq_of_ge _ _ ba, neg_eq_zero, ENNReal.toReal_eq_zero_iff,
    or_iff_left (hf b a hb ha), eVariationOn.eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ba : b ≤ a
rw :
  -(eVariationOn f (s ∩ Icc b a)).toReal = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
⊢ variationOnFromTo f s a b = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
have rw₁ : (eVariationOn f (s ∩ Icc b a)).toReal = 0 ↔
  ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
Tactic: rw [variationOnFromTo.eq_of_ge _ _ ba, neg_eq_zero, ENNReal.toReal_eq_zero_iff,
    or_iff_left (hf b a hb ha), eVariationOn.eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ba : b ≤ a
rw :
  -(eVariationOn f (s ∩ Icc b a)).toReal = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
rw₁ :
  (eVariationOn f (s ∩ Icc b a)).toReal = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
⊢ variationOnFromTo f s a b = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
have rw₂ : eVariationOn f (s ∩ Icc b a) = 0 ∨ eVariationOn f (s ∩ Icc b a) = ∞ ↔
  ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
Tactic: rw [variationOnFromTo.eq_of_ge _ _ ba, neg_eq_zero, ENNReal.toReal_eq_zero_iff,
    or_iff_left (hf b a hb ha), eVariationOn.eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ba : b ≤ a
rw :
  -(eVariationOn f (s ∩ Icc b a)).toReal = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
rw₁ :
  (eVariationOn f (s ∩ Icc b a)).toReal = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
rw₂ :
  eVariationOn f (s ∩ Icc b a) = 0 ∨ eVariationOn f (s ∩ Icc b a) = ∞ ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
⊢ variationOnFromTo f s a b = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
have rw₃ : eVariationOn f (s ∩ Icc b a) = 0 ↔
  ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
Tactic: rw [variationOnFromTo.eq_of_ge _ _ ba, neg_eq_zero, ENNReal.toReal_eq_zero_iff,
    or_iff_left (hf b a hb ha), eVariationOn.eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ba : b ≤ a
rw :
  -(eVariationOn f (s ∩ Icc b a)).toReal = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
rw₁ :
  (eVariationOn f (s ∩ Icc b a)).toReal = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
rw₂ :
  eVariationOn f (s ∩ Icc b a) = 0 ∨ eVariationOn f (s ∩ Icc b a) = ∞ ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
rw₃ :
  eVariationOn f (s ∩ Icc b a) = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
⊢ variationOnFromTo f s a b = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
have rw₄ : (∀ x ∈ s ∩ Icc b a, ∀ y ∈ s ∩ Icc b a, edist (f x) (f y) = 0) ↔
  ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
Tactic: rw [variationOnFromTo.eq_of_ge _ _ ba, neg_eq_zero, ENNReal.toReal_eq_zero_iff,
    or_iff_left (hf b a hb ha), eVariationOn.eq_zero_iff]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ variationOnFromTo f s a b = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ uIcc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ uIcc a b), edist (f x) (f y) = 0
have inl : ∀ (ab : a ≤ b),
  variationOnFromTo f s a b = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ uIcc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ uIcc a b), edist (f x) (f y) = 0
Tactic: rcases le_total a b with (ab | ba)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
inl :
  ∀ (ab : a ≤ b),
    variationOnFromTo f s a b = 0 ↔
      ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ uIcc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ uIcc a b), edist (f x) (f y) = 0
⊢ variationOnFromTo f s a b = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ uIcc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ uIcc a b), edist (f x) (f y) = 0
have inr : ∀ (ba : b ≤ a),
  variationOnFromTo f s a b = 0 ↔
    ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ uIcc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ uIcc a b), edist (f x) (f y) = 0
Tactic: rcases le_total a b with (ab | ba)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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 : α⦄ (_hx : x ∈ s ∩ uIcc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ uIcc a b), edist (f x) (f y) = 0
have inl : variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc a b), edist (f x) (f y) = 0
Tactic: rw [uIcc_of_le ab]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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 : α⦄ (_hx : x ∈ s ∩ uIcc a b) ⦃y : α⦄ (_hy : y ∈ s ∩ uIcc a b), edist (f x) (f y) = 0
have inr : variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄ (_hx : x ∈ s ∩ Icc b a) ⦃y : α⦄ (_hy : y ∈ s ∩ Icc b a), edist (f x) (f y) = 0
Tactic: rw [uIcc_of_ge ba]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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 c
have rw : variationOnFromTo f s a b ≤ variationOnFromTo f s a b + variationOnFromTo f s b c
Tactic: rw [← variationOnFromTo.add hf as bs cs]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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 b
have rw : variationOnFromTo f s c b ≤ variationOnFromTo f s a c + variationOnFromTo f s c b
Tactic: rw [← variationOnFromTo.add hf as cs bs]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : 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
⊢ (variationOnFromTo f s a - f) b ≤ (variationOnFromTo f s a - f) c
have rw : f c - f b ≤ variationOnFromTo f s a c - variationOnFromTo f s a b
Tactic: rw [Pi.sub_apply, Pi.sub_apply, le_sub_iff_add_le, add_comm_sub, ← le_sub_iff_add_le']
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : 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| = dist (f b) (f c)
have rw : |f c - f b| = dist (f c) (f b)
Tactic: rw [dist_comm, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : 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
rw : |f c - f b| = dist (f c) (f b)
⊢ |f c - f b| = dist (f b) (f c)
have rw₁ : |f c - f b| = |f c - f b|
Tactic: rw [dist_comm, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : 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
⊢ dist (f b) (f c) ≤ variationOnFromTo f s b c
have rw : (edist (f b) (f c)).toReal ≤ (eVariationOn f (s ∩ Icc b c)).toReal
Tactic: rw [variationOnFromTo.eq_of_le f s bc, dist_edist]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : 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
⊢ (edist (f b) (f c)).toReal ≤ (eVariationOn f (s ∩ Icc b c)).toReal
have apply : edist (f b) (f c) ≤ eVariationOn f (s ∩ Icc b c)
Tactic: apply ENNReal.toReal_mono (hf b c bs cs)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : 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
⊢ edist (f b) (f c) ≤ eVariationOn f (s ∩ Icc b c)
have hx : b ∈ s ∩ Icc b c
Tactic: apply eVariationOn.edist_le f
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : 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
hx : b ∈ s ∩ Icc b c
⊢ edist (f b) (f c) ≤ eVariationOn f (s ∩ Icc b c)
have hy : c ∈ s ∩ Icc b c
Tactic: apply eVariationOn.edist_le f
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : 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
⊢ variationOnFromTo f s b c = variationOnFromTo f s a c - variationOnFromTo f s a b
have rw : variationOnFromTo f s b c = variationOnFromTo f s a b + variationOnFromTo f s b c - variationOnFromTo f s a b
Tactic: rw [← variationOnFromTo.add hf as bs cs, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : 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
rw : variationOnFromTo f s b c = variationOnFromTo f s a b + variationOnFromTo f s b c - variationOnFromTo f s a b
⊢ variationOnFromTo f s b c = variationOnFromTo f s a c - variationOnFromTo f s a b
have rw₁ : variationOnFromTo f s b c = variationOnFromTo f s b c
Tactic: rw [← variationOnFromTo.add hf as bs cs, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : 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
have f₁ : |f c - f b| = dist (f b) (f c)
Tactic: calc
    f c - f b ≤ |f c - f b| := le_abs_self _
    _ = dist (f b) (f c) := by rw [dist_comm, Real.dist_eq]
    _ ≤ variationOnFromTo f s b c := by
      rw [variationOnFromTo.eq_of_le f s bc, dist_edist]
      apply ENNReal.toReal_mono (hf b c bs cs)
      apply eVariationOn.edist_le f
      exacts [⟨bs, le_rfl, bc⟩, ⟨cs, bc, le_rfl⟩]
    _ = variationOnFromTo f s a c - variationOnFromTo f s a b := by
      rw [← variationOnFromTo.add hf as bs cs, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.BoundedVariation (goal)
Goal:
α : 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₁ : |f c - f b| = dist (f b) (f c)
⊢ f c - f b ≤ variationOnFromTo f s a c - variationOnFromTo f s a b
have f₂ : dist (f b) (f c) ≤ variationOnFromTo f s b c
Tactic: calc
    f c - f b ≤ |f c - f b| := le_abs_self _
    _ = dist (f b) (f c) := by rw [dist_comm, Real.dist_eq]
    _ ≤ variationOnFromTo f s b c := by
      rw [variationOnFromTo.eq_of_le f s bc, dist_edist]
      apply ENNReal.toReal_mono (hf b c bs cs)
      apply eVariationOn.edist_le f
      exacts [⟨bs, le_rfl, bc⟩, ⟨cs, bc, le_rfl⟩]
    _ = variationOnFromTo f s a c - variationOnFromTo f s a b := by
      rw [← variationOnFromTo.add hf as bs cs, add_sub_cancel_left]