awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
zs : x ∈ s
xz : x ≤ x
zy : x ≤ y
ws : x ∈ s
xw : x ≤ x
wy : x ≤ y
⊢ x = x

Tactic:
rfl
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
mp :
  HasConstantSpeedOnWith f s l →
    LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
mpr :
  (LocallyBoundedVariationOn f s ∧
      ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)) →
    HasConstantSpeedOnWith f s l
⊢ HasConstantSpeedOnWith f s l ↔
    LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)

Tactic:
constructor
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
⊢ LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)

Tactic:
⟨h.hasLocallyBoundedVariationOn, fun x xs y ys => ?_⟩

Premises used: HasConstantSpeedOnWith.hasLocallyBoundedVariationOn, And.intro
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
mp : ∀ (x : ℝ) (xs : x ∈ s) (y : ℝ) (ys : y ∈ s), variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
⊢ LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)

Tactic:
refine ⟨h.hasLocallyBoundedVariationOn, fun x xs y ys => ?_⟩
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
mp :
  ∀
    (h :
      ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x)))
    (x : ℝ) (xs : x ∈ s) (y : ℝ) (ys : y ∈ s), variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
⊢ variationOnFromTo f s x y = (↑l : ℝ) * (y - x)

Tactic:
rw [hasConstantSpeedOnWith_iff_ordered] at h

Premises used: hasConstantSpeedOnWith_iff_ordered
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
mp : ∀ (xy : x ≤ y), variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
mp₁ : ∀ (yx : y ≤ x), variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
⊢ variationOnFromTo f s x y = (↑l : ℝ) * (y - x)

Tactic:
rcases le_total x y with (xy | yx)

Premises used: le_total
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
mp : (ENNReal.ofReal ((↑l : ℝ) * (y - x))).toReal = (↑l : ℝ) * (y - x)
⊢ variationOnFromTo f s x y = (↑l : ℝ) * (y - x)

Tactic:
rw [variationOnFromTo.eq_of_le f s xy, h xs ys xy]

Premises used: variationOnFromTo.eq_of_le
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ (ENNReal.ofReal ((↑l : ℝ) * (y - x))).toReal = (↑l : ℝ) * (y - x)

Tactic:
ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr xy))

Premises used: Iff.mpr, mul_nonneg, ENNReal.toReal_ofReal, Subtype.prop, sub_nonneg
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
⊢ (ENNReal.ofReal ((↑l : ℝ) * (y - x))).toReal = (↑l : ℝ) * (y - x)

Tactic:
exact ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr xy))

Premises used: Iff.mpr, mul_nonneg, ENNReal.toReal_ofReal, Subtype.prop, sub_nonneg
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
mp : -(ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (y - x)
⊢ variationOnFromTo f s x y = (↑l : ℝ) * (y - x)

Tactic:
rw [variationOnFromTo.eq_of_ge f s yx, h ys xs yx]

Premises used: variationOnFromTo.eq_of_ge
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
⊢ (ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (x - y)

Tactic:
have := ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr yx))
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
this : (ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (x - y)
mp :
  ∀ (this : (ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (x - y)),
    -((↑l : ℝ) * (x - y)) = (↑l : ℝ) * (y - x)
⊢ -(ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (y - x)

Tactic:
simp_all only [NNReal.val_eq_coe]

Premises used: NNReal.val_eq_coe
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
this : (ENNReal.ofReal ((↑l : ℝ) * (x - y))).toReal = (↑l : ℝ) * (x - y)
⊢ -((↑l : ℝ) * (x - y)) = (↑l : ℝ) * (y - x)

Tactic:
ring
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
mpr :
  (LocallyBoundedVariationOn f s ∧
      ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)) →
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
⊢ (LocallyBoundedVariationOn f s ∧
      ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)) →
    HasConstantSpeedOnWith f s l

Tactic:
rw [hasConstantSpeedOnWith_iff_ordered]

Premises used: hasConstantSpeedOnWith_iff_ordered
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = (↑l : ℝ) * (y - x)
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
xy : x ≤ y
mpr : eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (variationOnFromTo f s x y)
mpr₁ : eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (eVariationOn f (s ∩ Icc x y)).toReal
mpr₂ mpr₃ : eVariationOn f (s ∩ Icc x y) = eVariationOn f (s ∩ Icc x y)
⊢ eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))

