Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: case e'_2.e'_6
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 : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.symmL ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
y : M
hy : ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C
h'y : y ∈ (chartAt H x).source
A : ↑(extChartAt I x).symm (↑(extChartAt I x) y) = y
e_1✝ :
  (TangentSpace 𝓘(ℝ, E) (↑(extChartAt I x) y) →L[ℝ] TangentSpace I (↑(extChartAt I x).symm (↑(extChartAt I x) y))) =
    (E →L[ℝ] TangentSpace I y)
e_4✝ : TangentSpace I (↑(extChartAt I x).symm (↑(extChartAt I x) y)) = TangentSpace I y
⊢ NormedAddCommGroup.toSeminormedAddCommGroup = NormedAddCommGroup.toSeminormedAddCommGroup

pp: case e'_2.e'_10
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 : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.symmL ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
y : M
hy : ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C
h'y : y ∈ (chartAt H x).source
A : ↑(extChartAt I x).symm (↑(extChartAt I x) y) = y
e_1✝ :
  (TangentSpace 𝓘(ℝ, E) (↑(extChartAt I x) y) →L[ℝ] TangentSpace I (↑(extChartAt I x).symm (↑(extChartAt I x) y))) =
    (E →L[ℝ] TangentSpace I y)
e_4✝ : TangentSpace I (↑(extChartAt I x).symm (↑(extChartAt I x) y)) = TangentSpace I y
e_6✝ : NormedAddCommGroup.toSeminormedAddCommGroup ≍ NormedAddCommGroup.toSeminormedAddCommGroup
⊢ (instInnerProductSpaceReal (↑(extChartAt I x).symm (↑(extChartAt I x) y))).toNormedSpace ≍
    (instInnerProductSpaceReal y).toNormedSpace

Tactic:
<;>

Goal state after:
case e'_2.e'_6
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 : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.symmL ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
y : M
hy : ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C
h'y : y ∈ (chartAt H x).source
A : ↑(extChartAt I x).symm (↑(extChartAt I x) y) = y
e_1✝ :
  (TangentSpace 𝓘(ℝ, E) (↑(extChartAt I x) y) →L[ℝ] TangentSpace I (↑(extChartAt I x).symm (↑(extChartAt I x) y))) =
    (E →L[ℝ] TangentSpace I y)
e_4✝ : TangentSpace I (↑(extChartAt I x).symm (↑(extChartAt I x) y)) = TangentSpace I y
⊢ NormedAddCommGroup.toSeminormedAddCommGroup = NormedAddCommGroup.toSeminormedAddCommGroup

case e'_2.e'_10
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 : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.symmL ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
y : M
hy : ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C
h'y : y ∈ (chartAt H x).source
A : ↑(extChartAt I x).symm (↑(extChartAt I x) y) = y
e_1✝ :
  (TangentSpace 𝓘(ℝ, E) (↑(extChartAt I x) y) →L[ℝ] TangentSpace I (↑(extChartAt I x).symm (↑(extChartAt I x) y))) =
    (E →L[ℝ] TangentSpace I y)
e_4✝ : TangentSpace I (↑(extChartAt I x).symm (↑(extChartAt I x) y)) = TangentSpace I y
e_6✝ : NormedAddCommGroup.toSeminormedAddCommGroup ≍ NormedAddCommGroup.toSeminormedAddCommGroup
⊢ (instInnerProductSpaceReal (↑(extChartAt I x).symm (↑(extChartAt I x) y))).toNormedSpace ≍
    (instInnerProductSpaceReal y).toNormedSpace