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 : ℝ
γ : ℝ → 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[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))
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 : AntitoneOn 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 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
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 : AntitoneOn 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 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
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 : AntitoneOn 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 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
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 : AntitoneOn 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 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
⊢ 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 : AntitoneOn 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 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
⊢ UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc a b) t
have hxs : UniqueDiffWithinAt ℝ (Icc a b) t
Tactic: rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
-- 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)
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 b) (f a)) (f t))
    (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t))
Tactic: have : (mfderiv[Icc a b] (γ ∘ f) t)
      = (mfderiv[Icc (f b) (f a)] γ (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 : 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
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 b) (f a)) (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 b) (f a)) (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 : 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
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 b) (f a)) (f t))
      (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t))
⊢ enorm (E := TangentSpace I ((γ ∘ f) t))
      ((ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(ℝ, ℝ) (f t)) (mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f b) (f a)) (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 b) (f a)) (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 : 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
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 b) (f a)) (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 : 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
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 b) (f a)) (f t))
      (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) f (Icc a b) t))
⊢ enorm (E := TangentSpace I (γ (f t)))
      ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc (f b) (f a)) (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 : 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
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 b) (f a)) (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 b) (f a)) (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 b) (f a)) (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 : 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
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 b) (f a)) (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 b) (f a)) (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 := by simp [hf.derivWithin_nonpos]
-- 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)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
⊢ ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
have hf : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, ℝ) (M' := ℝ) 1 (⇑η : (a : ℝ) → ℝ) (Icc 0 1)
Tactic: apply hγ.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)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hf : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, ℝ) (M' := ℝ) 1 (⇑η : (a : ℝ) → ℝ) (Icc 0 1)
⊢ ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
have st : Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → ℝ) ⁻¹' Icc a b)
Tactic: apply hγ.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)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
⊢ ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, ℝ) (M' := ℝ) 1 (⇑η : (a : ℝ) → ℝ) (Icc 0 1)
have hf : ContDiffOn ℝ (E := ℝ) (F := ℝ) 1 (⇑η : (a : ℝ) → ℝ) (Icc 0 1)
Tactic: rw [contMDiffOn_iff_contDiffOn]
-- 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)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
⊢ Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → ℝ) ⁻¹' Icc a b)
have st : segment ℝ a b ⊆ Icc a b
Tactic: rw [← image_subset_iff, ContinuousAffineMap.coe_lineMap_eq, ← segment_eq_image_lineMap]
-- 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)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
⊢ riemannianEDist I x y ≤ pathELength I γ a b
have hη : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
Tactic: have hη : CMDiff[Icc 0 1] 1 (γ ∘ η) := by
    apply hγ.comp
    · rw [contMDiffOn_iff_contDiffOn]
      exact η.contDiff.contDiffOn
    · rw [← image_subset_iff, ContinuousAffineMap.coe_lineMap_eq, ← segment_eq_image_lineMap]
      simp [hab]