awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
h : Fact (a < b)
γ : (↑(Icc a b) : Type) → M
this :
  MeasurePreserving (α := { x : ℝ // x ∈ Icc a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc a b)) volume
    (Measure.restrict volume (Icc a b))
⊢ ∫⁻ (t : (↑(Icc a b) : Type)),
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑t : ℝ) :
              (a_1 : TangentSpace 𝓘(ℝ, ℝ) (↑t : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ)))
            1 :
          TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ))) =
    ∫⁻ (t : ℝ) in Icc a b,
      enorm (E := TangentSpace I ((γ ∘ projIcc a b ⋯) t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) t :
              (a_1 : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ projIcc a b ⋯) t))
            1 :
          TangentSpace I ((γ ∘ projIcc a b ⋯) t))
have rw : ∫⁻ (t : (↑(Icc a b) : Type)),
    enorm (E := TangentSpace I (γ t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b sorry) (Icc a b) (↑t : ℝ) :
            (a_1 : TangentSpace 𝓘(ℝ, ℝ) (↑t : ℝ)) → TangentSpace I ((γ ∘ projIcc a b sorry) (↑t : ℝ)))
          1 :
        TangentSpace I ((γ ∘ projIcc a b sorry) (↑t : ℝ))) =
  ∫⁻ (a_1 : { x : ℝ // x ∈ Icc a b }),
    enorm (E := TangentSpace I ((γ ∘ projIcc a b sorry) (↑a_1 : ℝ)))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b sorry) (Icc a b) (↑a_1 : ℝ) :
            (a_2 : TangentSpace 𝓘(ℝ, ℝ) (↑a_1 : ℝ)) → TangentSpace I ((γ ∘ projIcc a b sorry) (↑a_1 : ℝ)))
          1 :
        TangentSpace I ((γ ∘ projIcc a b sorry) (↑a_1 : ℝ)))
Tactic: rw [← MeasurePreserving.lintegral_comp_emb this
    (MeasurableEmbedding.subtype_coe measurableSet_Icc)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
h : Fact (a < b)
γ : (↑(Icc a b) : Type) → M
this :
  MeasurePreserving (α := { x : ℝ // x ∈ Icc a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc a b)) volume
    (Measure.restrict volume (Icc a b))
⊢ ∫⁻ (t : (↑(Icc a b) : Type)),
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑t : ℝ) :
              (a_1 : TangentSpace 𝓘(ℝ, ℝ) (↑t : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ)))
            1 :
          TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ))) =
    ∫⁻ (a_1 : { x : ℝ // x ∈ Icc a b }),
      enorm (E := TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑a_1 : ℝ) :
              (a_2 : TangentSpace 𝓘(ℝ, ℝ) (↑a_1 : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
            1 :
          TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
have e_f : Eq (α := (↑(Icc a b) : Type) → ℝ≥0∞)
  (fun (t : (↑(Icc a b) : Type)) ↦
    enorm (E := TangentSpace I (γ t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b sorry) (Icc a b) (↑t : ℝ) :
            (a_1 : TangentSpace 𝓘(ℝ, ℝ) (↑t : ℝ)) → TangentSpace I ((γ ∘ projIcc a b sorry) (↑t : ℝ)))
          1 :
        TangentSpace I ((γ ∘ projIcc a b sorry) (↑t : ℝ))))
  fun (a_1 : { x : ℝ // x ∈ Icc a b }) ↦
  enorm (E := TangentSpace I ((γ ∘ projIcc a b sorry) (↑a_1 : ℝ)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b sorry) (Icc a b) (↑a_1 : ℝ) :
          (a_2 : TangentSpace 𝓘(ℝ, ℝ) (↑a_1 : ℝ)) → TangentSpace I ((γ ∘ projIcc a b sorry) (↑a_1 : ℝ)))
        1 :
      TangentSpace I ((γ ∘ projIcc a b sorry) (↑a_1 : ℝ)))
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
h : Fact (a < b)
γ : (↑(Icc a b) : Type) → M
this :
  MeasurePreserving (α := { x : ℝ // x ∈ Icc a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc a b)) volume
    (Measure.restrict volume (Icc a b))
⊢ Eq (α := (↑(Icc a b) : Type) → ℝ≥0∞)
    (fun (t : (↑(Icc a b) : Type)) ↦
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑t : ℝ) :
              (a_1 : TangentSpace 𝓘(ℝ, ℝ) (↑t : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ)))
            1 :
          TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ))))
    fun (a_1 : { x : ℝ // x ∈ Icc a b }) ↦
    enorm (E := TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑a_1 : ℝ) :
            (a_2 : TangentSpace 𝓘(ℝ, ℝ) (↑a_1 : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
          1 :
        TangentSpace I ((γ ∘ projIcc a b ⋯) (↑a_1 : ℝ)))
have e_f : ∀ (t : (↑(Icc a b) : Type)),
  enorm (E := TangentSpace I (γ t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b sorry) (Icc a b) (↑t : ℝ) :
            (a_1 : TangentSpace 𝓘(ℝ, ℝ) (↑t : ℝ)) → TangentSpace I ((γ ∘ projIcc a b sorry) (↑t : ℝ)))
          1 :
        TangentSpace I ((γ ∘ projIcc a b sorry) (↑t : ℝ))) =
    enorm (E := TangentSpace I ((γ ∘ projIcc a b sorry) (↑t : ℝ)))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b sorry) (Icc a b) (↑t : ℝ) :
            (a_1 : TangentSpace 𝓘(ℝ, ℝ) (↑t : ℝ)) → TangentSpace I ((γ ∘ projIcc a b sorry) (↑t : ℝ)))
          1 :
        TangentSpace I ((γ ∘ projIcc a b sorry) (↑t : ℝ)))
