awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ s ∩ Icc z x ∪ t ∩ Icc x y
have h₁ : w ∈ s ∩ Icc z x ∪ t ∩ Icc x y → w ∈ (s ∪ t) ∩ Icc z y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
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
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have this : (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⟩]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have inl : ENNReal.ofReal ((↑l : ℝ) * (x - z)) + ENNReal.ofReal ((↑l : ℝ) * (y - x)) = 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)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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))
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have inl₁ : IsGreatest (s ∩ Icc z x) x
Tactic: rw [this, @eVariationOn.union _ _ _ _ f _ _ x, hfs zs hs.1 (hs.2 zs), hft ht.1 yt (ht.2 yt)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have inl₂ : IsLeast (t ∩ Icc x y) x
Tactic: rw [this, @eVariationOn.union _ _ _ _ f _ _ x, hfs zs hs.1 (hs.2 zs), hft ht.1 yt (ht.2 yt)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
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)) + ENNReal.ofReal ((↑l : ℝ) * (y - x)) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have q : 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)))
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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)) + ENNReal.ofReal ((↑l : ℝ) * (y - x)) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have inl : ENNReal.ofReal ((↑l : ℝ) * (x - z) + (↑l : ℝ) * (y - x)) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
Tactic: rw [← q]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have inr : ∀ (ys : z ∈ s) (zy : z ≤ z), eVariationOn f ((s ∪ t) ∩ Icc z z) = ENNReal.ofReal ((↑l : ℝ) * (z - z))
Tactic: cases le_antisymm zy ((hs.2 ys).trans (ht.2 zt))
Cleared hypotheses: y, ys, zy
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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) ∩ Icc z z) = ENNReal.ofReal ((↑l : ℝ) * (z - z))
have inr : eVariationOn f ((s ∪ t) ∩ {z}) = 0
Tactic: simp only [Icc_self, sub_self, mul_zero, ENNReal.ofReal_zero]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
have h : ∀ (w : ℝ), w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ t ∩ Icc z y
Tactic: ext w
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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 : ℝ
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ t ∩ Icc z y
have h : w ∈ (s ∪ t) ∩ Icc z y → w ∈ t ∩ Icc z y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ w ∈ (s ∪ t) ∩ Icc z y ↔ w ∈ t ∩ Icc z y
have h₁ : w ∈ t ∩ Icc z y → w ∈ (s ∪ t) ∩ Icc z y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
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
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have this : (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⟩
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have inr : eVariationOn f (t ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
Tactic: rw [this, hft zt yt zy]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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))
⊢ eVariationOn f ((s ∪ t) ∩ Icc z y) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
have inr₁ : ENNReal.ofReal ((↑l : ℝ) * (y - z)) = ENNReal.ofReal ((↑l : ℝ) * (y - z))
Tactic: rw [this, hft zt yt zy]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ HasConstantSpeedOnWith f (Icc x z) l
have inl : ∀ (xy : x ≤ y), HasConstantSpeedOnWith f (Icc x z) l
Tactic: rcases le_total x y with (xy | yx)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ HasConstantSpeedOnWith f (Icc x z) l
have inr : ∀ (yx : y ≤ x), HasConstantSpeedOnWith f (Icc x z) l
Tactic: rcases le_total x y with (xy | yx)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ HasConstantSpeedOnWith f (Icc x z) l
have inl : ∀ (yz : y ≤ z), HasConstantSpeedOnWith f (Icc x z) l
Tactic: rcases le_total y z with (yz | zy)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ HasConstantSpeedOnWith f (Icc x z) l
have inl₁ : ∀ (zy : z ≤ y), HasConstantSpeedOnWith f (Icc x z) l
Tactic: rcases le_total y z with (yz | zy)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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 z) l
have inl : HasConstantSpeedOnWith f (Icc x y ∪ Icc y z) l
Tactic: rw [← Set.Icc_union_Icc_eq_Icc xy yz]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inl : eVariationOn f (Icc (max x u) (min z 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)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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))
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inl₁ : eVariationOn f (Icc u (min z 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)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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))
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inl₂ : eVariationOn f (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)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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))
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inl₃ : eVariationOn f (Icc u v) = eVariationOn f (Icc x y ∩ Icc u v)
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)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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)
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inl₄ : eVariationOn f (Icc u v) = eVariationOn f (Icc (max x u) (min y v))
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)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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))
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inl₅ : eVariationOn f (Icc u v) = eVariationOn f (Icc u (min y v))
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)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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))
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inl₆ : eVariationOn f (Icc u v) = eVariationOn f (Icc u v)
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)]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inr : eVariationOn f (Icc (max x u) (min z 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]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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))
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inr₁ : eVariationOn f (Icc u (min z 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]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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))
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inr₂ : eVariationOn f (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]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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))
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inr₃ : eVariationOn f (Icc u v) = eVariationOn f (Icc y z ∩ Icc u v)
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]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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)
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inr₄ : eVariationOn f (Icc u v) = eVariationOn f (Icc (max y u) (min z v))
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]