awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw rw₁ : (↑l : ℝ) * (y - x) = (↑l : ℝ) * (y - x)
⊢ (y - x) * (↑l : ℝ) = (↑l : ℝ) * (y - x)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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
⊢ (↑l : ℝ) * (y - x) = variationOnFromTo (f ∘ φ) s x y

Tactic:
(hfφ.2 xs ys).symm

Premises used: And.right, Eq.symm
-- 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
⊢ variationOnFromTo (f ∘ φ) s x y = variationOnFromTo f (φ '' s) (φ x) (φ y)

Tactic:
(variationOnFromTo.comp_eq_of_monotoneOn f φ φm xs ys)

Premises used: variationOnFromTo.comp_eq_of_monotoneOn
-- 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
⊢ variationOnFromTo f (φ '' s) (φ x) (φ y) = (↑l' : ℝ) * (φ y - φ x)

Tactic:
(hf.2 ⟨x, xs, rfl⟩ ⟨y, ys, rfl⟩)

Premises used: And.right, And.intro, Exists.intro, rfl
-- 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
rw rw₁ : (φ y - φ x) * (↑l' : ℝ) = (φ y - φ x) * (↑l' : ℝ)
⊢ (↑l' : ℝ) * (φ y - φ x) = (φ y - φ x) * (↑l' : ℝ)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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
l₁ : (y - x) * (↑l : ℝ) = (↑l : ℝ) * (y - x)
l₂ : (↑l' : ℝ) * (φ y - φ x) = (φ y - φ x) * (↑l' : ℝ)
⊢ (y - x) * (↑l : ℝ) = (φ 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]

Premises used: HSub.hSub, Function.comp, variationOnFromTo.comp_eq_of_monotoneOn, And.right, And.intro, variationOnFromTo, Exists.intro, Set.image, Eq.symm, rfl
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
s t : Set ℝ
x : ℝ
hfs : HasUnitSpeedOn f s
hft : HasUnitSpeedOn f t
hs : IsGreatest s x
ht : IsLeast t x
⊢ HasUnitSpeedOn f (s ∪ t)

Tactic:
HasConstantSpeedOnWith.union hfs hft hs ht

Premises used: HasConstantSpeedOnWith.union, HasUnitSpeedOn
-- Module: Mathlib.Analysis.ConstantSpeed
Goal:
E : Type u_2
inst : PseudoEMetricSpace E
f : ℝ → E
x y z : ℝ
hfs : HasUnitSpeedOn f (Icc x y)
hft : HasUnitSpeedOn f (Icc y z)
⊢ HasUnitSpeedOn f (Icc x z)

Tactic:
HasConstantSpeedOnWith.Icc_Icc hfs hft

Premises used: HasUnitSpeedOn, HasConstantSpeedOnWith.Icc_Icc
-- Module: Mathlib.Analysis.ConstantSpeed
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 : ℝ) ↦ (↑1 : ℝ) / (↑1 : ℝ) * (y - x) + φ x) s

Tactic:
HasConstantSpeedOnWith.ratio one_ne_zero φm hfφ hf xs

Premises used: HasConstantSpeedOnWith.ratio, one_ne_zero
-- Module: Mathlib.Analysis.ConstantSpeed
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
h : ∀ (x_1 : ℝ), x_1 - x = (↑1 : ℝ) / (↑1 : ℝ) * (x_1 - x)
⊢ EqOn φ (fun (y : ℝ) ↦ y - x + φ x) s

Tactic:
convert! HasConstantSpeedOnWith.ratio one_ne_zero φm hfφ hf xs using 3

Premises used: HasConstantSpeedOnWith.ratio, one_ne_zero
-- Module: Mathlib.Analysis.ConstantSpeed
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
x_1 : ℝ
⊢ x_1 - x = (↑1 : ℝ) / (↑1 : ℝ) * (x_1 - x)

Tactic:
simp
-- Module: Mathlib.Analysis.ConstantSpeed
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)
⊢ HasUnitSpeedOn f (φ '' Icc 0 s)

Tactic:
rw [← φst] at hf
-- Module: Mathlib.Analysis.ConstantSpeed
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 φ (fun (y : ℝ) ↦ y - 0 + φ 0) (Icc 0 s)

Tactic:
unique_unit_speed φm hfφ hf ⟨le_rfl, hs⟩

Premises used: le_rfl, unique_unit_speed, And.intro
-- Module: Mathlib.Analysis.ConstantSpeed
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)
h : Eq (α := ℝ → ℝ) id fun (y : ℝ) ↦ y - 0 + φ 0
⊢ EqOn φ id (Icc 0 s)

