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
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
⊢ IsGreatest (s ∩ Icc z x) x

Tactic:
⟨⟨hs.1, hs.2 zs, le_rfl⟩, fun w ⟨_, _, wx⟩ => wx⟩

Premises used: le_rfl, _private.0.HasConstantSpeedOnWith.union.match_1, LE.le, IsGreatest, And.right, And.left, 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 : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
⊢ IsLeast (t ∩ Icc x y) x

Tactic:
⟨⟨ht.1, le_rfl, ht.2 yt⟩, fun w ⟨_, xw, _⟩ => xw⟩

Premises used: le_rfl, _private.0.HasConstantSpeedOnWith.union.match_2, LE.le, IsLeast, And.right, And.left, 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 : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = s ∩ Icc z x ∪ t ∩ Icc x y
⊢ IsGreatest (s ∩ Icc z x) x

Tactic:
exacts [⟨⟨hs.1, hs.2 zs, le_rfl⟩, fun w ⟨_, _, wx⟩ => wx⟩,
      ⟨⟨ht.1, le_rfl, ht.2 yt⟩, fun w ⟨_, xw, _⟩ => xw⟩]
-- 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 : ℝ
zt : z ∈ t
y : ℝ
ys : y ∈ s
zy : z ≤ y
inr : ∀ (ys : z ∈ s) (zy : z ≤ z), eVariationOn f ((s ∪ t) ∩ Icc z z) = ENNReal.ofReal ((↑l : ℝ) * (z - z))
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))

Tactic:
cases le_antisymm zy ((hs.2 ys).trans (ht.2 zt))

Premises used: le_antisymm, And.right, 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 : ℝ
zt : z ∈ t
ys : z ∈ s
zy : z ≤ z
inr : eVariationOn f ((s ∪ t) ∩ {z}) = 0
⊢ eVariationOn f ((s ∪ t) ∩ Icc z z) = ENNReal.ofReal ((↑l : ℝ) * (z - z))

Tactic:
simp only [Icc_self, sub_self, mul_zero, ENNReal.ofReal_zero]

Premises used: Set.Icc_self, sub_self, MulZeroClass.mul_zero, ENNReal.ofReal_zero
-- 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 : ℝ
zt : z ∈ t
ys : z ∈ s
zy : z ≤ z
⊢ eVariationOn f ((s ∪ t) ∩ {z}) = 0

Tactic:
eVariationOn.subsingleton _ fun _ ⟨_, uz⟩ _ ⟨_, vz⟩ => uz.trans vz.symm

Premises used: eVariationOn.subsingleton, _private.0.HasConstantSpeedOnWith.union.match_3, Eq.symm, Eq, Eq.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 : ℝ
zt : z ∈ t
ys : z ∈ s
zy : z ≤ z
⊢ eVariationOn f ((s ∪ t) ∩ {z}) = 0

Tactic:
exact eVariationOn.subsingleton _ fun _ ⟨_, uz⟩ _ ⟨_, vz⟩ => uz.trans vz.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 : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
h : ∀ (w : ℝ), w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ t ∩ Icc z y
⊢ (s ∪ t) ∩ Icc z y = t ∩ 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 : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
h : w ∈ (s ∪ t) ∩ Icc z y → w ∈ t ∩ Icc z y
h₁ : w ∈ t ∩ Icc z y → w ∈ (s ∪ t) ∩ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ t ∩ 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 : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
ws : w ∈ s
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ t ∩ Icc z y

Tactic:
⟨le_antisymm ((ht.2 zt).trans zw) (hs.2 ws) ▸ ht.1, zw, wy⟩

Premises used: Set.Mem, setOf, Eq.rec, Set.inter, le_antisymm, And.right, And.left, And.intro, 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 : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
ws : w ∈ s
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ t ∩ Icc z y

Tactic:
exact ⟨le_antisymm ((ht.2 zt).trans zw) (hs.2 ws) ▸ ht.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 : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
wt : w ∈ t
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ t ∩ Icc z y

