awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ γ 1 = y ∧ ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1) ∧ pathELength I γ 0 1 < r
have hr₁ : ∃ (i : Path x y),
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) I (M' := M)
      1 (⇑i : (a : (↑unitInterval : Type)) → M) ∧
    ∫⁻ (x_1 : (↑unitInterval : Type)),
        enorm (E := TangentSpace I (M := M) ((i : (a : (↑unitInterval : Type)) → M) x_1 : M))
          ((mfderiv% (⇑i : (a : (↑unitInterval : Type)) → M) x_1 :
                (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((i : (a : (↑unitInterval : Type)) → M) x_1))
              1 :
            TangentSpace I (M := M) ((i : (a : (↑unitInterval : Type)) → M) x_1 : M)) <
      r
Tactic: simp only [riemannianEDist, iInf_lt_iff, exists_prop] at hr
Cleared hypotheses: hr
-- 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)
x y : M
r : ℝ≥0∞
hr :
  ∃ (i : Path x y),
    ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) I (M' :=
        M) 1 (⇑i : (a : (↑unitInterval : Type)) → M) ∧
      ∫⁻ (x_1 : (↑unitInterval : Type)),
          enorm (E := TangentSpace I (M := M) ((i : (a : (↑unitInterval : Type)) → M) x_1 : M))
            ((mfderiv% (⇑i : (a : (↑unitInterval : Type)) → M) x_1 :
                  (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((i : (a : (↑unitInterval : Type)) → M) x_1))
                1 :
              TangentSpace I (M := M) ((i : (a : (↑unitInterval : Type)) → M) x_1 : M)) <
        r
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ γ 1 = y ∧ ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1) ∧ pathELength I γ 0 1 < r
have rcases : ∀ (γ : Path x y)
  (γ_smooth :
    ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) I (M' :=
      M) 1 (⇑γ : (a : (↑unitInterval : Type)) → M))
  (hγ :
    ∫⁻ (x_1 : (↑unitInterval : Type)),
        enorm (E := TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_1 : M))
          ((mfderiv% (⇑γ : (a : (↑unitInterval : Type)) → M) x_1 :
                (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((γ : (a : (↑unitInterval : Type)) → M) x_1))
              1 :
            TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_1 : M)) <
      r),
  ∃ (γ : ℝ → M), γ 0 = x ∧ γ 1 = y ∧ ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1) ∧ pathELength I γ 0 1 < r
Tactic: rcases hr with ⟨γ, γ_smooth, hγ⟩
Cleared hypotheses: hr
-- 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)
x y : M
r : ℝ≥0∞
γ : Path x y
γ_smooth :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) I (M' := M)
    1 (⇑γ : (a : (↑unitInterval : Type)) → M)
hγ :
  ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑γ : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((γ : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_1 : M)) <
    r
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ γ 1 = y ∧ ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1) ∧ pathELength I γ 0 1 < r
have refine : pathELength I (M := M)
    (Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 sorry)) 0 1 <
  r
Tactic: refine ⟨γ ∘ (projIcc 0 1 zero_le_one), by simp, by simp,
    contMDiffOn_comp_projIcc_iff.2 γ_smooth, ?_⟩
-- 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)
x y : M
r : ℝ≥0∞
γ : Path x y
γ_smooth :
  ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) (M := (↑unitInterval : Type)) I (M' := M)
    1 (⇑γ : (a : (↑unitInterval : Type)) → M)
hγ :
  ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑γ : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((γ : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) x_1 : M)) <
    r
⊢ pathELength I (M := M)
      (Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 <
    r
have rwa : ∫⁻ (t : (↑(Icc 0 1) : Type)),
    enorm (E := TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) t : M))
      ((mfderiv% (⇑γ : (a : (↑unitInterval : Type)) → M) t :
            (a : TangentSpace (𝓡∂ 1) t) → TangentSpace I ((γ : (a : (↑unitInterval : Type)) → M) t))
          1 :
        TangentSpace I (M := M) ((γ : (a : (↑unitInterval : Type)) → M) t : M)) <
  r
Tactic: rwa [← 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have rcases : ∀ (γ : ℝ → M) (hγx : γ 0 = x) (hγy : γ 1 = y) (γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1))
  (hγ : pathELength I γ 0 1 < r),
  ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
