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
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
h₁ h₂ : ∀ (t : ℝ) (ht : t ∈ Iio a'), (γ ∘ η) t = x
⊢ γ ∘ η =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x

Tactic:
filter_upwards [Iio_mem_nhds haa'] with t ht using A' t ht

Premises used: Iio_mem_nhds
-- 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
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 : ℝ
ht : t ∈ Ioi b'
⊢ (γ ∘ η) t = y

Tactic:
B' t ht
-- 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
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
h₁ h₂ : ∀ (t : ℝ) (ht : t ∈ Ioi b'), (γ ∘ η) t = y
⊢ γ ∘ η =ᶠ[𝓝 b] fun (x : ℝ) ↦ y

Tactic:
filter_upwards [Ioi_mem_nhds hb'b] with t ht using B' t ht

Premises used: Ioi_mem_nhds
-- 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 : M
apply : riemannianEDist I x x ≤ ⊥
⊢ riemannianEDist I x x = 0

Tactic:
apply le_antisymm _ bot_le

Premises used: le_antisymm, bot_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 : M
⊢ pathELength.{u_1, u_2, u_3} I (M := M) (fun (t : ℝ) ↦ x) 0 0 = ⊥

Tactic:
simp
-- 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 : M
⊢ riemannianEDist I x x ≤ ⊥

Tactic:
exact (riemannianEDist_le_pathELength (γ := fun (t : ℝ) ↦ x) (a := 0) (b := 0)
    contMDiffOn_const rfl rfl le_rfl).trans_eq (by simp)

Premises used: le_rfl, LE.le.trans_eq, Manifold.riemannianEDist_le_pathELength, contMDiffOn_const, 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
suffices : ∀ (x y : M), riemannianEDist I y x ≤ riemannianEDist I x y
⊢ riemannianEDist I x y = riemannianEDist I y x

Tactic:
suffices H : ∀ x y, riemannianEDist I y x ≤ riemannianEDist I x y from le_antisymm (H y x) (H x y)
-- 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_1 y_1 x y : M
apply : ∀ (r : ℝ≥0∞) (hr : riemannianEDist I x y < r), riemannianEDist I y x < r
⊢ riemannianEDist I y x ≤ riemannianEDist I x y

Tactic:
apply le_of_forall_gt (fun r hr ↦ ?_)

Premises used: le_of_forall_gt
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
rcases :
  ∀ (γ : ℝ → M) (γ0 : γ 0 = x) (γ1 : γ 1 = y) (γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ) (hγ : pathELength I γ 0 1 < r),
    riemannianEDist I y x < r
⊢ riemannianEDist I y x < r

Tactic:
rcases exists_lt_locally_constant_of_riemannianEDist_lt hr zero_lt_one
    with ⟨γ, γ0, γ1, γ_smooth, hγ, -⟩

Premises used: zero_lt_one, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
apply : ContMDiff 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) 1 η
⊢ ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)

Tactic:
apply γ_smooth.comp ?_

Premises used: ContMDiff.comp
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
simp : ContDiff ℝ 1 η
⊢ ContMDiff 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) 1 η

Tactic:
simp only [contMDiff_iff_contDiff]

Premises used: contMDiff_iff_contDiff
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
⊢ ContDiff ℝ 1 η

Tactic:
fun_prop
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
⊢ ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)

Tactic:
have h_smooth : CMDiff 1 (γ ∘ η) := by
    apply γ_smooth.comp ?_
    simp only [contMDiff_iff_contDiff]
    fun_prop
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
ha : (γ ∘ η) (η 1) = y
hb : (γ ∘ η) (η 0) = x
hab : η 1 ≤ η 0
⊢ riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0)

Tactic:
apply riemannianEDist_le_pathELength h_smooth.contMDiffOn

Premises used: Manifold.riemannianEDist_le_pathELength, ContMDiff.contMDiffOn
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ (γ ∘ η) (η 1) = y

Tactic:
simp [η, γ0, γ1]
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ (γ ∘ η) (η 0) = x

Tactic:
simp [η, γ0, γ1]
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ η 1 ≤ η 0

Tactic:
simp [η, γ0, γ1]
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
⊢ riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0)

