awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : a ≤ b
⊢ (eVariationOn f (s ∩ Icc a b)).toReal ≤ (eVariationOn f s).toReal

Tactic:
exact ENNReal.toReal_mono hf (eVariationOn.mono _ inter_subset_left)

Premises used: Set.inter_subset_left, eVariationOn.mono, ENNReal.toReal_mono
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : ¬a ≤ b
neg : (eVariationOn f (s ∩ Icc b a)).toReal ≤ (eVariationOn f s).toReal
⊢ |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal

Tactic:
simp only [variationOnFromTo, hab, ↓reduceIte, abs_neg, ENNReal.abs_toReal]

Premises used: abs_neg, variationOnFromTo, reduceIte, ENNReal.abs_toReal
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : ¬a ≤ b
⊢ (eVariationOn f (s ∩ Icc b a)).toReal ≤ (eVariationOn f s).toReal

Tactic:
ENNReal.toReal_mono hf (eVariationOn.mono _ inter_subset_left)

Premises used: Set.inter_subset_left, eVariationOn.mono, ENNReal.toReal_mono
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : BoundedVariationOn f s
a b : α
hab : ¬a ≤ b
⊢ (eVariationOn f (s ∩ Icc b a)).toReal ≤ (eVariationOn f s).toReal

Tactic:
exact ENNReal.toReal_mono hf (eVariationOn.mono _ inter_subset_left)

Premises used: Set.inter_subset_left, eVariationOn.mono, ENNReal.toReal_mono
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : a ≤ b
⊢ variationOnFromTo f s a b = (eVariationOn f (s ∩ Icc a b)).toReal

Tactic:
if_pos h

Premises used: if_pos, variationOnFromTo
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
a b : α
h : b ≤ a
rw : -variationOnFromTo f s b a = -(eVariationOn f (s ∩ Icc b a)).toReal
rw₁ : variationOnFromTo f s b a = (eVariationOn f (s ∩ Icc b a)).toReal
rw₂ rw₃ : (eVariationOn f (s ∩ Icc b a)).toReal = (eVariationOn f (s ∩ Icc b a)).toReal
⊢ variationOnFromTo f s a b = -(eVariationOn f (s ∩ Icc b a)).toReal

Tactic:
rw [variationOnFromTo.eq_neg_swap, neg_inj, variationOnFromTo.eq_of_le f s h]

Premises used: neg_inj, variationOnFromTo.eq_of_le, variationOnFromTo.eq_neg_swap
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
symm : variationOnFromTo f s a 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

Tactic:
symm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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 a b + variationOnFromTo f s b c

Tactic:
additive_of_total (· ≤ · : α → α → Prop) (variationOnFromTo f s) (· ∈ s) ?_ ?_ ha hb hc

Premises used: additive_of_total, Membership.mem, LE.le, variationOnFromTo
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
refine_1 :
  ∀ {a b : α},
    (fun (x : α) ↦ x ∈ s) a → (fun (x : α) ↦ x ∈ s) b → variationOnFromTo f s a b + variationOnFromTo f s b a = 0
refine_2 :
  ∀ {a b c : α},
    (fun (x1 x2 : α) ↦ x1 ≤ x2) a b →
      (fun (x1 x2 : α) ↦ x1 ≤ x2) b c →
        (fun (x : α) ↦ x ∈ s) a →
          (fun (x : α) ↦ x ∈ s) b →
            (fun (x : α) ↦ x ∈ s) c → variationOnFromTo f s a c = variationOnFromTo f s a b + variationOnFromTo f s b c
⊢ variationOnFromTo f s a c = variationOnFromTo f s a b + variationOnFromTo f s b c

Tactic:
refine additive_of_total (· ≤ · : α → α → Prop) (variationOnFromTo f s) (· ∈ s) ?_ ?_ ha hb hc

Premises used: additive_of_total, Membership.mem, LE.le, variationOnFromTo
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
x y : α
_xs : x ∈ s
_ys : y ∈ s
⊢ variationOnFromTo f s x y + variationOnFromTo f s y x = 0

Tactic:
simp only [variationOnFromTo.eq_neg_swap f s y x, add_neg_cancel]

