awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x x_1 v w : F
⊢ Eq (α := ℝ)
    ((((((↑(trivializationAt (F →L[ℝ] F →L[ℝ] ℝ)
                          (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) x) :
                      (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) fun (x : F) ↦
                          TangentSpace 𝓘(ℝ, F) x →L[ℝ] TangentSpace 𝓘(ℝ, F) x →L[ℝ] ℝ) →
                        F × (F →L[ℝ] F →L[ℝ] ℝ))
                    ⟨x_1, innerSL ℝ⟩).2 :
                (a : F) → F →L[ℝ] ℝ)
              v :
            F →L[ℝ] ℝ) :
          (a : F) → ℝ)
        w :
      ℝ)
    ((((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) v : F →L[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)

Tactic:
simp [hom_trivializationAt_apply, ContinuousLinearMap.inCoordinates, TangentSpace]

Premises used: ContinuousLinearMap.inCoordinates, TangentSpace, hom_trivializationAt_apply
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
v : TangentSpace 𝓘(ℝ, F) x
rw : √⟪v, v⟫ = ‖v‖
rw₁ rw₂ : √⟪v, v⟫ = √⟪v, v⟫
⊢ ‖v‖ = ‖v‖

Tactic:
rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner]

Premises used: norm_eq_sqrt_real_inner
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
v : TangentSpace 𝓘(ℝ, F) x
⊢ ‖v‖₊ = ‖v‖₊

Tactic:
simp [nnnorm, norm_tangentSpace_vectorSpace]

Premises used: NNNorm.nnnorm, norm_tangentSpace_vectorSpace
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
x : F
v : TangentSpace 𝓘(ℝ, F) x
⊢ ‖v‖ₑ = ‖v‖ₑ

Tactic:
simp [enorm, nnnorm_tangentSpace_vectorSpace]

Premises used: ENorm.enorm, nnnorm_tangentSpace_vectorSpace
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
⊢ edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ

Tactic:
simp [edist_comm x y, edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub, PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
⊢ edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ

Tactic:
have : edist x y = ∫⁻ t in Icc (0 : ℝ) 1, ‖y - x‖ₑ := by
    simp [edist_comm x y, edist_eq_enorm_sub]
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
rw :
  ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := E)
        ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) t : (a : ℝ) → E) 1 : E) =
    ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
⊢ ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := E)
        ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) t : (a : ℝ) → E) 1 : E) =
    edist x y

Tactic:
rw [this]
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
apply :
  ∀ (z : ℝ) (hz : Membership.mem (γ := Set ℝ) (Icc 0 1) z),
    enorm (E := E)
        ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z : (a : ℝ) → E) 1 : E) =
      ‖y - x‖ₑ
⊢ ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := E)
        ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) t : (a : ℝ) → E) 1 : E) =
    ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ

Tactic:
apply setLIntegral_congr_fun measurableSet_Icc (fun z hz ↦ ?_)

Premises used: MeasureTheory.setLIntegral_congr_fun, measurableSet_Icc
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
z : ℝ
hz : Membership.mem (γ := Set ℝ) (Icc 0 1) z
⊢ y - x = (fderiv ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) z : (a : ℝ) → E) 1

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
z : ℝ
hz : Membership.mem (γ := Set ℝ) (Icc 0 1) z
rw :
  enorm (E := E) ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z : (a : ℝ) → E) 1 : E) =
    enorm (E := E) ((fderiv ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) z : (a : ℝ) → E) 1 : E)
⊢ enorm (E := E) ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z : (a : ℝ) → E) 1 : E) =
    ‖y - x‖ₑ

Tactic:
rw [show y - x = fderiv ℝ (ContinuousAffineMap.lineMap (R := ℝ) x y) z 1 by simp]
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
z : ℝ
hz : Membership.mem (γ := Set ℝ) (Icc 0 1) z
e_a :
  Eq (α := ℝ →L[ℝ] E) (fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z)
    (fderiv ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) z)
⊢ enorm (E := E) ((fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z : (a : ℝ) → E) 1 : E) =
    enorm (E := E) ((fderiv ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) z : (a : ℝ) → E) 1 : E)

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
z : ℝ
hz : Membership.mem (γ := Set ℝ) (Icc 0 1) z
⊢ Eq (α := ℝ →L[ℝ] E) (fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z)
    (fderiv ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) z)

Tactic:
fderivWithin_eq_fderiv (uniqueDiffOn_Icc zero_lt_one _ hz)
    (ContinuousAffineMap.differentiableAt _)

Premises used: uniqueDiffOn_Icc, fderivWithin_eq_fderiv, zero_lt_one, ContinuousAffineMap.differentiableAt
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
this : edist x y = ∫⁻ (t : ℝ) in Icc 0 1, ‖y - x‖ₑ
z : ℝ
hz : Membership.mem (γ := Set ℝ) (Icc 0 1) z
⊢ Eq (α := ℝ →L[ℝ] E) (fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) (Icc 0 1) z)
    (fderiv ℝ (⇑(ContinuousAffineMap.lineMap x y) : (a : ℝ) → E) z)

