-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (hypothesis)
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 : riemannianEDist I x y ≤ pathELength I γ 0 1
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ enorm (E := TangentSpace I (γ t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 1) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
        TangentSpace I (γ t)) ≤
    (↑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 this₁ : 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))
Tactic: have : mfderiv[Icc 0 1] γ t =
      (mfderiv[range I] (extChartAt I x).symm (η t)) ∘L (mfderiv[Icc 0 1] η t) := by
    apply mfderivWithin_comp
    · exact mdifferentiableWithinAt_extChartAt_symm (hη.1 ht)
    · exact η_smooth.mdifferentiableOn one_ne_zero t ht
    · exact hη.1.trans (preimage_mono (extChartAt_target_subset_range x))
    · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
      exact uniqueDiffOn_Icc zero_lt_one t ht