Premises used: add_neg_cancel, variationOnFromTo.eq_neg_swap
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
x y z : α
xy : x ≤ y
yz : y ≤ z
xs : x ∈ s
ys : y ∈ s
zs : z ∈ s
refine_2 : variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + variationOnFromTo f s y z
refine_2₁ : variationOnFromTo f s x z = (eVariationOn f (s ∩ Icc x y)).toReal + (eVariationOn f (s ∩ Icc y z)).toReal
refine_2₂ :
  (eVariationOn f (s ∩ Icc x z)).toReal = (eVariationOn f (s ∩ Icc x y)).toReal + (eVariationOn f (s ∩ Icc y z)).toReal
refine_2₃ : (eVariationOn f (s ∩ Icc x z)).toReal = (eVariationOn f (s ∩ Icc x y) + eVariationOn f (s ∩ Icc y z)).toReal
refine_2₄ refine_2₅ : (eVariationOn f (s ∩ Icc x z)).toReal = (eVariationOn f (s ∩ Icc x z)).toReal
⊢ variationOnFromTo f s x z = variationOnFromTo f s x y + variationOnFromTo f s y z

Tactic:
rw [variationOnFromTo.eq_of_le f s xy, variationOnFromTo.eq_of_le f s yz,
      variationOnFromTo.eq_of_le f s (xy.trans yz),
      ← ENNReal.toReal_add (hf x y xs ys) (hf y z ys zs), eVariationOn.Icc_add_Icc f xy yz ys]

Premises used: ENNReal.toReal_add, variationOnFromTo.eq_of_le, LE.le.trans, eVariationOn.Icc_add_Icc
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
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
⊢ edist (f a) (f b) = 0

Tactic:
wlog h' : a ≤ b
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
inr : edist (f b) (f a) = 0
⊢ edist (f a) (f b) = 0

Tactic:
rw [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
apply : variationOnFromTo f s b a = 0
⊢ edist (f b) (f a) = 0

Tactic:
apply this hf hb ha _ (le_of_not_ge h')

Premises used: le_of_not_ge
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ variationOnFromTo f s b a = 0

Tactic:
rw [variationOnFromTo.eq_neg_swap, h, neg_zero]

Premises used: variationOnFromTo.eq_neg_swap, neg_zero
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
rw : edist (f a) (f b) ≤ eVariationOn f (s ∩ Icc a b)
⊢ edist (f a) (f b) = 0

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)]

Premises used: ENNReal.ofReal_toReal, variationOnFromTo.eq_of_le, ENNReal.ofReal_zero, nonpos_iff_eq_zero
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
hy : b ∈ s ∩ Icc a b
⊢ edist (f a) (f b) ≤ eVariationOn f (s ∩ Icc a b)

Tactic:
apply eVariationOn.edist_le

Premises used: eVariationOn.edist_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ a ∈ s ∩ Icc a b

Tactic:
⟨ha, ⟨le_rfl, h'⟩⟩

Premises used: le_rfl, Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ b ∈ s ∩ Icc a b

Tactic:
⟨hb, ⟨h', le_rfl⟩⟩

Premises used: le_rfl, Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
⊢ a ∈ s ∩ Icc a b

Tactic:
exacts [⟨ha, ⟨le_rfl, h'⟩⟩, ⟨hb, ⟨h', le_rfl⟩⟩]
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : 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 b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0

Tactic:
simp only [← variationOnFromTo.add hf ha hb hc, left_eq_add]

Premises used: left_eq_add, variationOnFromTo.add
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
rw₃ 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
⊢ 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 [variationOnFromTo.eq_of_le _ _ ab, ENNReal.toReal_eq_zero_iff, or_iff_left (hf a b ha hb),
    eVariationOn.eq_zero_iff]

Premises used: variationOnFromTo.eq_of_le, or_iff_left, ENNReal.toReal_eq_zero_iff, eVariationOn.eq_zero_iff
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
rw₄ 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
⊢ 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 [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]

Premises used: variationOnFromTo.eq_of_ge, neg_eq_zero, or_iff_left, ENNReal.toReal_eq_zero_iff, eVariationOn.eq_zero_iff
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
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
⊢ 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)

Premises used: le_total
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
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
⊢ 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:
rw [uIcc_of_le ab]

