awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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))
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)))
⊢ 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:
simp only [Function.comp_apply, ContinuousLinearMap.coe_comp']

Premises used: ContinuousLinearMap.coe_comp', Function.comp_apply
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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))
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)
⊢ (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:
simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]

Premises used: mfderivWithin_eq_fderivWithin, fderivWithin_derivWithin, smul_eq_mul, mul_one
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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))
⊢ 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:
rfl
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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

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
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
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)))
⊢ 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:
rw [this]
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
⊢ 0 ≤ -derivWithin f (Icc a b) t

Tactic:
simp [hf.derivWithin_nonpos]

Premises used: AntitoneOn.derivWithin_nonpos
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
⊢ 0 ≤ -derivWithin f (Icc a b) t

Tactic:
have : 0 ≤ -derivWithin f (Icc a b) t := by simp [hf.derivWithin_nonpos]
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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_2 :
  (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
this : 0 ≤ -derivWithin 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)))
          (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:
simp only [map_smul, enorm_smul, f_im, ← Real.enorm_of_nonneg this, enorm_neg]

Premises used: enorm_smul, enorm_neg, Real.enorm_of_nonneg, map_smul
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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)
st : Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → ℝ) ⁻¹' Icc a b)
⊢ ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)

Tactic:
apply hγ.comp

Premises used: ContMDiffOn.comp
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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 : ContDiffOn ℝ (E := ℝ) (F := ℝ) 1 (⇑η : (a : ℝ) → ℝ) (Icc 0 1)
⊢ ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, ℝ) (M' := ℝ) 1 (⇑η : (a : ℝ) → ℝ) (Icc 0 1)

Tactic:
rw [contMDiffOn_iff_contDiffOn]

Premises used: contMDiffOn_iff_contDiffOn
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
⊢ ContDiffOn ℝ (E := ℝ) (F := ℝ) 1 (⇑η : (a : ℝ) → ℝ) (Icc 0 1)

Tactic:
η.contDiff.contDiffOn

Premises used: ContDiff.contDiffOn, ContinuousAffineMap.contDiff
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
⊢ ContDiffOn ℝ (E := ℝ) (F := ℝ) 1 (⇑η : (a : ℝ) → ℝ) (Icc 0 1)

Tactic:
exact η.contDiff.contDiffOn

Premises used: ContDiff.contDiffOn, ContinuousAffineMap.contDiff
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
st : segment ℝ a b ⊆ Icc a b
⊢ Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → ℝ) ⁻¹' Icc a b)

Tactic:
rw [← image_subset_iff, ContinuousAffineMap.coe_lineMap_eq, ← segment_eq_image_lineMap]

Premises used: ContinuousAffineMap.coe_lineMap_eq, segment_eq_image_lineMap, Set.image_subset_iff
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
⊢ segment ℝ a b ⊆ Icc a b

Tactic:
simp [hab]
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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)

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]
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
hη : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
f : (↑unitInterval : Type) → M := fun (t : (↑unitInterval : Type)) ↦ (γ ∘ (⇑η : (a : ℝ) → ℝ)) (↑t : ℝ)
rw : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (f ∘ projIcc 0 1 ⋯) (Icc 0 1)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I 1 f

Tactic:
rw [← contMDiffOn_comp_projIcc_iff]

Premises used: contMDiffOn_comp_projIcc_iff
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
hη : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
f : (↑unitInterval : Type) → M := fun (t : (↑unitInterval : Type)) ↦ (γ ∘ (⇑η : (a : ℝ) → ℝ)) (↑t : ℝ)
apply : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t), (f ∘ projIcc 0 1 ⋯) t = (γ ∘ (⇑η : (a : ℝ) → ℝ)) t
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I 1 (f ∘ projIcc 0 1 ⋯) (Icc 0 1)

Tactic:
apply hη.congr (fun t ht ↦ ?_)

Premises used: ContMDiffOn.congr
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
hη : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
f : (↑unitInterval : Type) → M := fun (t : (↑unitInterval : Type)) ↦ (γ ∘ (⇑η : (a : ℝ) → ℝ)) (↑t : ℝ)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ (f ∘ projIcc 0 1 ⋯) t = (γ ∘ (⇑η : (a : ℝ) → ℝ)) t

Tactic:
simp only [Function.comp_apply, f, projIcc_of_mem, ht]

Premises used: Set.projIcc_of_mem, Function.comp_apply
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
hη : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
f : (↑unitInterval : Type) → M := fun (t : (↑unitInterval : Type)) ↦ (γ ∘ (⇑η : (a : ℝ) → ℝ)) (↑t : ℝ)
⊢ ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I 1 f

Tactic:
have hf : CMDiff 1 f := by
    rw [← contMDiffOn_comp_projIcc_iff]
    apply hη.congr (fun t ht ↦ ?_)
    simp only [Function.comp_apply, f, projIcc_of_mem, ht]
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
hη : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
f : (↑unitInterval : Type) → M := fun (t : (↑unitInterval : Type)) ↦ (γ ∘ (⇑η : (a : ℝ) → ℝ)) (↑t : ℝ)
hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I 1 f
refine_1 : { toFun := f, continuous_toFun := ⋯ : C((↑unitInterval : Type), M) }.toFun 0 = x
refine_2 : { toFun := f, continuous_toFun := ⋯ : C((↑unitInterval : Type), M) }.toFun 1 = y
⊢ Path x y

Tactic:
refine ⟨⟨f, hf.continuous⟩, ?_, ?_⟩
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
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
hη : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
f : (↑unitInterval : Type) → M := fun (t : (↑unitInterval : Type)) ↦ (γ ∘ (⇑η : (a : ℝ) → ℝ)) (↑t : ℝ)
hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I 1 f
⊢ { toFun := f, continuous_toFun := ⋯ : C((↑unitInterval : Type), M) }.toFun 0 = x

Tactic:
simp [f, η, ContinuousAffineMap.coe_lineMap_eq, ha, hb]

Premises used: ContinuousAffineMap.coe_lineMap_eq