-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ≥0∞)
r : ℝ
r_pos : r > 0
hr :
  ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E) ⊆
    (extChartAt I x).target ∩
      {y : E |
        enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
          (↑C : ℝ≥0∞)}
A : (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E))
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
η : ℝ →ᴬ[ℝ] E := ContinuousAffineMap.lineMap ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
γ : ℝ → M := (↑(extChartAt I x).symm : E → M) ∘ (⇑η : (a : ℝ) → E)
hη :
  Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → E) ⁻¹' (extChartAt I x).target) ∧
    Subset (α := Set ℝ) (Icc 0 1)
      (preimage (β := E) (⇑η : (a : ℝ) → E)
        {y : E |
          enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
              (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
            (↑C : ℝ≥0∞)})
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, E) (M' := E) 1 (⇑η : (a : ℝ) → E) (Icc 0 1)
this_1 : riemannianEDist I x y ≤ pathELength I γ 0 1
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
this_2 :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ t)) (mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 1) t)
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(ℝ, E) (M := E) ((η : (a : ℝ) → E) t : E))
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((η : (a : ℝ) → E) t))
      (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) (⇑η : (a : ℝ) → E) (Icc 0 1) t))
this :
  Eq (α := TangentSpace I (γ t))
    ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 1) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
      TangentSpace I (γ t))
    ((mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((η : (a : ℝ) → E) t) :
          (a : TangentSpace 𝓘(ℝ, E) ((η : (a : ℝ) → E) t)) →
            TangentSpace I ((↑(extChartAt I x).symm : E → M) ((η : (a : ℝ) → E) t)))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) (⇑η : (a : ℝ) → E) (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((η : (a : ℝ) → E) t))
            1 :
          TangentSpace 𝓘(ℝ, E) (M := E) ((η : (a : ℝ) → E) t : E)) :
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((η : (a : ℝ) → E) t)))
h₁ :
  enorm (E := TangentSpace 𝓘(ℝ, E) (M := E) ((η : (a : ℝ) → E) t : E) →L[ℝ] TangentSpace I (γ t))
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((η : (a : ℝ) → E) t)) ≤
    (↑C : ℝ≥0∞)
⊢ enorm (E := TangentSpace 𝓘(ℝ, E) (M := E) ((η : (a : ℝ) → E) t : E) →L[ℝ] TangentSpace I (γ t))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((η : (a : ℝ) → E) t)) *
      enorm (E := TangentSpace 𝓘(ℝ, E) (M := E) ((η : (a : ℝ) → E) t : E))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) (⇑η : (a : ℝ) → E) (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((η : (a : ℝ) → E) t))
            1 :
          TangentSpace 𝓘(ℝ, E) (M := E) ((η : (a : ℝ) → E) t : E)) ≤
    (↑C : ℝ≥0∞) *
      enorm (E := E)
        ((fderivWithin ℝ
                (⇑(ContinuousAffineMap.lineMap ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)) :
                  (a : ℝ) → E)
                (Icc 0 1) t :
              (a : ℝ) → E)
            1 :
          E)
have h₂ : enorm (E := TangentSpace 𝓘(ℝ, E) (M := E) ((η : (a : ℝ) → E) t : E))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) (⇑η : (a : ℝ) → E) (Icc 0 1) t :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((η : (a : ℝ) → E) t))
        1 :
      TangentSpace 𝓘(ℝ, E) (M := E) ((η : (a : ℝ) → E) t : E)) ≤
  enorm (E := E)
    ((fderivWithin ℝ
            (⇑(ContinuousAffineMap.lineMap ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)) :
              (a : ℝ) → E)
            (Icc 0 1) t :
          (a : ℝ) → E)
        1 :
      E)
Tactic: gcongr