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
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 (γ ∘ η)
refine_2 : pathELength I (γ ∘ η) a b < r
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have refine_3 : γ ∘ η =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x
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 (γ ∘ η)
refine_2 : pathELength I (γ ∘ η) a b < r
refine_3 : γ ∘ η =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have refine_4 : γ ∘ η =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
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
⊢ ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
have refine_1 : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ η) univ
Tactic: rw [← contMDiffOn_univ]
-- 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
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ η) univ
have refine_1 : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) 1 η univ
Tactic: apply γ_smooth.comp
-- 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 : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) 1 η univ
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ η) univ
have refine_1₁ : univ ⊆ η ⁻¹' Icc 0 1
Tactic: apply γ_smooth.comp
-- 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
⊢ ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) 1 η univ
have refine_1 : ContDiff ℝ 1 η
Tactic: rw [contMDiffOn_univ, contMDiff_iff_contDiff]
-- 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
⊢ pathELength I (γ ∘ η) a b < r
have h : pathELength I (γ ∘ η) a b = pathELength I γ 0 1
Tactic: convert! hγ using 1
-- 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
⊢ pathELength I (γ ∘ η) a b = pathELength I γ 0 1
have h : pathELength I (γ ∘ η) a b = pathELength I γ (η a) (η b)
Tactic: rw [← A a haa', ← B 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
⊢ pathELength I (γ ∘ η) a b = pathELength I γ (η a) (η b)
have h : MonotoneOn η (Icc a b)
Tactic: apply pathELength_comp_of_monotoneOn hab.le
-- 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
h : MonotoneOn η (Icc a b)
⊢ pathELength I (γ ∘ η) a b = pathELength I γ (η a) (η b)
have h₁ : DifferentiableOn ℝ η (Icc a b)
Tactic: apply pathELength_comp_of_monotoneOn hab.le
-- 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
h : MonotoneOn η (Icc a b)
h₁ : DifferentiableOn ℝ η (Icc a b)
⊢ pathELength I (γ ∘ η) a b = pathELength I γ (η a) (η b)
have h₂ : MDiff[Icc (η a) (η b)] γ
Tactic: apply pathELength_comp_of_monotoneOn hab.le
-- 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
⊢ MonotoneOn η (Icc a b)
have h : Monotone η
Tactic: apply Monotone.monotoneOn
-- 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
⊢ Monotone η
have h : Monotone (β := ℝ) fun (t : ℝ) ↦ (b' - a')⁻¹ * (t - a')
Tactic: apply Real.smoothTransition.monotone.comp
-- 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
t u : ℝ
htu : t ≤ u
⊢ (b' - a')⁻¹ * (t - a') ≤ (b' - a')⁻¹ * (u - a')
have h : 0 ≤ (b' - a')⁻¹
Tactic: gcongr
-- 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
⊢ DifferentiableOn ℝ (F := ℝ) (fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition) (Icc a b)
have apply : ContDiff ℝ (F := ℝ) 1 fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
Tactic: apply (ContDiff.contDiffOn _).differentiableOn one_ne_zero
-- 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
⊢ MDiff[Icc (η a) (η b)] γ
have h : MDiff[Icc 0 1] γ
Tactic: rw [A a haa', B 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
⊢ γ ∘ η =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x_1 : ℝ |
      x_1 ∈ Iio a' →
        Membership.mem (γ := Set ℝ) {x_2 : ℝ | (fun (x_3 : ℝ) ↦ (γ ∘ η) x_3 = (fun (x_4 : ℝ) ↦ x) x_3) x_2} x_1}
    a
Tactic: filter_upwards [Iio_mem_nhds haa'] with t ht using A' 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
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
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ |
        x_1 ∈ Iio a' →
          Membership.mem (γ := Set ℝ) {x_2 : ℝ | (fun (x_3 : ℝ) ↦ (γ ∘ η) x_3 = (fun (x_4 : ℝ) ↦ x) x_3) x_2} x_1}
      a
⊢ γ ∘ η =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x
have h₁ : ∀ a ∈ Iio a', (γ ∘ η) a = x
Tactic: filter_upwards [Iio_mem_nhds haa'] with t ht using A' 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
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
⊢ γ ∘ η =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ | x ∈ Ioi b' → Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ (γ ∘ η) x = (fun (x : ℝ) ↦ y) x) x} x} a
Tactic: filter_upwards [Ioi_mem_nhds hb'b] with t ht using B' 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
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
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ | x ∈ Ioi b' → Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ (γ ∘ η) x = (fun (x : ℝ) ↦ y) x) x} x} a
⊢ γ ∘ η =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
have h₁ : ∀ a ∈ Ioi b', (γ ∘ η) a = y
Tactic: filter_upwards [Ioi_mem_nhds hb'b] with t ht using B' 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 : M
⊢ riemannianEDist I x x = 0
have apply : riemannianEDist I x x ≤ ⊥
Tactic: apply le_antisymm _ bot_le
-- 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
⊢ riemannianEDist I x y = riemannianEDist I y x
have suffices : ∀ (x y : M), riemannianEDist I y x ≤ riemannianEDist I x y
Tactic: suffices H : ∀ x y, riemannianEDist I y x ≤ riemannianEDist I x y from le_antisymm (H y x) (H x 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_1 y_1 x y : M
⊢ riemannianEDist I y x ≤ riemannianEDist I x y
have apply : ∀ (r : ℝ≥0∞) (hr : riemannianEDist I x y < r), riemannianEDist I y x < r
Tactic: apply le_of_forall_gt (fun r 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)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
⊢ riemannianEDist I y x < r
have rcases : ∀ (γ : ℝ → M) (γ0 : γ 0 = x) (γ1 : γ 1 = y) (γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ) (hγ : pathELength I γ 0 1 < r),
  riemannianEDist I y x < r
Tactic: rcases exists_lt_locally_constant_of_riemannianEDist_lt hr zero_lt_one
    with ⟨γ, γ0, γ1, γ_smooth, hγ, -⟩