Tactic: ext t
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
h : Fact (a < b)
γ : (↑(Icc a b) : Type) → M
this :
  MeasurePreserving (α := { x : ℝ // x ∈ Icc a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Icc a b)) volume
    (Measure.restrict volume (Icc a b))
t : (↑(Icc a b) : Type)
⊢ enorm (E := TangentSpace I (γ t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑t : ℝ) :
            (a_1 : TangentSpace 𝓘(ℝ, ℝ) (↑t : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ)))
          1 :
        TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ))) =
    enorm (E := TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ)))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ projIcc a b ⋯) (Icc a b) (↑t : ℝ) :
            (a_1 : TangentSpace 𝓘(ℝ, ℝ) (↑t : ℝ)) → TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ)))
          1 :
        TangentSpace I ((γ ∘ projIcc a b ⋯) (↑t : ℝ)))
have this₁ : t = projIcc a b sorry (↑t : ℝ)
Tactic: have : t = projIcc a b h.out.le (t : ℝ) := by simp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)
have inl : ∀ (h : a ≤ a) (hf : MonotoneOn f (Icc a a)) (h'f : DifferentiableOn ℝ f (Icc a a)) (hγ : MDiff[Icc (f a) (f a)] γ),
  pathELength I (γ ∘ f) a a = pathELength I γ (f a) (f a)
Tactic: rcases h.eq_or_lt with rfl | h
Cleared hypotheses: b, h, hf, h'f, hγ
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
inl :
  ∀ (h : a ≤ a) (hf : MonotoneOn f (Icc a a)) (h'f : DifferentiableOn ℝ f (Icc a a)) (hγ : MDiff[Icc (f a) (f a)] γ),
    pathELength I (γ ∘ f) a a = pathELength I γ (f a) (f a)
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)
have inr : ∀ (h : a < b), pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)
Tactic: rcases h.eq_or_lt with rfl | h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)
have f_im : f '' Icc a b = Icc (f a) (f b)
Tactic: have f_im : f '' (Icc a b) = Icc (f a) (f b) := h'f.continuousOn.image_Icc_of_monotoneOn h.le hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)
have inr : ∫⁻ (t : ℝ) in Icc a b,
    enorm (E := TangentSpace I ((γ ∘ f) t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ f) t)) 1 :
        TangentSpace I ((γ ∘ f) t)) =
  ∫⁻ (t : ℝ) in f '' Icc a b,
    enorm (E := TangentSpace I (γ t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
        TangentSpace I (γ t))
Tactic: simp only [pathELength_eq_lintegral_mfderivWithin_Icc, ← f_im]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
⊢ ∫⁻ (t : ℝ) in Icc a b,
      enorm (E := TangentSpace I ((γ ∘ f) t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ f) t)) 1 :
          TangentSpace I ((γ ∘ f) t)) =
    ∫⁻ (t : ℝ) in f '' Icc a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
          TangentSpace I (γ t))
have B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
Tactic: have B (t) (ht : t ∈ Icc a b) : HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t :=
    (h'f t ht).hasDerivWithinAt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
⊢ ∫⁻ (t : ℝ) in Icc a b,
      enorm (E := TangentSpace I ((γ ∘ f) t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ f) t)) 1 :
          TangentSpace I ((γ ∘ f) t)) =
    ∫⁻ (t : ℝ) in f '' Icc a b,
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
          TangentSpace I (γ t))
