-- Mathlib/Analysis/ConstantSpeed.lean
theorem edist_naturalParameterization_eq_zero {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

Proof state:
case intro
α : 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
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

Tactic:
rw [variationOnFromTo.eq_left_iff hf as cs bs] at hc

Result:
case intro
α : 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
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

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
b : α
bs : b ∈ s
⊢ edist (naturalParameterization f s a (variationOnFromTo f s a b)) (f b) = 0

Tactic:
dsimp only [naturalParameterization]

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
b : α
bs : b ∈ s
⊢ edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0

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
b : α
bs : b ∈ s
this : Nonempty α
⊢ edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0

Tactic:
obtain ⟨cs, hc⟩ := Function.invFunOn_pos (b := variationOnFromTo f s a b) ⟨b, bs, rfl⟩

Result:
case intro
α : 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
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

Proof state:
case intro
α : 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
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

Result:
no goals

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
b : α
bs : b ∈ s
⊢ edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0

Tactic:
haveI : Nonempty α := ⟨a⟩

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
b : α
bs : b ∈ s
this : Nonempty α
⊢ edist ((f ∘ Function.invFunOn (variationOnFromTo f s a) s) (variationOnFromTo f s a b)) (f b) = 0