Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
r : ℝ
r_pos : r > 0
hr :
  ball (↑(extChartAt I x) x) r ∩ range ↑I ⊆
    (extChartAt I x).target ∩ {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
A : ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I)
h'y : y ∈ (chartAt H x).source
η : ℝ →ᴬ[ℝ] E := ⋯
γ : ℝ → M := ⋯
hη :
  Icc 0 1 ⊆ ⇑η ⁻¹' (extChartAt I x).target ∧ Icc 0 1 ⊆ ⇑η ⁻¹' {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 (⇑η) (Icc 0 1)
this✝¹ : riemannianEDist I x y ≤ pathELength I γ 0 1
t : ℝ
ht : t ∈ Icc 0 1
this✝ : mfderiv[Icc 0 1] γ t = mfderiv[range ↑I] ↑(extChartAt I x).symm (η t) ∘SL mfderiv[Icc 0 1] ⇑η t
this : (mfderiv[Icc 0 1] γ t) 1 = (mfderiv[range ↑I] ↑(extChartAt I x).symm (η t)) ((mfderiv[Icc 0 1] ⇑η t) 1)
⊢ ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (η t)‖ₑ ≤ ↑C

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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
r : ℝ
r_pos : r > 0
hr :
  ball (↑(extChartAt I x) x) r ∩ range ↑I ⊆
    (extChartAt I x).target ∩ {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
A : ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I)
h'y : y ∈ (chartAt H x).source
η : ℝ →ᴬ[ℝ] E := ⋯
γ : ℝ → M := ⋯
hη :
  Icc 0 1 ⊆ ⇑η ⁻¹' (extChartAt I x).target ∧ Icc 0 1 ⊆ ⇑η ⁻¹' {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 (⇑η) (Icc 0 1)
this✝¹ : riemannianEDist I x y ≤ pathELength I γ 0 1
t : ℝ
ht : t ∈ Icc 0 1
this✝ : mfderiv[Icc 0 1] γ t = mfderiv[range ↑I] ↑(extChartAt I x).symm (η t) ∘SL mfderiv[Icc 0 1] ⇑η t
this : (mfderiv[Icc 0 1] γ t) 1 = (mfderiv[range ↑I] ↑(extChartAt I x).symm (η t)) ((mfderiv[Icc 0 1] ⇑η t) 1)
⊢ ‖(mfderiv[Icc 0 1] ⇑η t) 1‖ₑ ≤
    ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap (↑(extChartAt I x) x) (↑(extChartAt I x) y))) (Icc 0 1) t) 1‖ₑ

Tactic:
· exact (hη.2 ht).le

Goal state after:
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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
r : ℝ
r_pos : r > 0
hr :
  ball (↑(extChartAt I x) x) r ∩ range ↑I ⊆
    (extChartAt I x).target ∩ {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
A : ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I)
h'y : y ∈ (chartAt H x).source
η : ℝ →ᴬ[ℝ] E := ⋯
γ : ℝ → M := ⋯
hη :
  Icc 0 1 ⊆ ⇑η ⁻¹' (extChartAt I x).target ∧ Icc 0 1 ⊆ ⇑η ⁻¹' {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 (⇑η) (Icc 0 1)
this✝¹ : riemannianEDist I x y ≤ pathELength I γ 0 1
t : ℝ
ht : t ∈ Icc 0 1
this✝ : mfderiv[Icc 0 1] γ t = mfderiv[range ↑I] ↑(extChartAt I x).symm (η t) ∘SL mfderiv[Icc 0 1] ⇑η t
this : (mfderiv[Icc 0 1] γ t) 1 = (mfderiv[range ↑I] ↑(extChartAt I x).symm (η t)) ((mfderiv[Icc 0 1] ⇑η t) 1)
⊢ ‖(mfderiv[Icc 0 1] ⇑η t) 1‖ₑ ≤
    ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap (↑(extChartAt I x) x) (↑(extChartAt I x) y))) (Icc 0 1) t) 1‖ₑ