Tactic:
have : riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0) := by
    apply riemannianEDist_le_pathELength h_smooth.contMDiffOn <;> simp [η, γ0, γ1]
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0)
rw : ∀ (this : riemannianEDist I y x ≤ pathELength I ((γ ∘ η) ∘ η) 0 1), riemannianEDist I y x < r
hf : AntitoneOn η (Icc 0 1)
h'f : DifferentiableOn ℝ η (Icc 0 1)
hγ₁ : MDiff[Icc (η 1) (η 0)] (γ ∘ η)
⊢ riemannianEDist I y x < r

Tactic:
rw [← pathELength_comp_of_antitoneOn zero_le_one] at this

Premises used: Manifold.pathELength_comp_of_antitoneOn, zero_le_one
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0)
⊢ AntitoneOn η (Icc 0 1)

Tactic:
monotone_id.neg.antitoneOn _

Premises used: Antitone.antitoneOn, monotone_id, Monotone.neg
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0)
⊢ AntitoneOn η (Icc 0 1)

Tactic:
exact monotone_id.neg.antitoneOn _

Premises used: Antitone.antitoneOn, monotone_id, Monotone.neg
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0)
⊢ DifferentiableOn ℝ η (Icc 0 1)

Tactic:
differentiableOn_neg _

Premises used: differentiableOn_neg
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0)
⊢ DifferentiableOn ℝ η (Icc 0 1)

Tactic:
exact differentiableOn_neg _

Premises used: differentiableOn_neg
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0)
⊢ MDiff[Icc (η 1) (η 0)] (γ ∘ η)

Tactic:
h_smooth.contMDiffOn.mdifferentiableOn one_ne_zero

Premises used: ContMDiff.contMDiffOn, one_ne_zero, ContMDiffOn.mdifferentiableOn
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0)
⊢ MDiff[Icc (η 1) (η 0)] (γ ∘ η)

Tactic:
exact h_smooth.contMDiffOn.mdifferentiableOn one_ne_zero

Premises used: ContMDiff.contMDiffOn, one_ne_zero, ContMDiffOn.mdifferentiableOn
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I ((γ ∘ η) ∘ η) 0 1
apply : pathELength I ((γ ∘ η) ∘ η) 0 1 < r
⊢ riemannianEDist I y x < r

Tactic:
apply this.trans_lt

Premises used: LE.le.trans_lt
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I ((γ ∘ η) ∘ η) 0 1
⊢ pathELength I γ 0 1 < r

Tactic:
hγ
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I ((γ ∘ η) ∘ η) 0 1
h : (γ ∘ η) ∘ η = γ
⊢ pathELength I ((γ ∘ η) ∘ η) 0 1 < r

Tactic:
convert! hγ
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I ((γ ∘ η) ∘ η) 0 1
h : ∀ (t : ℝ), ((γ ∘ η) ∘ η) t = γ t
⊢ (γ ∘ η) ∘ η = γ

Tactic:
ext t
-- 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_1 y_1 x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun (t : ℝ) ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I ((γ ∘ η) ∘ η) 0 1
t : ℝ
⊢ ((γ ∘ η) ∘ η) t = γ t

Tactic:
simp [η]
-- 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 z : M
apply : ∀ (r : ℝ≥0∞) (hr : riemannianEDist I x y + riemannianEDist I y z < r), riemannianEDist I x z < r
⊢ riemannianEDist I x z ≤ riemannianEDist I x y + riemannianEDist I y z

Tactic:
apply le_of_forall_gt (fun r hr ↦ ?_)

Premises used: le_of_forall_gt
-- 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 z : M
r : ℝ≥0∞
hr : riemannianEDist I x y + riemannianEDist I y z < r
rcases :
  ∀ (u : ℝ≥0∞) (hu : u > riemannianEDist I x y) (v : ℝ≥0∞) (hv : v > riemannianEDist I y z) (huv : u + v < r),
    riemannianEDist I x z < r
⊢ riemannianEDist I x z < r

Tactic:
rcases ENNReal.exists_add_lt_of_add_lt hr with ⟨u, hu, v, hv, huv⟩

Premises used: ENNReal.exists_add_lt_of_add_lt