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
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))
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inr₅ : eVariationOn f (Icc u v) = eVariationOn f (Icc 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]
-- 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)
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))
⊢ eVariationOn f (Icc x z ∩ Icc u v) = ENNReal.ofReal ((↑l : ℝ) * (v - u))
have inr₆ : 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, ←
      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
s : Set ℝ
⊢ (∀ ⦃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
have simp : (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) ↔ eVariationOn f s = 0
Tactic: simp only [zero_mul, ENNReal.ofReal_zero, ← eVariationOn.eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) ↔ eVariationOn f s = 0
have mp : (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) → eVariationOn f s = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) ↔ eVariationOn f s = 0
have mpr : eVariationOn f s = 0 → ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
⊢ (∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) → eVariationOn f s = 0
have mp : ∀ (h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Icc x y) = 0) (hfs : eVariationOn f s ≠ 0), False
Tactic: by_contra! ⟨h, hfs⟩
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
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
⊢ False
have hfs₁ : ¬∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
Tactic: simp_rw [ne_eq, eVariationOn.eq_zero_iff] at hfs h
Cleared hypotheses: h, hfs
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
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
⊢ False
have 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
Tactic: simp_rw [ne_eq, eVariationOn.eq_zero_iff] at hfs h
Cleared hypotheses: h, hfs
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
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
⊢ False
have hfs₁ : ∃ x ∈ s, ∃ y ∈ s, edist (f x) (f y) ≠ 0
Tactic: push Not at hfs
Cleared hypotheses: hfs
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ False
have mp : ∀ (x : ℝ) (xs : x ∈ s) (y : ℝ) (ys : y ∈ s) (hxy : edist (f x) (f y) ≠ 0), False
Tactic: obtain ⟨x, xs, y, ys, hxy⟩ := hfs
Cleared hypotheses: hfs
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ False
have mp : ∀ (xy : x ≤ y), False
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
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
⊢ False
have mp₁ : ∀ (yx : y ≤ x), False
Tactic: rcases le_total x y with (xy | yx)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
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
⊢ False
have hxy₁ : edist (f y) (f x) ≠ 0
Tactic: rw [edist_comm] at hxy
Cleared hypotheses: hxy, yx
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ φ y = (fun (y : ℝ) ↦ (↑l : ℝ) / (↑l' : ℝ) * (y - x) + φ x) y
have rw : (φ y - φ x) * (↑l' : ℝ) = (y - x) * (↑l : ℝ)
Tactic: rw [← sub_eq_iff_eq_add, mul_comm, ← mul_div_assoc, eq_div_iff (NNReal.coe_ne_zero.mpr hl')]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ (φ y - φ x) * (↑l' : ℝ) = (y - x) * (↑l : ℝ)
have 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 : ℝ)
Tactic: rw [hasConstantSpeedOnWith_iff_variationOnFromTo_eq] at hf
Cleared hypotheses: hf, x, xs, y, ys
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ (φ y - φ x) * (↑l' : ℝ) = (y - x) * (↑l : ℝ)
have 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 : ℝ)
Tactic: rw [hasConstantSpeedOnWith_iff_variationOnFromTo_eq] at hfφ
Cleared hypotheses: hfφ, hf, x, xs, y, ys
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ (φ y - φ x) * (↑l' : ℝ) = (y - x) * (↑l : ℝ)
have symm : (y - x) * (↑l : ℝ) = (φ y - φ x) * (↑l' : ℝ)
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ (y - x) * (↑l : ℝ) = (↑l : ℝ) * (y - x)
have rw : (↑l : ℝ) * (y - x) = (↑l : ℝ) * (y - x)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ (↑l' : ℝ) * (φ y - φ x) = (φ y - φ x) * (↑l' : ℝ)
have rw : (φ y - φ x) * (↑l' : ℝ) = (φ y - φ x) * (↑l' : ℝ)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
⊢ (y - x) * (↑l : ℝ) = (φ y - φ x) * (↑l' : ℝ)
have l₁ : (y - x) * (↑l : ℝ) = (↑l : ℝ) * (y - x)
Tactic: calc
    (y - x) * l = l * (y - x) := by rw [mul_comm]
    _ = variationOnFromTo (f ∘ φ) s x y := (hfφ.2 xs ys).symm
    _ = variationOnFromTo f (φ '' s) (φ x) (φ y) :=
      (variationOnFromTo.comp_eq_of_monotoneOn f φ φm xs ys)
    _ = l' * (φ y - φ x) := (hf.2 ⟨x, xs, rfl⟩ ⟨y, ys, rfl⟩)
    _ = (φ y - φ x) * l' := by rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
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
l₁ : (y - x) * (↑l : ℝ) = (↑l : ℝ) * (y - x)
⊢ (y - x) * (↑l : ℝ) = (φ y - φ x) * (↑l' : ℝ)
have l₂ : (↑l' : ℝ) * (φ y - φ x) = (φ y - φ x) * (↑l' : ℝ)
Tactic: calc
    (y - x) * l = l * (y - x) := by rw [mul_comm]
    _ = variationOnFromTo (f ∘ φ) s x y := (hfφ.2 xs ys).symm
    _ = variationOnFromTo f (φ '' s) (φ x) (φ y) :=
      (variationOnFromTo.comp_eq_of_monotoneOn f φ φm xs ys)
    _ = l' * (φ y - φ x) := (hf.2 ⟨x, xs, rfl⟩ ⟨y, ys, rfl⟩)
    _ = (φ y - φ x) * l' := by rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s 1
hf : HasConstantSpeedOnWith f (φ '' s) 1
x : ℝ
xs : x ∈ s
⊢ EqOn φ (fun (y : ℝ) ↦ y - x + φ x) s
have h : ∀ (x_1 : ℝ), x_1 - x = (↑1 : ℝ) / (↑1 : ℝ) * (x_1 - x)
Tactic: convert! HasConstantSpeedOnWith.ratio one_ne_zero φm hfφ hf xs using 3
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (Icc 0 t)
⊢ EqOn φ id (Icc 0 s)
have hf₁ : HasUnitSpeedOn f (φ '' Icc 0 s)
Tactic: rw [← φst] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
⊢ EqOn φ id (Icc 0 s)
have h : Eq (α := ℝ → ℝ) id fun (y : ℝ) ↦ y - 0 + φ 0
Tactic: convert! unique_unit_speed φm hfφ hf ⟨le_rfl, hs⟩ using 1
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
⊢ φ 0 = 0
have hm : 0 ∈ φ '' Icc 0 s
Tactic: have hm : 0 ∈ φ '' Icc 0 s := by simp only [φst, ht, mem_Icc, le_refl, and_self]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
hm : 0 ∈ φ '' Icc 0 s
⊢ φ 0 = 0
have obtain : ∀ (x : ℝ) (xs : x ∈ Icc 0 s) (hx : φ x = 0), φ 0 = 0
Tactic: obtain ⟨x, xs, hx⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x : ℝ
xs : x ∈ Icc 0 s
hx : φ x = 0
⊢ φ 0 = 0
have apply : 0 ≤ φ 0
Tactic: apply le_antisymm ((φm ⟨le_rfl, hs⟩ xs xs.1).trans_eq hx) _
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
x : ℝ
xs : x ∈ Icc 0 s
hx : φ x = 0
⊢ 0 ≤ φ 0
have this : MapsTo φ (Icc 0 s) (Icc 0 t)
Tactic: have := φst ▸ mapsTo_image φ (Icc 0 s)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
⊢ Eq (α := ℝ → ℝ) id fun (y : ℝ) ↦ y - 0 + φ 0
have this : φ 0 = 0
Tactic: have : φ 0 = 0 := by
    have hm : 0 ∈ φ '' Icc 0 s := by simp only [φst, ht, mem_Icc, le_refl, and_self]
    obtain ⟨x, xs, hx⟩ := hm
    apply le_antisymm ((φm ⟨le_rfl, hs⟩ xs xs.1).trans_eq hx) _
    have := φst ▸ mapsTo_image φ (Icc 0 s)
    exact (mem_Icc.mp (@this 0 (by rw [mem_Icc]; exact ⟨le_rfl, hs⟩))).1
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s t : ℝ
hs : 0 ≤ s
ht : 0 ≤ t
φ : ℝ → ℝ
φm : MonotoneOn φ (Icc 0 s)
φst : φ '' Icc 0 s = Icc 0 t
hfφ : HasUnitSpeedOn (f ∘ φ) (Icc 0 s)
hf : HasUnitSpeedOn f (φ '' Icc 0 s)
this : φ 0 = 0
⊢ Eq (α := ℝ → ℝ) id fun (y : ℝ) ↦ y - 0 + φ 0
have h : Eq (α := ℝ → ℝ) id fun (y : ℝ) ↦ y
Tactic: simp only [tsub_zero, this, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
⊢ edist (naturalParameterization f s a (variationOnFromTo f s a b)) (f b) = 0
have dsimp : edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0
Tactic: dsimp only [naturalParameterization]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
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
⊢ edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0
have this : Nonempty α
Tactic: haveI : Nonempty α := ⟨a⟩
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
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
this : Nonempty α
⊢ edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0
have cs : Function.invFunOn (variationOnFromTo f s a) s (variationOnFromTo f s a b) ∈ s
Tactic: obtain ⟨cs, hc⟩ := Function.invFunOn_pos (b := variationOnFromTo f s a b) ⟨b, bs, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
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
this : Nonempty α
cs : Function.invFunOn (variationOnFromTo f s a) s (variationOnFromTo f s a b) ∈ s
⊢ edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0
have hc : variationOnFromTo f s a (Function.invFunOn (variationOnFromTo f s a) s (variationOnFromTo f s a b)) =
  variationOnFromTo f s a b
Tactic: obtain ⟨cs, hc⟩ := Function.invFunOn_pos (b := variationOnFromTo f s a b) ⟨b, bs, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (hypothesis)
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
this : Nonempty α
cs : Function.invFunOn (variationOnFromTo f s a) s (variationOnFromTo f s a b) ∈ s
hc :
  variationOnFromTo f s a (Function.invFunOn (variationOnFromTo f s a) s (variationOnFromTo f s a b)) =
    variationOnFromTo f s a b
⊢ edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0
have hc₁ : variationOnFromTo f s (Function.invFunOn (variationOnFromTo f s a) s (variationOnFromTo f s a b)) b = 0
Tactic: rw [variationOnFromTo.eq_left_iff hf as cs bs] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
⊢ HasConstantSpeedOnWith (naturalParameterization f s a) (variationOnFromTo f s a '' s) 1
have rw : ∀ ⦃x : ℝ⦄,
  x ∈ variationOnFromTo f s a '' s →
    ∀ ⦃y : ℝ⦄,
      y ∈ variationOnFromTo f s a '' s →
        x ≤ y →
          eVariationOn (naturalParameterization f s a) (variationOnFromTo f s a '' s ∩ Icc x y) =
            ENNReal.ofReal ((↑1 : ℝ) * (y - x))
Tactic: rw [hasConstantSpeedOnWith_iff_ordered]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
⊢ eVariationOn (naturalParameterization f s a)
      (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) =
    ENNReal.ofReal ((↑1 : ℝ) * (variationOnFromTo f s a c - variationOnFromTo f s a b))
have inl : ∀ (cb : c ≤ b),
  eVariationOn (naturalParameterization f s a)
      (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) =
    ENNReal.ofReal ((↑1 : ℝ) * (variationOnFromTo f s a c - variationOnFromTo f s a b))
Tactic: rcases le_total c b with (cb | bc)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
inl :
  ∀ (cb : c ≤ b),
    eVariationOn (naturalParameterization f s a)
        (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) =
      ENNReal.ofReal ((↑1 : ℝ) * (variationOnFromTo f s a c - variationOnFromTo f s a b))
⊢ eVariationOn (naturalParameterization f s a)
      (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) =
    ENNReal.ofReal ((↑1 : ℝ) * (variationOnFromTo f s a c - variationOnFromTo f s a b))
have inr : ∀ (bc : b ≤ c),
  eVariationOn (naturalParameterization f s a)
      (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) =
    ENNReal.ofReal ((↑1 : ℝ) * (variationOnFromTo f s a c - variationOnFromTo f s a b))
Tactic: rcases le_total c b with (cb | bc)
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
cb : c ≤ b
⊢ eVariationOn (naturalParameterization f s a)
      (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) =
    ENNReal.ofReal ((↑1 : ℝ) * (variationOnFromTo f s a c - variationOnFromTo f s a b))
have inl : (variationOnFromTo f s a '' s ∩ {variationOnFromTo f s a c}).Subsingleton
Tactic: rw [NNReal.coe_one, one_mul, le_antisymm h (variationOnFromTo.monotoneOn hf as cs bs cb),
      sub_self, ENNReal.ofReal_zero, Icc_self, eVariationOn.subsingleton]
-- Lean 4 proof step from Mathlib.Analysis.ConstantSpeed (goal)
Goal:
α : Type u_1
inst : LinearOrder α
E : Type u_2
inst_1 : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
b : α
bs : b ∈ s
c : α
cs : c ∈ s
h : variationOnFromTo f s a b ≤ variationOnFromTo f s a c
bc : b ≤ c
⊢ eVariationOn (naturalParameterization f s a)
      (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) =
    ENNReal.ofReal ((↑1 : ℝ) * (variationOnFromTo f s a c - variationOnFromTo f s a b))
have inr : eVariationOn (naturalParameterization f s a)
    (variationOnFromTo f s a '' s ∩ Icc (variationOnFromTo f s a b) (variationOnFromTo f s a c)) =
  ENNReal.ofReal (variationOnFromTo f s b c)
Tactic: rw [NNReal.coe_one, one_mul, sub_eq_add_neg, variationOnFromTo.eq_neg_swap, neg_neg, add_comm,
      variationOnFromTo.add hf bs as cs, ← variationOnFromTo.eq_neg_swap f]