Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case hg
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ MDiffAt[f '' Icc a b] γ (f t)

pp: case hf
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ MDiffAt[Icc a b] f t

pp: case h
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ Icc a b ⊆ f ⁻¹' f '' Icc a b

pp: case hxs
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ UniqueMDiffAt[Icc a b] t

Tactic:
· apply hγ _ (mem_image_of_mem _ ht)

Goal state after:
case hf
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ MDiffAt[Icc a b] f t

case h
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ Icc a b ⊆ f ⁻¹' f '' Icc a b

case hxs
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h✝ : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
B : ∀ t ∈ Icc a b, HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ UniqueMDiffAt[Icc a b] t