awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ 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)))
have this : 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))
Tactic: have : (mfderiv[Icc a b] (γ ∘ f) t) =
      (mfderiv[Icc (f a) (f b)] γ (f t)) ∘L mfderiv[Icc a b] f t := by
    rw [← f_im] at hγ ⊢
    apply mfderivWithin_comp
    · apply hγ _ (mem_image_of_mem _ ht)
    · rw [mdifferentiableWithinAt_iff_differentiableWithinAt]
      exact h'f _ ht
    · exact subset_preimage_image _ _
    · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
      exact uniqueDiffOn_Icc h _ 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
this :
  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))
⊢ 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)))
have rw : enorm (E := TangentSpace I ((γ ∘ f) t))
    ((ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(ℝ, ℝ) (f t)) (mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f a) (f b)) (f t))
            (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) 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: rw [this]
-- 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
this :
  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))
⊢ enorm (E := TangentSpace I ((γ ∘ f) t))
      ((ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(ℝ, ℝ) (f t)) (mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f a) (f b)) (f t))
              (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) 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)))
have simp : enorm (E := TangentSpace I (γ (f t)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f a) (f b)) (f t) : (a : TangentSpace 𝓘(ℝ, ℝ) (f t)) → TangentSpace I (γ (f t)))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) (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: simp only [Function.comp_apply, ContinuousLinearMap.coe_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[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
this :
  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))
⊢ (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) (f t)) 1 =
    HSMul.hSMul (β := TangentSpace 𝓘(ℝ, ℝ) (f t)) (derivWithin f (Icc a b) t) 1
have simp : Eq (α := TangentSpace 𝓘(ℝ, ℝ) (f t))
  ((fderivWithin ℝ f (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) (f t)) 1)
  ((fderivWithin ℝ f (Icc a b) t : (a : ℝ) → ℝ) 1)
Tactic: simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]
-- 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)
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
this :
  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))
⊢ enorm (E := TangentSpace I (γ (f t)))
      ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f a) (f b)) (f t) : (a : TangentSpace 𝓘(ℝ, ℝ) (f t)) → TangentSpace I (γ (f t)))
          ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) (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)))
have this₁ : (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) (f t)) 1 =
  HSMul.hSMul (β := TangentSpace 𝓘(ℝ, ℝ) (f t)) (derivWithin f (Icc a b) t) 1
Tactic: have : mfderiv[Icc a b] f t 1 = derivWithin f (Icc a b) t • (1 : TangentSpace 𝓘(ℝ) (f t)) := by
    simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]
    rfl
-- 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
this_1 :
  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))
this :
  (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) (f t)) 1 =
    HSMul.hSMul (β := TangentSpace 𝓘(ℝ, ℝ) (f t)) (derivWithin f (Icc a b) t) 1
⊢ enorm (E := TangentSpace I (γ (f t)))
      ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f a) (f b)) (f t) : (a : TangentSpace 𝓘(ℝ, ℝ) (f t)) → TangentSpace I (γ (f t)))
          ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) (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)))
have rw : enorm (E := TangentSpace I (γ (f t)))
    ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f a) (f b)) (f t) : (a : TangentSpace 𝓘(ℝ, ℝ) (f t)) → TangentSpace I (γ (f t)))
        (HSMul.hSMul (β := TangentSpace 𝓘(ℝ, ℝ) (f t)) (derivWithin f (Icc a b) 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: rw [this]
-- 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)
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
this_1 :
  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))
this :
  (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) (f t)) 1 =
    HSMul.hSMul (β := TangentSpace 𝓘(ℝ, ℝ) (f t)) (derivWithin f (Icc a b) t) 1
⊢ enorm (E := TangentSpace I (γ (f t)))
      ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f a) (f b)) (f t) : (a : TangentSpace 𝓘(ℝ, ℝ) (f t)) → TangentSpace I (γ (f t)))
          (HSMul.hSMul (β := TangentSpace 𝓘(ℝ, ℝ) (f t)) (derivWithin f (Icc a b) 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)))
have this₁ : 0 ≤ derivWithin f (Icc a b) t
Tactic: have : 0 ≤ derivWithin f (Icc a b) t := hf.derivWithin_nonneg
-- 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 : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a)
have inl : ∀ (h : a ≤ a) (hf : AntitoneOn 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 : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
inl :
  ∀ (h : a ≤ a) (hf : AntitoneOn 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 b) (f a)
have inr : ∀ (h : a < b), pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a)
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 : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
h : a < b
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a)
have f_im : f '' Icc a b = Icc (f b) (f a)
Tactic: have f_im : f '' (Icc a b) = Icc (f b) (f a) := h'f.continuousOn.image_Icc_of_antitoneOn 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 : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a)
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 : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
⊢ ∫⁻ (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 : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
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_antitoneOn 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 : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
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 : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
h : a < b
f_im : f '' Icc a b = Icc (f b) (f a)
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 b) (f a)) (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 b) (f a))
  (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