Tactic:
exact fderivWithin_eq_fderiv (uniqueDiffOn_Icc zero_lt_one _ hz)
    (ContinuousAffineMap.differentiableAt _)

Premises used: uniqueDiffOn_Icc, fderivWithin_eq_fderiv, zero_lt_one, ContinuousAffineMap.differentiableAt
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
⊢ IsRiemannianManifold 𝓘(ℝ, F) F

Tactic:
⟨fun x y ↦ le_antisymm ?_ ?_⟩

Premises used: IsRiemannianManifold.mk, le_antisymm
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
refine_1 : ∀ (x y : F), edist x y ≤ riemannianEDist 𝓘(ℝ, F) x y
refine_2 : ∀ (x y : F), riemannianEDist 𝓘(ℝ, F) x y ≤ edist x y
⊢ IsRiemannianManifold 𝓘(ℝ, F) F

Tactic:
refine ⟨fun x y ↦ le_antisymm ?_ ?_⟩
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
refine_1 :
  ∀ (i : Path x y)
    (i_1 :
      ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) 𝓘(ℝ, F)
        (M' := F) 1 (⇑i : (a : (↑unitInterval : Type)) → F)),
    edist x y ≤
      ∫⁻ (x_1 : (↑unitInterval : Type)),
        enorm (E := TangentSpace 𝓘(ℝ, F) (M := F) ((i : (a : (↑unitInterval : Type)) → F) x_1 : F))
          ((mfderiv% (⇑i : (a : (↑unitInterval : Type)) → F) x_1 :
                (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace 𝓘(ℝ, F) ((i : (a : (↑unitInterval : Type)) → F) x_1))
              1 :
            TangentSpace 𝓘(ℝ, F) (M := F) ((i : (a : (↑unitInterval : Type)) → F) x_1 : F))
⊢ edist x y ≤ riemannianEDist 𝓘(ℝ, F) x y

Tactic:
simp only [riemannianEDist, le_iInf_iff]

Premises used: le_iInf_iff, Manifold.riemannianEDist
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) 𝓘(ℝ, F)
    (M' := F) 1 (⇑γ : (a : (↑unitInterval : Type)) → F)
e : ℝ → F := Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯)
⊢ ContDiffOn ℝ 1 e (Icc 0 1)

Tactic:
have D : ContDiffOn ℝ 1 e (Icc 0 1) :=
      contMDiffOn_iff_contDiffOn.mp (hγ.comp_contMDiffOn contMDiffOn_projIcc)
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) 𝓘(ℝ, F)
    (M' := F) 1 (⇑γ : (a : (↑unitInterval : Type)) → F)
e : ℝ → F := Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯)
D : ContDiffOn ℝ 1 e (Icc 0 1)
refine_1 :
  edist x y ≤
    ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E :=
        TangentSpace 𝓘(ℝ, F) (M := F)
          (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯) t))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, F)
                (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯))
                (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) →
                TangentSpace 𝓘(ℝ, F) (((⇑γ : (a : (↑unitInterval : Type)) → F) ∘ projIcc 0 1 ⋯) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F)
            (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯) t))
⊢ edist x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : (↑unitInterval : Type)) → F) x_1 : F))
        ((mfderiv% (⇑γ : (a : (↑unitInterval : Type)) → F) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace 𝓘(ℝ, F) ((γ : (a : (↑unitInterval : Type)) → F) x_1))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : (↑unitInterval : Type)) → F) x_1 : F))

Tactic:
rw [lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc,
      pathELength_eq_lintegral_mfderivWithin_Icc]

Premises used: Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) 𝓘(ℝ, F)
    (M' := F) 1 (⇑γ : (a : (↑unitInterval : Type)) → F)
e : ℝ → F := Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯)
D : ContDiffOn ℝ 1 e (Icc 0 1)
⊢ x = e 0

Tactic:
simp [e]
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) 𝓘(ℝ, F)
    (M' := F) 1 (⇑γ : (a : (↑unitInterval : Type)) → F)
e : ℝ → F := Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯)
D : ContDiffOn ℝ 1 e (Icc 0 1)
⊢ y = e 1

Tactic:
simp [e]
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) 𝓘(ℝ, F)
    (M' := F) 1 (⇑γ : (a : (↑unitInterval : Type)) → F)
e : ℝ → F := Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯)
D : ContDiffOn ℝ 1 e (Icc 0 1)
rw : ‖e 1 - e 0‖ₑ
| edist x y

Tactic:
rw [edist_comm, edist_eq_enorm_sub, show x = e 0 by simp [e], show y = e 1 by simp [e]]

