Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: 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 : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A : riemannianEDist I x y ≤ ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑g x_1) 1‖ₑ
E : pathELength I (⇑g ∘ projIcc 0 1 ⋯) 0 1 = pathELength I (γ ∘ ⇑η) 0 1
⊢ pathELength I (⇑g ∘ projIcc 0 1 ⋯) 0 1 = pathELength I γ a b

Tactic:
rw [E, pathELength_comp_of_monotoneOn zero_le_one _ η.differentiableOn]

Goal state after:
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 : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A : riemannianEDist I x y ≤ ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑g x_1) 1‖ₑ
E : pathELength I (⇑g ∘ projIcc 0 1 ⋯) 0 1 = pathELength I (γ ∘ ⇑η) 0 1
⊢ pathELength I γ (η 0) (η 1) = pathELength I γ a b

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 : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A : riemannianEDist I x y ≤ ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑g x_1) 1‖ₑ
E : pathELength I (⇑g ∘ projIcc 0 1 ⋯) 0 1 = pathELength I (γ ∘ ⇑η) 0 1
⊢ MDiff[Icc (η 0) (η 1)] γ

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 : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A : riemannianEDist I x y ≤ ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑g x_1) 1‖ₑ
E : pathELength I (⇑g ∘ projIcc 0 1 ⋯) 0 1 = pathELength I (γ ∘ ⇑η) 0 1
⊢ MonotoneOn (⇑η) (Icc 0 1)