Tactic:
convert! unique_unit_speed φm hfφ hf ⟨le_rfl, hs⟩ using 1

Premises used: le_rfl, unique_unit_speed, And.intro
-- Module: Mathlib.Analysis.ConstantSpeed
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 ∈ φ '' Icc 0 s

Tactic:
simp only [φst, ht, mem_Icc, le_refl, and_self]

Premises used: le_refl, and_self, Set.mem_Icc
-- Module: Mathlib.Analysis.ConstantSpeed
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 ∈ φ '' Icc 0 s

Tactic:
have hm : 0 ∈ φ '' Icc 0 s := by simp only [φst, ht, mem_Icc, le_refl, and_self]
-- Module: Mathlib.Analysis.ConstantSpeed
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
obtain : ∀ (x : ℝ) (xs : x ∈ Icc 0 s) (hx : φ x = 0), φ 0 = 0
⊢ φ 0 = 0

Tactic:
obtain ⟨x, xs, hx⟩ := hm
-- Module: Mathlib.Analysis.ConstantSpeed
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
apply : 0 ≤ φ 0
⊢ φ 0 = 0

Tactic:
apply le_antisymm ((φm ⟨le_rfl, hs⟩ xs xs.1).trans_eq hx) _

Premises used: le_rfl, LE.le.trans_eq, le_antisymm, And.left, And.intro
-- Module: Mathlib.Analysis.ConstantSpeed
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
⊢ MapsTo φ (Icc 0 s) (Icc 0 t)

Tactic:
have := φst ▸ mapsTo_image φ (Icc 0 s)
-- Module: Mathlib.Analysis.ConstantSpeed
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
this : MapsTo φ (Icc 0 s) (Icc 0 t)
⊢ LE.le (α := ℝ) 0 0 ∧ 0 ≤ s

Tactic:
⟨le_rfl, hs⟩

Premises used: le_rfl, And.intro
-- Module: Mathlib.Analysis.ConstantSpeed
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
this : MapsTo φ (Icc 0 s) (Icc 0 t)
⊢ LE.le (α := ℝ) 0 0 ∧ 0 ≤ s

Tactic:
exact ⟨le_rfl, hs⟩
-- Module: Mathlib.Analysis.ConstantSpeed
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
this : MapsTo φ (Icc 0 s) (Icc 0 t)
⊢ 0 ≤ φ 0

Tactic:
exact (mem_Icc.mp (@this 0 (by rw [mem_Icc]; exact ⟨le_rfl, hs⟩))).1

Premises used: And.left, Iff.mp, Set.mem_Icc
-- Module: Mathlib.Analysis.ConstantSpeed
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

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
-- Module: Mathlib.Analysis.ConstantSpeed
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
h : Eq (α := ℝ → ℝ) id fun (y : ℝ) ↦ y
⊢ Eq (α := ℝ → ℝ) id fun (y : ℝ) ↦ y - 0 + φ 0

Tactic:
simp only [tsub_zero, this, add_zero]

Premises used: tsub_zero, add_zero
-- Module: Mathlib.Analysis.ConstantSpeed
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

Tactic:
rfl
-- Module: Mathlib.Analysis.ConstantSpeed
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
dsimp : edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0
⊢ edist (naturalParameterization f s a (variationOnFromTo f s a b)) (f b) = 0

Tactic:
dsimp only [naturalParameterization]

Premises used: naturalParameterization
-- Module: Mathlib.Analysis.ConstantSpeed
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
⊢ Nonempty α

Tactic:
haveI : Nonempty α := ⟨a⟩
-- Module: Mathlib.Analysis.ConstantSpeed
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 α
⊢ 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⟩

Premises used: Function.invFunOn_pos, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.ConstantSpeed
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
⊢ 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⟩

Premises used: Function.invFunOn_pos, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.ConstantSpeed
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
⊢ 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

Premises used: variationOnFromTo.eq_left_iff
-- Module: Mathlib.Analysis.ConstantSpeed
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 (Function.invFunOn (variationOnFromTo f s a) s (variationOnFromTo f s a b)) b = 0
⊢ edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0

Tactic:
apply variationOnFromTo.edist_zero_of_eq_zero hf cs bs hc

Premises used: variationOnFromTo.edist_zero_of_eq_zero
-- Module: Mathlib.Analysis.ConstantSpeed
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
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))
⊢ HasConstantSpeedOnWith (naturalParameterization f s a) (variationOnFromTo f s a '' s) 1

Tactic:
rw [hasConstantSpeedOnWith_iff_ordered]

Premises used: hasConstantSpeedOnWith_iff_ordered
-- Module: Mathlib.Analysis.ConstantSpeed
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))
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))
⊢ 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)

