-- 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 : riemannianEDist I x y ≤ pathELength I γ 0 1
⊢ ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 1) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
          TangentSpace I (γ t)) ≤
    ∫⁻ (a : ℝ) in Icc 0 1,
      (↑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) a :
                (a : ℝ) → E)
              1 :
            E)
have apply : ∀ (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)
Tactic: apply setLIntegral_mono' measurableSet_Icc (fun t ht ↦ ?_)