have inr : ∫⁻ (t : ℝ) in Icc a b,
    enorm (E := TangentSpace I ((γ ∘ f) t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ f) t)) 1 :
        TangentSpace I ((γ ∘ f) t)) =
  ∫⁻ (x : ℝ) in Icc a b,
    ENNReal.ofReal (derivWithin f (Icc a b) x) *
      enorm (E := TangentSpace I (γ (f x)))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) (f x) : (a : TangentSpace 𝓘(ℝ, ℝ) (f x)) → TangentSpace I (γ (f x)))
            1 :
          TangentSpace I (γ (f x)))
Tactic: rw [lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn measurableSet_Icc B hf]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
⊢ ∫⁻ (t : ℝ) in Icc a b,
      enorm (E := TangentSpace I ((γ ∘ f) t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ f) t)) 1 :
          TangentSpace I ((γ ∘ f) t)) =
    ∫⁻ (x : ℝ) in Icc a b,
      ENNReal.ofReal (derivWithin f (Icc a b) x) *
        enorm (E := TangentSpace I (γ (f x)))
          ((mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) (f x) :
                (a : TangentSpace 𝓘(ℝ, ℝ) (f x)) → TangentSpace I (γ (f x)))
              1 :
            TangentSpace I (γ (f x)))
have apply : ∀ (t : ℝ) (ht : t ∈ Icc a b),
  enorm (E := TangentSpace I ((γ ∘ f) t))
      ((mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I ((γ ∘ f) t)) 1 :
        TangentSpace I ((γ ∘ f) t)) =
    ENNReal.ofReal (derivWithin f (Icc a b) t) *
      enorm (E := TangentSpace I (γ (f t)))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) (f t) : (a : TangentSpace 𝓘(ℝ, ℝ) (f t)) → TangentSpace I (γ (f t)))
            1 :
          TangentSpace I (γ (f t)))
Tactic: apply setLIntegral_congr_fun measurableSet_Icc (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f a) (f b)] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I ((γ ∘ f) t)) (mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t)
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(ℝ, ℝ) (f t)) (mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f a) (f b)) (f t))
      (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t))
have rw : ∀ (hγ : MDiff[f '' Icc a b] γ) (h : a < b) (f_im : f '' Icc a b = Icc (f a) (f b))
  (B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t) (t : ℝ)
  (ht : t ∈ Icc a b),
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I ((γ ∘ f) t)) (mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t)
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(ℝ, ℝ) (f t)) (mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) (f t))
      (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t))
Tactic: rw [← f_im] at hγ ⊢
Cleared hypotheses: hγ, h, f_im, B, t, ht
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I ((γ ∘ f) t)) (mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t)
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(ℝ, ℝ) (f t)) (mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) (f t))
      (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t))
have hg : MDiffAt[f '' Icc a b] γ (f t)
Tactic: apply mfderivWithin_comp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
hg : MDiffAt[f '' Icc a b] γ (f t)
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I ((γ ∘ f) t)) (mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t)
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(ℝ, ℝ) (f t)) (mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) (f t))
      (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t))
have hf₁ : MDiffAt[Icc a b] f t
Tactic: apply mfderivWithin_comp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
hg : MDiffAt[f '' Icc a b] γ (f t)
hf₁ : MDiffAt[Icc a b] f t
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I ((γ ∘ f) t)) (mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t)
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(ℝ, ℝ) (f t)) (mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) (f t))
      (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t))
have h₁ : Icc a b ⊆ f ⁻¹' f '' Icc a b
Tactic: apply mfderivWithin_comp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
hg : MDiffAt[f '' Icc a b] γ (f t)
hf₁ : MDiffAt[Icc a b] f t
h₁ : Icc a b ⊆ f ⁻¹' f '' Icc a b
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I ((γ ∘ f) t)) (mfderivWithin 𝓘(ℝ, ℝ) I (γ ∘ f) (Icc a b) t)
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(ℝ, ℝ) (f t)) (mfderivWithin 𝓘(ℝ, ℝ) I γ (f '' Icc a b) (f t))
      (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t))
have hxs : UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc a b) t
Tactic: apply mfderivWithin_comp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ MDiffAt[Icc a b] f t
have hf₁ : DifferentiableWithinAt ℝ f (Icc a b) t
Tactic: rw [mdifferentiableWithinAt_iff_differentiableWithinAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (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 : (x : M) → ENorm (TangentSpace I x)
a b : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
h_1 : a ≤ b
hf : MonotoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[f '' Icc a b] γ
h : a < b
f_im : f '' Icc a b = Icc (f a) (f b)
B : ∀ (t : ℝ) (ht : t ∈ Icc a b), HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t
t : ℝ
ht : t ∈ Icc a b
⊢ UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc a b) t
have hxs : UniqueDiffWithinAt ℝ (Icc a b) t
Tactic: rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]