Tactic:
⟨wt, 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 : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
wt : w ∈ t
zw : z ≤ w
wy : w ≤ y
⊢ w ∈ t ∩ Icc z y

Tactic:
exact ⟨wt, 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 : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
wt : w ∈ t
zwy : w ∈ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y

Tactic:
⟨Or.inr wt, zwy⟩

Premises used: Set.Mem, setOf, Set.inter, 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 : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
w : ℝ
wt : w ∈ t
zwy : w ∈ Icc z y
⊢ w ∈ (s ∪ t) ∩ Icc z y

Tactic:
exact ⟨Or.inr wt, 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 : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
⊢ (s ∪ t) ∩ Icc z y = t ∩ Icc z y

Tactic:
have : (s ∪ t) ∩ Icc z y = t ∩ Icc z y := by
      ext w; constructor
      · rintro ⟨ws | wt, zw, wy⟩
        · exact ⟨le_antisymm ((ht.2 zt).trans zw) (hs.2 ws) ▸ ht.1, zw, wy⟩
        · exact ⟨wt, zw, wy⟩
      · rintro ⟨wt, zwy⟩; exact ⟨Or.inr wt, 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 : ℝ
zt : z ∈ t
y : ℝ
yt : y ∈ t
zy : z ≤ y
this : (s ∪ t) ∩ Icc z y = t ∩ Icc z y
inr : eVariationOn f (t ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
inr₁ inr₂ : 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, hft zt yt zy]
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
inl : ∀ (xy : x ≤ y), HasConstantSpeedOnWith f (Icc x z) l
inr : ∀ (yx : y ≤ x), HasConstantSpeedOnWith f (Icc x z) l
⊢ HasConstantSpeedOnWith f (Icc x z) l

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
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
inl : ∀ (yz : y ≤ z), HasConstantSpeedOnWith f (Icc x z) l
inl₁ : ∀ (zy : z ≤ y), HasConstantSpeedOnWith f (Icc x z) l
⊢ HasConstantSpeedOnWith f (Icc x z) l

Tactic:
rcases le_total y z with (yz | zy)

Premises used: le_total
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
yz : y ≤ z
inl : HasConstantSpeedOnWith f (Icc x y ∪ Icc y z) l
⊢ HasConstantSpeedOnWith f (Icc x z) l

Tactic:
rw [← Set.Icc_union_Icc_eq_Icc xy yz]

Premises used: Set.Icc_union_Icc_eq_Icc
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
yz : y ≤ z
⊢ HasConstantSpeedOnWith f (Icc x y ∪ Icc y z) l

Tactic:
hfs.union hft (isGreatest_Icc xy) (isLeast_Icc yz)

Premises used: isLeast_Icc, HasConstantSpeedOnWith.union, isGreatest_Icc
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
yz : y ≤ z
⊢ HasConstantSpeedOnWith f (Icc x y ∪ Icc y z) l

Tactic:
exact hfs.union hft (isGreatest_Icc xy) (isLeast_Icc yz)

Premises used: isLeast_Icc, HasConstantSpeedOnWith.union, isGreatest_Icc
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
xy : x ≤ y
zy : z ≤ y
u : ℝ
xu : x ≤ u
uz : u ≤ z
v : ℝ
xv : x ≤ v
vz : v ≤ z
inl : eVariationOn f (Icc (max x u) (min z v)) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
inl₁ : eVariationOn f (Icc u (min z v)) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
inl₂ : eVariationOn f (Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
inl₃ : eVariationOn f (Icc u v) = eVariationOn f (Icc x y ∩ Icc u v)
inl₄ : eVariationOn f (Icc u v) = eVariationOn f (Icc (max x u) (min y v))
inl₅ : eVariationOn f (Icc u v) = eVariationOn f (Icc u (min y v))
inl₆ inl₇ : eVariationOn f (Icc u v) = eVariationOn f (Icc u v)
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))

Tactic:
rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ←
        hfs ⟨xu, uz.trans zy⟩ ⟨xv, vz.trans zy⟩, Icc_inter_Icc, sup_of_le_right xu,
        inf_of_le_right (vz.trans zy)]