Tactic:
rw [← h.2 xs ys, variationOnFromTo.eq_of_le f s xy, ENNReal.ofReal_toReal (h.1 x y xs ys)]

Premises used: ENNReal.ofReal_toReal, And.right, And.left, variationOnFromTo.eq_of_le
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : HasConstantSpeedOnWith f s l
hft : HasConstantSpeedOnWith f t l
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
rw :
  ∀
    (hfs :
      ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x)))
    (hft :
      ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x)))
    {x : ℝ} (hs : IsGreatest s x) (ht : IsLeast t x) ⦃x : ℝ⦄,
    x ∈ s ∪ t → ∀ ⦃y : ℝ⦄, y ∈ s ∪ t → x ≤ y → eVariationOn f ((s ∪ t) ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
⊢ HasConstantSpeedOnWith f (s ∪ t) l

Tactic:
rw [hasConstantSpeedOnWith_iff_ordered] at hfs hft ⊢

Premises used: hasConstantSpeedOnWith_iff_ordered
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
h : ∀ (w : ℝ), w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z y
⊢ (s ∪ t) ∩ Icc z y = s ∩ Icc z y

Tactic:
ext w
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
h : w ∈ (s ∪ t) ∩ Icc z y → w ∈ s ∩ Icc z y
h₁ : w ∈ s ∩ Icc z y → w ∈ (s ∪ t) ∩ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z y

Tactic:
constructor
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
ws : w ∈ s
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z y

Tactic:
⟨ws, zw, wy⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
ws : w ∈ s
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z y

Tactic:
exact ⟨ws, zw, wy⟩
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
wt : w ∈ t
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z y

Tactic:
⟨(le_antisymm (wy.trans (hs.2 ys)) (ht.2 wt)).symm ▸ hs.1, zw, wy⟩

Premises used: Set.Mem, setOf, Eq.rec, Set.inter, le_antisymm, And.right, And.left, And.intro, LE.le.trans, Eq.symm
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
wt : w ∈ t
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z y

Tactic:
exact ⟨(le_antisymm (wy.trans (hs.2 ys)) (ht.2 wt)).symm ▸ hs.1, zw, wy⟩
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
ws : w ∈ s
zwy : w ∈ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y

Tactic:
⟨Or.inl ws, zwy⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro, Or.inl
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
w : ℝ
ws : w ∈ s
zwy : w ∈ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y

Tactic:
exact ⟨Or.inl ws, zwy⟩
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
⊢ (s ∪ t) ∩ Icc z y = s ∩ Icc z y

Tactic:
have : (s ∪ t) ∩ Icc z y = s ∩ Icc z y := by
      ext w; constructor
      · rintro ⟨ws | wt, zw, wy⟩
        · exact ⟨ws, zw, wy⟩
        · exact ⟨(le_antisymm (wy.trans (hs.2 ys)) (ht.2 wt)).symm ▸ hs.1, zw, wy⟩
      · rintro ⟨ws, zwy⟩; exact ⟨Or.inl ws, zwy⟩
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
ys : y ∈ s
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z y
inl : eVariationOn f (s ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
inl₁ inl₂ : ENNReal.ofReal ((↑l : ℝ) * (y - z)) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))

