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)
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 1 = y

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

Premises used: ContinuousAffineMap.coe_lineMap_eq
-- 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
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
rw :
  ⨅ (γ : Path x y),
      ⨅ (_ :
        ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) I
          (M' := M) 1 (⇑γ : (a : (↑unitInterval : Type)) → M)),
        ∫⁻ (x_2 : (↑unitInterval : Type)),
          enorm (E := TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_2 : M))
            ((mfderiv% (⇑γ : (a : (↑unitInterval : Type)) → M) x_2 :
                  (a : TangentSpace (𝓡∂ 1) x_2) → TangentSpace I ((γ : (a : (↑unitInterval : Type)) → M) x_2))
                1 :
              TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_2 : M)) ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
⊢ riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))

Tactic:
rw [riemannianEDist]

Premises used: Manifold.riemannianEDist
-- 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
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
⊢ ⨅ (γ : Path x y),
      ⨅ (_ :
        ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) I
          (M' := M) 1 (⇑γ : (a : (↑unitInterval : Type)) → M)),
        ∫⁻ (x_2 : (↑unitInterval : Type)),
          enorm (E := TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_2 : M))
            ((mfderiv% (⇑γ : (a : (↑unitInterval : Type)) → M) x_2 :
                  (a : TangentSpace (𝓡∂ 1) x_2) → TangentSpace I ((γ : (a : (↑unitInterval : Type)) → M) x_2))
                1 :
              TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_2 : M)) ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))

Tactic:
biInf_le _ hf

Premises used: Set.Mem, ContMDiff, biInf_le
-- 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
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
⊢ ⨅ (γ : Path x y),
      ⨅ (_ :
        ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) I
          (M' := M) 1 (⇑γ : (a : (↑unitInterval : Type)) → M)),
        ∫⁻ (x_2 : (↑unitInterval : Type)),
          enorm (E := TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_2 : M))
            ((mfderiv% (⇑γ : (a : (↑unitInterval : Type)) → M) x_2 :
                  (a : TangentSpace (𝓡∂ 1) x_2) → TangentSpace I ((γ : (a : (↑unitInterval : Type)) → M) x_2))
                1 :
              TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_2 : M)) ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))

Tactic:
exact biInf_le _ hf

Premises used: biInf_le
-- 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
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
⊢ riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))

Tactic:
have A : riemannianEDist I x y ≤ ∫⁻ x, ‖mfderiv% g x 1‖ₑ := by
    rw [riemannianEDist]; exact biInf_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)
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
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A :
  riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
apply :
  ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M)) =
    pathELength I γ a b
⊢ riemannianEDist I x y ≤ pathELength I γ a b

Tactic:
apply A.trans_eq

Premises used: LE.le.trans_eq
-- 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
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A :
  riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
rw :
  pathELength I (M := M)
      (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I γ a b
⊢ ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M)) =
    pathELength I γ a b

Tactic:
rw [lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc]

Premises used: Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc
-- 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
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A :
  riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
apply :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t),
    Function.comp (β := (↑unitInterval : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯) t =
      (γ ∘ (⇑η : (a : ℝ) → ℝ)) t
⊢ pathELength I (M := M)
      (Function.comp (β := (↑unitInterval : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I (γ ∘ (⇑η : (a : ℝ) → ℝ)) 0 1

Tactic:
apply pathELength_congr (fun t ht ↦ ?_)

Premises used: Manifold.pathELength_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 : ℝ)
hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A :
  riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
simp :
  (g : (a : (↑unitInterval : Type)) → M)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) t ht) =
    γ ((η : (a : ℝ) → ℝ) t)
⊢ Function.comp (β := (↑unitInterval : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯) t =
    (γ ∘ (⇑η : (a : ℝ) → ℝ)) t

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

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 : ℝ)
hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A :
  riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ (g : (a : (↑unitInterval : Type)) → M)
      (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) t ht) =
    γ ((η : (a : ℝ) → ℝ) t)

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)
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
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A :
  riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
⊢ pathELength I (M := M)
      (Function.comp (β := (↑unitInterval : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I (γ ∘ (⇑η : (a : ℝ) → ℝ)) 0 1

Tactic:
have E : pathELength I (g ∘ projIcc 0 1 zero_le_one) 0 1 = pathELength I (γ ∘ η) 0 1 := by
    apply pathELength_congr (fun t ht ↦ ?_)
    simp only [Function.comp_apply, ht, projIcc_of_mem]
    rfl
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E_1 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
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A :
  riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
E :
  pathELength I (M := M)
      (Function.comp (β := (↑unitInterval : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I (γ ∘ (⇑η : (a : ℝ) → ℝ)) 0 1
rw : pathELength I γ ((η : (a : ℝ) → ℝ) 0) ((η : (a : ℝ) → ℝ) 1) = pathELength I γ a b
rw₁ : MDiff[Icc ((η : (a : ℝ) → ℝ) 0) ((η : (a : ℝ) → ℝ) 1)] γ
rw₂ : MonotoneOn (α := ℝ) (β := ℝ) (⇑η : (a : ℝ) → ℝ) (Icc 0 1)
⊢ pathELength I (M := M)
      (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I γ a b

Tactic:
rw [E, pathELength_comp_of_monotoneOn zero_le_one _ η.differentiableOn]

Premises used: zero_le_one, Manifold.pathELength_comp_of_monotoneOn, ContinuousAffineMap.differentiableOn
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E_1 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
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A :
  riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
E :
  pathELength I (M := M)
      (Function.comp (β := (↑unitInterval : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I (γ ∘ (⇑η : (a : ℝ) → ℝ)) 0 1
⊢ pathELength I γ ((η : (a : ℝ) → ℝ) 0) ((η : (a : ℝ) → ℝ) 1) = pathELength I γ a b

Tactic:
simp [η, ContinuousAffineMap.coe_lineMap_eq]

Premises used: ContinuousAffineMap.coe_lineMap_eq