Premises used: inf_of_le_right, Set.Icc_inter_Icc, sup_of_le_right, And.intro, LE.le.trans
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
l : ℝ≥0
x y z : ℝ
hfs : HasConstantSpeedOnWith f (Icc x y) l
hft : HasConstantSpeedOnWith f (Icc y z) l
yx : y ≤ x
u : ℝ
xu : x ≤ u
uz : u ≤ z
v : ℝ
xv : x ≤ v
vz : v ≤ z
inr : eVariationOn f (Icc (max x u) (min z v)) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
inr₁ : eVariationOn f (Icc u (min z v)) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
inr₂ : eVariationOn f (Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
inr₃ : eVariationOn f (Icc u v) = eVariationOn f (Icc y z ∩ Icc u v)
inr₄ : eVariationOn f (Icc u v) = eVariationOn f (Icc (max y u) (min z v))
inr₅ : eVariationOn f (Icc u v) = eVariationOn f (Icc u (min z v))
inr₆ inr₇ : eVariationOn f (Icc u v) = eVariationOn f (Icc u v)
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))

Tactic:
rw [Icc_inter_Icc, sup_of_le_right xu, inf_of_le_right vz, ←
      hft ⟨yx.trans xu, uz⟩ ⟨yx.trans xv, vz⟩, Icc_inter_Icc, sup_of_le_right (yx.trans xu),
      inf_of_le_right vz]

Premises used: inf_of_le_right, Set.Icc_inter_Icc, sup_of_le_right, And.intro, LE.le.trans
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
simp : (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) ↔ eVariationOn f s = 0
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (0 * (y - x))) ↔
    ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

Tactic:
simp only [zero_mul, ENNReal.ofReal_zero, ← eVariationOn.eq_zero_iff]

Premises used: MulZeroClass.zero_mul, ENNReal.ofReal_zero, eVariationOn.eq_zero_iff
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
mp : (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) → eVariationOn f s = 0
mpr : eVariationOn f s = 0 → ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) ↔ eVariationOn f s = 0

Tactic:
constructor
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
mp : ∀ (h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) (hfs : eVariationOn f s ≠ 0), False
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) → eVariationOn f s = 0

Tactic:
by_contra! ⟨h, hfs⟩
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0
hfs : eVariationOn f s ≠ 0
⊢ ¬∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

Tactic:
simp_rw [ne_eq, eVariationOn.eq_zero_iff] at hfs h

Premises used: ne_eq, eVariationOn.eq_zero_iff
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0
hfs : eVariationOn f s ≠ 0
hfs₁ : ¬∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
⊢ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0

Tactic:
simp_rw [ne_eq, eVariationOn.eq_zero_iff] at hfs h

Premises used: ne_eq, eVariationOn.eq_zero_iff
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hfs : ¬∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
⊢ ∃ x ∈ s, ∃ y ∈ s, edist (f x) (f y) ≠ 0

Tactic:
push Not at hfs

Premises used: Not
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
hfs : ∃ x ∈ s, ∃ y ∈ s, edist (f x) (f y) ≠ 0
mp : ∀ (x : ℝ) (xs : x ∈ s) (y : ℝ) (ys : y ∈ s) (hxy : edist (f x) (f y) ≠ 0), False
⊢ False

Tactic:
obtain ⟨x, xs, y, ys, hxy⟩ := hfs
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
hxy : edist (f x) (f y) ≠ 0
mp : ∀ (xy : x ≤ y), False
mp₁ : ∀ (yx : y ≤ x), False
⊢ False

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 ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
hxy : edist (f x) (f y) ≠ 0
xy : x ≤ y
⊢ False

Tactic:
hxy (h xs ys x ⟨xs, le_rfl, xy⟩ y ⟨ys, xy, le_rfl⟩)

Premises used: le_rfl, And.intro
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
hxy : edist (f x) (f y) ≠ 0
xy : x ≤ y
⊢ False

Tactic:
exact hxy (h xs ys x ⟨xs, le_rfl, xy⟩ y ⟨ys, xy, le_rfl⟩)

