-- 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
t' : ℝ
ht' : t' ∈ Icc 0 t₁
this_1 :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) t' →L[ℝ] TangentSpace 𝓘(ℝ, E) (γ' t')) (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ' (Icc 0 t₁) t')
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (γ t')) (mfderiv% (↑(extChartAt I x) : M → E) (γ t'))
      (mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t'))
this :
  Eq (α := TangentSpace 𝓘(ℝ, E) (γ' t'))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ' (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace 𝓘(ℝ, E) (γ' t')) 1 :
      TangentSpace 𝓘(ℝ, E) (γ' t'))
    ((mfderiv% (↑(extChartAt I x) : M → E) (γ t') :
          (a : TangentSpace I (γ t')) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) (γ t')))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace I (γ t')) 1) :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) (γ t')))
⊢ enorm (E := TangentSpace I (γ t') →L[ℝ] TangentSpace 𝓘(ℝ, E) (γ' t')) (mfderiv% (↑(extChartAt I x) : M → E) (γ t')) *
      enorm (E := TangentSpace I (γ t'))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace I (γ t')) 1 :
          TangentSpace I (γ t')) ≤
    (↑C : ℝ≥0∞) *
      enorm (E := TangentSpace I (γ t'))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace I (γ t')) 1 :
          TangentSpace I (γ t'))
have bc : enorm (E := TangentSpace I (γ t') →L[ℝ] TangentSpace 𝓘(ℝ, E) (γ' t')) (mfderiv% (↑(extChartAt I x) : M → E) (γ t')) ≤
  (↑C : ℝ≥0∞)
Tactic: gcongr