Premises used: Set.uIcc_of_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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

Tactic:
variationOnFromTo.eq_zero_iff_of_le hf ha hb ab

Premises used: variationOnFromTo.eq_zero_iff_of_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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

Tactic:
exact variationOnFromTo.eq_zero_iff_of_le hf ha hb ab

Premises used: variationOnFromTo.eq_zero_iff_of_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
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
⊢ 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:
rw [uIcc_of_ge ba]

Premises used: Set.uIcc_of_ge
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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

Tactic:
variationOnFromTo.eq_zero_iff_of_ge hf ha hb ba

Premises used: variationOnFromTo.eq_zero_iff_of_ge
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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

Tactic:
exact variationOnFromTo.eq_zero_iff_of_ge hf ha hb ba

Premises used: variationOnFromTo.eq_zero_iff_of_ge
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
rw : variationOnFromTo f s a b ≤ variationOnFromTo f s a b + variationOnFromTo f s b c
⊢ variationOnFromTo f s a b ≤ variationOnFromTo f s a c

Tactic:
rw [← variationOnFromTo.add hf as bs cs]

Premises used: variationOnFromTo.add
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 b + variationOnFromTo f s b c

Tactic:
le_add_of_nonneg_right (variationOnFromTo.nonneg_of_le f s bc)

Premises used: le_add_of_nonneg_right, variationOnFromTo.nonneg_of_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 b + variationOnFromTo f s b c

Tactic:
exact le_add_of_nonneg_right (variationOnFromTo.nonneg_of_le f s bc)

Premises used: le_add_of_nonneg_right, variationOnFromTo.nonneg_of_le
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
rw : variationOnFromTo f s c b ≤ variationOnFromTo f s a c + variationOnFromTo f s c b
⊢ variationOnFromTo f s c b ≤ variationOnFromTo f s a b

Tactic:
rw [← variationOnFromTo.add hf as cs bs]

Premises used: variationOnFromTo.add
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 c + variationOnFromTo f s c b

Tactic:
le_add_of_nonneg_left (variationOnFromTo.nonneg_of_le f s ac)

Premises used: variationOnFromTo.nonneg_of_le, le_add_of_nonneg_left
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 c + variationOnFromTo f s c b

Tactic:
exact le_add_of_nonneg_left (variationOnFromTo.nonneg_of_le f s ac)

Premises used: variationOnFromTo.nonneg_of_le, le_add_of_nonneg_left
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 ≤ variationOnFromTo f s a c - variationOnFromTo f s a b
⊢ (variationOnFromTo f s a - f) b ≤ (variationOnFromTo f s a - f) c

Tactic:
rw [Pi.sub_apply, Pi.sub_apply, le_sub_iff_add_le, add_comm_sub, ← le_sub_iff_add_le']

Premises used: le_sub_iff_add_le', add_comm_sub, le_sub_iff_add_le, Pi.sub_apply
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 ≤ |f c - f b|

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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)
rw₁ rw₂ : |f c - f b| = |f c - f b|
⊢ |f c - f b| = dist (f b) (f c)

Tactic:
rw [dist_comm, Real.dist_eq]

Premises used: dist_comm, Real.dist_eq
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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 : (edist (f b) (f c)).toReal ≤ (eVariationOn f (s ∩ Icc b c)).toReal
⊢ dist (f b) (f c) ≤ variationOnFromTo f s b c

Tactic:
rw [variationOnFromTo.eq_of_le f s bc, dist_edist]

Premises used: variationOnFromTo.eq_of_le, dist_edist
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
apply : edist (f b) (f c) ≤ eVariationOn f (s ∩ Icc b c)
⊢ (edist (f b) (f c)).toReal ≤ (eVariationOn f (s ∩ Icc b c)).toReal

Tactic:
apply ENNReal.toReal_mono (hf b c bs cs)

Premises used: ENNReal.toReal_mono
-- Module: Mathlib.Topology.EMetricSpace.BoundedVariation
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
hy : c ∈ s ∩ Icc b c
⊢ edist (f b) (f c) ≤ eVariationOn f (s ∩ Icc b c)

Tactic:
apply eVariationOn.edist_le f

Premises used: eVariationOn.edist_le