Premises used: le_rfl, And.intro
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
hxy : edist (f x) (f y) ≠ 0
yx : y ≤ x
⊢ edist (f y) (f x) ≠ 0

Tactic:
rw [edist_comm] at hxy

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
hxy : edist (f x) (f y) ≠ 0
yx : y ≤ x
hxy₁ : edist (f y) (f x) ≠ 0
⊢ y ≤ x

Tactic:
rw [edist_comm] at hxy

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
hxy : edist (f y) (f x) ≠ 0
yx : y ≤ x
⊢ False

Tactic:
hxy (h ys xs y ⟨ys, le_rfl, yx⟩ x ⟨xs, yx, le_rfl⟩)

Premises used: le_rfl, And.intro
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → ∀ x_3 ∈ s ∩ Icc x y, ∀ y_1 ∈ s ∩ Icc x y, edist (f x_3) (f y_1) = 0
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
hxy : edist (f y) (f x) ≠ 0
yx : y ≤ x
⊢ False

Tactic:
exact hxy (h ys xs y ⟨ys, le_rfl, yx⟩ x ⟨xs, yx, le_rfl⟩)

Premises used: le_rfl, And.intro
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
h : eVariationOn f s = 0
x : ℝ
h_1 : x ∈ s
y : ℝ
h_2 : y ∈ s
⊢ eVariationOn f (s ∩ Icc x y) = 0

Tactic:
simpa [h] using eVariationOn.mono (s := s) f inter_subset_left

Premises used: Set.inter_subset_left, eVariationOn.mono
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l l' : ℝ≥0
hl' : l' ≠ 0
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s l
hf : HasConstantSpeedOnWith f (φ '' s) l'
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
rw : (φ y - φ x) * (↑l' : ℝ) = (y - x) * (↑l : ℝ)
⊢ φ y = (fun (y : ℝ) ↦ (↑l : ℝ) / (↑l' : ℝ) * (y - x) + φ x) y

Tactic:
rw [← sub_eq_iff_eq_add, mul_comm, ← mul_div_assoc, eq_div_iff (NNReal.coe_ne_zero.mpr hl')]

Premises used: Iff.mpr, mul_div_assoc, sub_eq_iff_eq_add, mul_comm, NNReal.coe_ne_zero, eq_div_iff
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l l' : ℝ≥0
hl' : l' ≠ 0
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s l
hf : HasConstantSpeedOnWith f (φ '' s) l'
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
rw :
  ∀
    (hf :
      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), (φ y - φ x) * (↑l' : ℝ) = (y - x) * (↑l : ℝ)
⊢ (φ y - φ x) * (↑l' : ℝ) = (y - x) * (↑l : ℝ)

Tactic:
rw [hasConstantSpeedOnWith_iff_variationOnFromTo_eq] at hf

Premises used: hasConstantSpeedOnWith_iff_variationOnFromTo_eq
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l l' : ℝ≥0
hl' : l' ≠ 0
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s l
hf :
  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
rw :
  ∀
    (hfφ :
      LocallyBoundedVariationOn (f ∘ φ) s ∧
        ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo (f ∘ φ) s x y = (↑l : ℝ) * (y - x))
    (hf :
      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), (φ y - φ x) * (↑l' : ℝ) = (y - x) * (↑l : ℝ)
⊢ (φ y - φ x) * (↑l' : ℝ) = (y - x) * (↑l : ℝ)

Tactic:
rw [hasConstantSpeedOnWith_iff_variationOnFromTo_eq] at hfφ

Premises used: hasConstantSpeedOnWith_iff_variationOnFromTo_eq
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l l' : ℝ≥0
hl' : l' ≠ 0
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ :
  LocallyBoundedVariationOn (f ∘ φ) s ∧
    ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo (f ∘ φ) s x y = (↑l : ℝ) * (y - x)
hf :
  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
symm : (y - x) * (↑l : ℝ) = (φ y - φ x) * (↑l' : ℝ)
⊢ (φ y - φ x) * (↑l' : ℝ) = (y - x) * (↑l : ℝ)

Tactic:
symm