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 : 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
⊢ 0 ≤ derivWithin f (Icc a b) t

Tactic:
have : 0 ≤ derivWithin f (Icc a b) t := hf.derivWithin_nonneg
-- 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 : 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_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 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:
simp only [map_smul, enorm_smul, ← Real.enorm_of_nonneg this, f_im]

Premises used: enorm_smul, 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)
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)
inr : ∀ (h : a < b), pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a)
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a)

Tactic:
rcases h.eq_or_lt with rfl | h

Premises used: LE.le.eq_or_lt, 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 : ℝ
γ : ℝ → M
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
f : ℝ → ℝ
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:
simp
-- 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 '' 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
-- 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)
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))
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a)

Tactic:
simp only [pathELength_eq_lintegral_mfderivWithin_Icc, ← f_im]

Premises used: Manifold.pathELength_eq_lintegral_mfderivWithin_Icc
-- 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)
⊢ ∀ (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
-- 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
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)))
⊢ ∫⁻ (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:
rw [lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn measurableSet_Icc B hf]

Premises used: MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn, measurableSet_Icc
-- 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
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)))
⊢ ∫⁻ (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:
apply setLIntegral_congr_fun measurableSet_Icc (fun t ht ↦ ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun, measurableSet_Icc
-- 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
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))
⊢ 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:
rw [← f_im] at hγ ⊢
-- 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[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
hxs : UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc a b) 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))

Tactic:
apply mfderivWithin_comp

Premises used: mfderivWithin_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)
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[f '' Icc a b] γ (f t)

Tactic:
apply hγ _ (mem_image_of_mem _ ht)

Premises used: Set.mem_image_of_mem
-- 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[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
hf₁ : DifferentiableWithinAt ℝ f (Icc a b) t
⊢ MDiffAt[Icc a b] f t

Tactic:
rw [mdifferentiableWithinAt_iff_differentiableWithinAt]

Premises used: mdifferentiableWithinAt_iff_differentiableWithinAt
-- 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[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
⊢ DifferentiableWithinAt ℝ f (Icc a b) t

Tactic:
h'f _ 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)
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
⊢ DifferentiableWithinAt ℝ f (Icc a b) t

Tactic:
exact h'f _ 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)
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
⊢ Icc a b ⊆ f ⁻¹' f '' Icc a b

Tactic:
subset_preimage_image _ _

Premises used: Set.subset_preimage_image
-- 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[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
⊢ Icc a b ⊆ f ⁻¹' f '' Icc a b

Tactic:
exact subset_preimage_image _ _

Premises used: Set.subset_preimage_image
-- 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[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
hxs : UniqueDiffWithinAt ℝ (Icc a b) t
⊢ UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc a b) t

Tactic:
rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]

Premises used: uniqueMDiffWithinAt_iff_uniqueDiffWithinAt
-- 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[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
⊢ UniqueDiffWithinAt ℝ (Icc a b) t

Tactic:
uniqueDiffOn_Icc h _ ht

Premises used: uniqueDiffOn_Icc
-- 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[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
⊢ UniqueDiffWithinAt ℝ (Icc a b) t

Tactic:
exact uniqueDiffOn_Icc h _ ht

Premises used: uniqueDiffOn_Icc
-- 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
⊢ 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
-- 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))
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)))
⊢ 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:
rw [this]