-- Mathlib/Analysis/ConstantSpeed.lean
theorem has_unit_speed_naturalParameterization (f : α → E) {s : Set α}
    (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) :
    HasUnitSpeedOn (naturalParameterization f s a) (variationOnFromTo f s a '' s)

Proof state:
case intro.intro.intro.intro.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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))

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]

Result:
case intro.intro.intro.intro.inl.hs
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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

Proof state:
case intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 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)]

Result:
no goals

Proof state:
case intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 (variationOnFromTo f s b c)

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

Result:
case intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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 b c) =
    ENNReal.ofReal (variationOnFromTo f s b c)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a : α
as : a ∈ s
⊢ HasUnitSpeedOn (naturalParameterization f s a) (variationOnFromTo f s a '' s)

Tactic:
dsimp only [HasUnitSpeedOn]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : 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