awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
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
have rw : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (f ∘ projIcc 0 1 sorry) (Icc 0 1)
Tactic: rw [← contMDiffOn_comp_projIcc_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
f : (↑unitInterval : Type) → M := fun (t : (↑unitInterval : Type)) ↦ (γ ∘ (⇑η : (a : ℝ) → ℝ)) (↑t : ℝ)
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I 1 (f ∘ projIcc 0 1 ⋯) (Icc 0 1)
have apply : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t), (f ∘ projIcc 0 1 sorry) t = (γ ∘ (⇑η : (a : ℝ) → ℝ)) t
Tactic: apply hη.congr (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
f : (↑unitInterval : Type) → M := fun (t : (↑unitInterval : Type)) ↦ (γ ∘ (⇑η : (a : ℝ) → ℝ)) (↑t : ℝ)
⊢ riemannianEDist I x y ≤ pathELength I γ a b
have hf : 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
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
⊢ Path x y
have refine_1 : { toFun := f, continuous_toFun := sorry : C((↑unitInterval : Type), M) }.toFun 0 = x
Tactic: refine ⟨⟨f, hf.continuous⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
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
⊢ Path x y
have refine_2 : { toFun := f, continuous_toFun := sorry : C((↑unitInterval : Type), M) }.toFun 1 = y
Tactic: refine ⟨⟨f, hf.continuous⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
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))
have 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))
Tactic: rw [riemannianEDist]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
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 ≤ pathELength I γ a b
have 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))
Tactic: have A : riemannianEDist I x y ≤ ∫⁻ x, ‖mfderiv% g x 1‖ₑ := by
    rw [riemannianEDist]; exact biInf_le _ hf
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
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))
⊢ riemannianEDist I x y ≤ pathELength I γ a b
have 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
Tactic: apply A.trans_eq
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
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))
⊢ ∫⁻ (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
have rw : pathELength I (M := M)
    (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 sorry)) 0 1 =
  pathELength I γ a b
Tactic: rw [lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
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
have apply : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t),
  Function.comp (β := (↑unitInterval : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 sorry) t =
    (γ ∘ (⇑η : (a : ℝ) → ℝ)) t
Tactic: apply pathELength_congr (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
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
⊢ Function.comp (β := (↑unitInterval : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯) t =
    (γ ∘ (⇑η : (a : ℝ) → ℝ)) t
have simp : (g : (a : (↑unitInterval : Type)) → M) (Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Icc 0 1) x) t ht) =
  γ ((η : (a : ℝ) → ℝ) t)
Tactic: simp only [Function.comp_apply, ht, projIcc_of_mem]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
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 (β := (↑(Icc 0 1) : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I γ a b
have E₁ : pathELength I (M := M)
    (Function.comp (β := (↑unitInterval : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 sorry)) 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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
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 (M := M)
      (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I γ a b
have rw : pathELength I γ ((η : (a : ℝ) → ℝ) 0) ((η : (a : ℝ) → ℝ) 1) = pathELength I γ a b
Tactic: rw [E, pathELength_comp_of_monotoneOn zero_le_one _ η.differentiableOn]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
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
⊢ pathELength I (M := M)
      (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I γ a b
have rw₁ : MDiff[Icc ((η : (a : ℝ) → ℝ) 0) ((η : (a : ℝ) → ℝ) 1)] γ
Tactic: rw [E, pathELength_comp_of_monotoneOn zero_le_one _ η.differentiableOn]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.PathELength (goal)
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)] γ
⊢ pathELength I (M := M)
      (Function.comp (β := (↑(Icc 0 1) : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I γ a b
have rw₂ : MonotoneOn (α := ℝ) (β := ℝ) (⇑η : (a : ℝ) → ℝ) (Icc 0 1)
Tactic: rw [E, pathELength_comp_of_monotoneOn zero_le_one _ η.differentiableOn]