Premises used: le_total
-- Module: Mathlib.Analysis.ConstantSpeed
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
inl : (variationOnFromTo f s a '' s ∩ {variationOnFromTo f s a c}).Subsingleton
⊢ 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:
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]

Premises used: Set.Icc_self, sub_self, le_antisymm, variationOnFromTo.monotoneOn, eVariationOn.subsingleton, ENNReal.ofReal_zero, NNReal.coe_one, one_mul
-- Module: Mathlib.Analysis.ConstantSpeed
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
⊢ (variationOnFromTo f s a '' s ∩ {variationOnFromTo f s a c}).Subsingleton

Tactic:
fun x hx y hy => hx.2.trans hy.2.symm

Premises used: And.right, Set.Subsingleton, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.ConstantSpeed
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
⊢ (variationOnFromTo f s a '' s ∩ {variationOnFromTo f s a c}).Subsingleton

Tactic:
exact fun x hx y hy => hx.2.trans hy.2.symm
-- Module: Mathlib.Analysis.ConstantSpeed
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
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)
⊢ 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:
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]

Premises used: sub_eq_add_neg, neg_neg, add_comm, variationOnFromTo.add, NNReal.coe_one, variationOnFromTo.eq_neg_swap, one_mul
-- Module: Mathlib.Analysis.ConstantSpeed
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
inr :
  eVariationOn (naturalParameterization f s a ∘ variationOnFromTo f s a) (s ∩ Icc b c) =
    ENNReal.ofReal (variationOnFromTo f s 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 (variationOnFromTo f s b c)

Tactic:
rw [←
      eVariationOn.comp_inter_Icc_eq_of_monotoneOn (naturalParameterization f s a) _
        (variationOnFromTo.monotoneOn hf as) bs cs]

Premises used: eVariationOn.comp_inter_Icc_eq_of_monotoneOn, naturalParameterization, variationOnFromTo.monotoneOn
-- Module: Mathlib.Analysis.ConstantSpeed
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
inr : eVariationOn f (s ∩ Icc b c) = ENNReal.ofReal (variationOnFromTo f s b c)
inr₁ : ∀ ⦃x : α⦄, x ∈ s ∩ Icc b c → edist ((naturalParameterization f s a ∘ variationOnFromTo f s a) x) (f x) = 0
⊢ eVariationOn (naturalParameterization f s a ∘ variationOnFromTo f s a) (s ∩ Icc b c) =
    ENNReal.ofReal (variationOnFromTo f s b c)

Tactic:
rw [@eVariationOn.eq_of_edist_zero_on _ _ _ _ _ f]

Premises used: eVariationOn.eq_of_edist_zero_on
-- Module: Mathlib.Analysis.ConstantSpeed
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
inr : eVariationOn f (s ∩ Icc b c) = ENNReal.ofReal (eVariationOn f (s ∩ Icc b c)).toReal
inr₁ inr₂ : eVariationOn f (s ∩ Icc b c) = eVariationOn f (s ∩ Icc b c)
⊢ eVariationOn f (s ∩ Icc b c) = ENNReal.ofReal (variationOnFromTo f s b c)

Tactic:
rw [variationOnFromTo.eq_of_le _ _ bc, ENNReal.ofReal_toReal (hf b c bs cs)]

Premises used: ENNReal.ofReal_toReal, variationOnFromTo.eq_of_le
-- Module: Mathlib.Analysis.ConstantSpeed
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
x : α
xs : x ∈ s
left : b ≤ x
right : x ≤ c
⊢ edist ((naturalParameterization f s a ∘ variationOnFromTo f s a) x) (f x) = 0

Tactic:
edist_naturalParameterization_eq_zero hf as xs

Premises used: naturalParameterization, edist_naturalParameterization_eq_zero
-- Module: Mathlib.Analysis.ConstantSpeed
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
x : α
xs : x ∈ s
left : b ≤ x
right : x ≤ c
⊢ edist ((naturalParameterization f s a ∘ variationOnFromTo f s a) x) (f x) = 0

Tactic:
exact edist_naturalParameterization_eq_zero hf as xs

Premises used: edist_naturalParameterization_eq_zero
-- Module: Mathlib.Analysis.Convex.AmpleSet
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
x : F
_ :
  Membership.mem (γ := Set F) univ x →
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn univ x) : Set F) (univ : Set F)
⊢ Membership.mem (γ := Set F) univ x →
    Eq (α := Set F) ((convexHull ℝ : (a : Set F) → Set F) (connectedComponentIn univ x) : Set F) (univ : Set F)

Tactic:
_