Tactic: rcases exists_lt_of_riemannianEDist_lt hr with ⟨γ, hγx, hγy, γ_smooth, hγ⟩
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have rcases : ∀ (a' : ℝ) (haa' : a < a') (ha'b : a' < b),
  ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
Tactic: rcases exists_between hab with ⟨a', haa', ha'b⟩
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have rcases : ∀ (b' : ℝ) (ha'b' : a' < b') (hb'b : b' < b),
  ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
Tactic: rcases exists_between ha'b with ⟨b', ha'b', hb'b⟩
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
t : ℝ
ht : t < a'
⊢ η t = 0
have simp : (b' - a')⁻¹ * (t - a') ≤ 0
Tactic: simp only [η, Real.smoothTransition.zero_iff_nonpos]
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
t : ℝ
ht : t < a'
⊢ (b' - a')⁻¹ * (t - a') ≤ 0
have ha : 0 ≤ (b' - a')⁻¹
Tactic: apply mul_nonpos_of_nonneg_of_nonpos
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
t : ℝ
ht : t < a'
ha : 0 ≤ (b' - a')⁻¹
⊢ (b' - a')⁻¹ * (t - a') ≤ 0
have hb : t - a' ≤ 0
Tactic: apply mul_nonpos_of_nonneg_of_nonpos
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
t : ℝ
ht : t < a'
⊢ t - a' ≤ 0
have linarith : 0 < t - a' → t - a' + (0 - (t - a')) = 0
Tactic: linarith
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have A : ∀ (t : ℝ) (ht : t < a'), η t = 0
Tactic: have A (t) (ht : t < a') : η t = 0 := by
    simp only [η, Real.smoothTransition.zero_iff_nonpos]
    apply mul_nonpos_of_nonneg_of_nonpos
    · simpa using ha'b'.le
    · linarith
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ (t : ℝ) (ht : t < a'), η t = 0
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have A' : ∀ (t : ℝ) (ht : t < a'), (γ ∘ η) t = x
Tactic: have A' (t) (ht : t < a') : (γ ∘ η) t = x := by simp [A t ht, hγx]
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ (t : ℝ) (ht : t < a'), η t = 0
A' : ∀ (t : ℝ) (ht : t < a'), (γ ∘ η) t = x
t : ℝ
ht : b' < t
⊢ η t = 1
have simp : 1 ≤ (t - a') / (b' - a')
Tactic: simp only [η, Real.smoothTransition.eq_one_iff_one_le, inv_mul_eq_div]
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ (t : ℝ) (ht : t < a'), η t = 0
A' : ∀ (t : ℝ) (ht : t < a'), (γ ∘ η) t = x
t : ℝ
ht : b' < t
⊢ 1 ≤ (t - a') / (b' - a')
have rw : b' - a' ≤ t - a'
Tactic: rw [one_le_div₀]
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ (t : ℝ) (ht : t < a'), η t = 0
A' : ∀ (t : ℝ) (ht : t < a'), (γ ∘ η) t = x
t : ℝ
ht : b' < t
rw : b' - a' ≤ t - a'
⊢ 1 ≤ (t - a') / (b' - a')
have rw₁ : 0 < b' - a'
Tactic: rw [one_le_div₀]
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ (t : ℝ) (ht : t < a'), η t = 0
A' : ∀ (t : ℝ) (ht : t < a'), (γ ∘ η) t = x
t : ℝ
ht : b' < t
⊢ b' - a' ≤ t - a'
have linarith : t - a' < b' - a' → b' - t + (t - a' - (b' - a')) = 0
Tactic: linarith
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ (t : ℝ) (ht : t < a'), η t = 0
A' : ∀ (t : ℝ) (ht : t < a'), (γ ∘ η) t = x
t : ℝ
ht : b' < t
⊢ 0 < b' - a'
have linarith : b' - a' ≤ 0 → a' - b' + (b' - a' - 0) = 0
Tactic: linarith
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ (t : ℝ) (ht : t < a'), η t = 0
A' : ∀ (t : ℝ) (ht : t < a'), (γ ∘ η) t = x
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have B : ∀ (t : ℝ) (ht : b' < t), η t = 1
Tactic: have B (t) (ht : b' < t) : η t = 1 := by
    simp only [η, Real.smoothTransition.eq_one_iff_one_le, inv_mul_eq_div]
    rw [one_le_div₀] <;> linarith
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ (t : ℝ) (ht : t < a'), η t = 0
A' : ∀ (t : ℝ) (ht : t < a'), (γ ∘ η) t = x
B : ∀ (t : ℝ) (ht : b' < t), η t = 1
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have B' : ∀ (t : ℝ) (ht : b' < t), (γ ∘ η) t = y
Tactic: have B' (t) (ht : b' < t) : (γ ∘ η) t = y := by simp [B t ht, hγy]
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ (t : ℝ) (ht : t < a'), η t = 0
A' : ∀ (t : ℝ) (ht : t < a'), (γ ∘ η) t = x
B : ∀ (t : ℝ) (ht : b' < t), η t = 1
B' : ∀ (t : ℝ) (ht : b' < t), (γ ∘ η) t = y
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have refine_1 : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
Tactic: refine ⟨γ ∘ η, A' _ haa', B' _ hb'b, ?_, ?_, ?_, ?_⟩
-- 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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : (t : ℝ) → ℝ := fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ (t : ℝ) (ht : t < a'), η t = 0
A' : ∀ (t : ℝ) (ht : t < a'), (γ ∘ η) t = x
B : ∀ (t : ℝ) (ht : b' < t), η t = 1
B' : ∀ (t : ℝ) (ht : b' < t), (γ ∘ η) t = y
refine_1 : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have refine_2 : pathELength I (γ ∘ η) a b < r
Tactic: refine ⟨γ ∘ η, A' _ haa', B' _ hb'b, ?_, ?_, ?_, ?_⟩