Tactic:
rw [this, hfs zs ys zy]
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
h : ∀ (w : ℝ), w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y
⊢ (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y

Tactic:
ext w
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
h : w ∈ (s ∪ t) ∩ Icc z y → w ∈ s ∩ Icc z x ∪ t ∩ Icc x y
h₁ : w ∈ s ∩ Icc z x ∪ t ∩ Icc x y → w ∈ (s ∪ t) ∩ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y

Tactic:
constructor
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
ws : w ∈ s
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y

Tactic:
Or.inl ⟨ws, zw, hs.2 ws⟩

Premises used: Set.union, Set.Mem, setOf, And.right, And.intro, Or.inl
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
wt : w ∈ t
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y

Tactic:
Or.inr ⟨wt, ht.2 wt, wy⟩

Premises used: Set.union, Set.Mem, setOf, And.right, And.intro, Or.inr
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
ws : w ∈ s
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y

Tactic:
exacts [Or.inl ⟨ws, zw, hs.2 ws⟩, Or.inr ⟨wt, ht.2 wt, wy⟩]

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
ws : w ∈ s
zw : z ≤ w
wx : w ≤ x
⊢ w ∈ (s ∪ t) ∩ Icc z y

Tactic:
⟨Or.inl ws, zw, wx.trans (ht.2 yt)⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.intro, Or.inl, LE.le.trans
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
wt : w ∈ t
xw : x ≤ w
wy : w ≤ y
⊢ w ∈ (s ∪ t) ∩ Icc z y

Tactic:
⟨Or.inr wt, (hs.2 zs).trans xw, wy⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.intro, LE.le.trans, Or.inr
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
ws : w ∈ s
zw : z ≤ w
wx : w ≤ x
⊢ w ∈ (s ∪ t) ∩ Icc z y

Tactic:
exacts [⟨Or.inl ws, zw, wx.trans (ht.2 yt)⟩, ⟨Or.inr wt, (hs.2 zs).trans xw, wy⟩]
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
⊢ (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y

Tactic:
have : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y := by
      ext w; constructor
      · rintro ⟨ws | wt, zw, wy⟩
        exacts [Or.inl ⟨ws, zw, hs.2 ws⟩, Or.inr ⟨wt, ht.2 wt, wy⟩]
      · rintro (⟨ws, zw, wx⟩ | ⟨wt, xw, wy⟩)
        exacts [⟨Or.inl ws, zw, wx.trans (ht.2 yt)⟩, ⟨Or.inr wt, (hs.2 zs).trans xw, wy⟩]
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
inl : ENNReal.ofReal ((↑l : ℝ) * (x - z)) + ENNReal.ofReal ((↑l : ℝ) * (y - x)) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
inl₁ : IsGreatest (s ∩ Icc z x) x
inl₂ : IsLeast (t ∩ Icc x y) x
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))

Tactic:
rw [this, @eVariationOn.union _ _ _ _ f _ _ x, hfs zs hs.1 (hs.2 zs), hft ht.1 yt (ht.2 yt)]

Premises used: eVariationOn.union, And.right, And.left
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
⊢ ENNReal.ofReal ((↑l : ℝ) * (x - z) + (↑l : ℝ) * (y - x)) =
    ENNReal.ofReal ((↑l : ℝ) * (x - z)) + ENNReal.ofReal ((↑l : ℝ) * (y - x))

Tactic:
have q := ENNReal.ofReal_add (mul_nonneg l.prop (sub_nonneg.mpr (hs.2 zs)))
        (mul_nonneg l.prop (sub_nonneg.mpr (ht.2 yt)))
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
q :
  ENNReal.ofReal ((↑l : ℝ) * (x - z) + (↑l : ℝ) * (y - x)) =
    ENNReal.ofReal ((↑l : ℝ) * (x - z)) + ENNReal.ofReal ((↑l : ℝ) * (y - x))
inl : ENNReal.ofReal ((↑l : ℝ) * (x - z) + (↑l : ℝ) * (y - x)) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
⊢ ENNReal.ofReal ((↑l : ℝ) * (x - z)) + ENNReal.ofReal ((↑l : ℝ) * (y - x)) = ENNReal.ofReal ((↑l : ℝ) * (y - z))

Tactic:
rw [← q]
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
t : Set ℝ
hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal ((↑l : ℝ) * (y - x))
x : ℝ
hs : IsGreatest s x
ht : IsLeast t x
z : ℝ
zs : z ∈ s
y : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
q :
  ENNReal.ofReal ((↑l : ℝ) * (x - z) + (↑l : ℝ) * (y - x)) =
    ENNReal.ofReal ((↑l : ℝ) * (x - z)) + ENNReal.ofReal ((↑l : ℝ) * (y - x))
⊢ ENNReal.ofReal ((↑l : ℝ) * (x - z) + (↑l : ℝ) * (y - x)) = ENNReal.ofReal ((↑l : ℝ) * (y - z))

Tactic:
ring_nf