Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case ha
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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x✝ y✝ x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := ⋯
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ (γ ∘ η) (η 1) = y

pp: case hb
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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x✝ y✝ x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := ⋯
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ (γ ∘ η) (η 0) = x

pp: case hab
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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x✝ y✝ x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := ⋯
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ η 1 ≤ η 0

Tactic:
<;>

Goal state after:
case ha
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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x✝ y✝ x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := ⋯
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ (γ ∘ η) (η 1) = y

case hb
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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x✝ y✝ x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := ⋯
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ (γ ∘ η) (η 0) = x

case hab
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)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x✝ y✝ x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := ⋯
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ η 1 ≤ η 0