-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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₂ : ‖γ' t₁ - γ' 0‖ₑ ≤ ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖derivWithin γ' (Icc 0 t₁) t'‖ₑ
t₃ :
  ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖derivWithin γ' (Icc 0 t₁) t'‖ₑ =
    ∫⁻ (t' : ℝ) in Icc 0 t₁,
      enorm (E := TangentSpace 𝓘(ℝ, E) (γ' t'))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ' (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace 𝓘(ℝ, E) (γ' t'))
            1 :
          TangentSpace 𝓘(ℝ, E) (γ' t'))
t₄ :
  ∫⁻ (t' : ℝ) in Icc 0 t₁,
      enorm (E := TangentSpace 𝓘(ℝ, E) (γ' t'))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ' (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace 𝓘(ℝ, E) (γ' t'))
            1 :
          TangentSpace 𝓘(ℝ, E) (γ' t')) ≤
    ∫⁻ (t' : ℝ) in Icc 0 t₁,
      (↑C : ℝ≥0∞) *
        enorm (E := TangentSpace I (γ t'))
          ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace I (γ t')) 1 :
            TangentSpace I (γ t'))
t₅ :
  ∫⁻ (t' : ℝ) in Icc 0 t₁,
      (↑C : ℝ≥0∞) *
        enorm (E := TangentSpace I (γ t'))
          ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace I (γ t')) 1 :
            TangentSpace I (γ t')) =
    (↑C : ℝ≥0∞) * pathELength I γ 0 t₁
t₆ : (↑C : ℝ≥0∞) * pathELength I γ 0 t₁ ≤ (↑C : ℝ≥0∞) * pathELength I γ 0 1
t₇ : (↑C : ℝ≥0∞) * pathELength I γ 0 1 < (↑C : ℝ≥0∞) * ((↑r : ℝ≥0∞) / (↑C : ℝ≥0∞))
⊢ ‖γ' t₁ - γ' 0‖ₑ < (↑r : ℝ≥0∞)

Tactic:
calc
      ‖γ' t₁ - γ' 0‖ₑ
    _ ≤ ∫⁻ t' in Icc 0 t₁, ‖derivWithin γ' (Icc 0 t₁) t'‖ₑ := by
      apply enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc _ ht₁0
      rwa [← contMDiffOn_iff_contDiffOn]
    _ = ∫⁻ t' in Icc 0 t₁, ‖mfderiv[Icc 0 t₁] γ' t' 1‖ₑ := by
      simp_rw [← fderivWithin_derivWithin, mfderivWithin_eq_fderivWithin]
      rfl
    _ ≤ ∫⁻ t' in Icc 0 t₁, C * ‖mfderiv[Icc 0 t₁] γ t' 1‖ₑ := by
      apply setLIntegral_mono' measurableSet_Icc (fun t' ht' ↦ ?_)
      have : mfderiv[Icc 0 t₁] γ' t' =
          (mfderiv% (extChartAt I x) (γ t')) ∘L (mfderiv[Icc 0 t₁] γ t') := by
        apply mfderiv_comp_mfderivWithin
        · refine mdifferentiableAt_extChartAt (uc' ?_)
          apply t₁_mem ht'
        · exact (γ_smooth.mdifferentiable one_ne_zero).mdifferentiableOn _ ht'
        · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
          exact uniqueDiffOn_Icc h't' _ ht'
      have : mfderiv[Icc 0 t₁] γ' t' 1 =
          (mfderiv% (extChartAt I x) (γ t')) (mfderiv[Icc 0 t₁] γ t' 1) :=
        congr($this 1)
      rw [this]
      apply (ContinuousLinearMap.le_opNorm_enorm _ _).trans
      gcongr
      refine (hu ?_).le
      apply t₁_mem ht'
    _ = C * pathELength I γ 0 t₁ := by
      rw [lintegral_const_mul' _ _ ENNReal.coe_ne_top,
          pathELength_eq_lintegral_mfderivWithin_Icc]
    _ ≤ C * pathELength I γ 0 1 := by
      gcongr
    _ < C * (r / C) := by
      gcongr
      · exact ENNReal.coe_ne_top
      · exact hγ.trans_eq (ENNReal.coe_div C_pos.ne')
    _ = r := (ENNReal.eq_div_iff (by simpa using C_pos.ne') ENNReal.coe_ne_top).mp rfl

Premises used: HDiv.hDiv, Manifold.pathELength, Set.Icc, Iff.mp, OfNat.ofNat, rfl, ENNReal.coe_ne_top, ENNReal.eq_div_iff