Premises used: edist_eq_enorm_sub, PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) 𝓘(ℝ, F)
    (M' := F) 1 (⇑γ : (a : (↑unitInterval : Type)) → F)
e : ℝ → F := Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯)
D : ContDiffOn ℝ 1 e (Icc 0 1)
refine_1 :
  ‖e 1 - e 0‖ₑ ≤
    ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := F)
        ((fderivWithin ℝ
                (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯))
                (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) →
                TangentSpace 𝓘(ℝ, F) (((⇑γ : (a : (↑unitInterval : Type)) → F) ∘ projIcc 0 1 ⋯) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F)
            (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯) t))
⊢ edist x y ≤
    ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := F)
        ((fderivWithin ℝ
                (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯))
                (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) →
                TangentSpace 𝓘(ℝ, F) (((⇑γ : (a : (↑unitInterval : Type)) → F) ∘ projIcc 0 1 ⋯) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F)
            (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯) t))

Tactic:
conv_lhs =>
      rw [edist_comm, edist_eq_enorm_sub, show x = e 0 by simp [e], show y = e 1 by simp [e]]

Premises used: edist_eq_enorm_sub, PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) 𝓘(ℝ, F)
    (M' := F) 1 (⇑γ : (a : (↑unitInterval : Type)) → F)
e : ℝ → F := Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯)
D : ContDiffOn ℝ 1 e (Icc 0 1)
⊢ ‖e 1 - e 0‖ₑ ≤
    ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := F)
        ((fderivWithin ℝ
                (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯))
                (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) →
                TangentSpace 𝓘(ℝ, F) (((⇑γ : (a : (↑unitInterval : Type)) → F) ∘ projIcc 0 1 ⋯) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F)
            (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯) t))

Tactic:
(enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc D zero_le_one).trans_eq rfl

Premises used: LE.le.trans_eq, enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc, zero_le_one, rfl
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : Path x y
hγ :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) 𝓘(ℝ, F)
    (M' := F) 1 (⇑γ : (a : (↑unitInterval : Type)) → F)
e : ℝ → F := Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯)
D : ContDiffOn ℝ 1 e (Icc 0 1)
⊢ ‖e 1 - e 0‖ₑ ≤
    ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := F)
        ((fderivWithin ℝ
                (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯))
                (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) →
                TangentSpace 𝓘(ℝ, F) (((⇑γ : (a : (↑unitInterval : Type)) → F) ∘ projIcc 0 1 ⋯) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F)
            (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑γ : (a : (↑unitInterval : Type)) → F) (projIcc 0 1 ⋯) t))

Tactic:
exact (enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc D zero_le_one).trans_eq rfl

Premises used: LE.le.trans_eq, enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc, zero_le_one, rfl
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
⊢ (γ : (a : ℝ) → F) 0 = x

Tactic:
simp [γ, ContinuousAffineMap.coe_lineMap_eq]

Premises used: ContinuousAffineMap.coe_lineMap_eq
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
⊢ (γ : (a : ℝ) → F) 1 = y

Tactic:
simp [γ, ContinuousAffineMap.coe_lineMap_eq]

Premises used: ContinuousAffineMap.coe_lineMap_eq
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
apply : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, F) (M' := F) 1 (⇑γ : (a : ℝ) → F) (Icc 0 1)
⊢ riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1

Tactic:
apply riemannianEDist_le_pathELength ?_ (by simp [γ, ContinuousAffineMap.coe_lineMap_eq])
        (by simp [γ, ContinuousAffineMap.coe_lineMap_eq]) zero_le_one

Premises used: Manifold.riemannianEDist_le_pathELength, zero_le_one
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
rw : ContDiffOn ℝ (E := ℝ) (F := F) 1 (⇑γ : (a : ℝ) → F) (Icc 0 1)
⊢ ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, F) (M' := F) 1 (⇑γ : (a : ℝ) → F) (Icc 0 1)

Tactic:
rw [contMDiffOn_iff_contDiffOn]

Premises used: contMDiffOn_iff_contDiffOn
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
⊢ ContDiffOn ℝ (E := ℝ) (F := F) 1 (⇑γ : (a : ℝ) → F) (Icc 0 1)

Tactic:
γ.contDiff.contDiffOn

Premises used: ContDiff.contDiffOn, ContinuousAffineMap.contDiff
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
⊢ ContDiffOn ℝ (E := ℝ) (F := F) 1 (⇑γ : (a : ℝ) → F) (Icc 0 1)

Tactic:
exact γ.contDiff.contDiffOn

Premises used: ContDiff.contDiffOn, ContinuousAffineMap.contDiff
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
⊢ riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1

Tactic:
have : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) γ 0 1 := by
      apply riemannianEDist_le_pathELength ?_ (by simp [γ, ContinuousAffineMap.coe_lineMap_eq])
        (by simp [γ, ContinuousAffineMap.coe_lineMap_eq]) zero_le_one
      rw [contMDiffOn_iff_contDiffOn]
      exact γ.contDiff.contDiffOn
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1
refine_2 : pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1 = edist x y
⊢ riemannianEDist 𝓘(ℝ, F) x y ≤ edist x y

Tactic:
apply this.trans_eq

Premises used: LE.le.trans_eq