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
⊢ ∀ (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
-- 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
t : ℝ
ht : b' < t
⊢ (γ ∘ η) t = y

Tactic:
simp [B t ht, hγ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 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
⊢ ∀ (t : ℝ) (ht : b' < t), (γ ∘ η) t = y

Tactic:
have B' (t) (ht : b' < t) : (γ ∘ η) t = y := by simp [B t ht, hγ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 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

Tactic:
⟨γ ∘ η, A' _ haa', B' _ hb'b, ?_, ?_, ?_, ?_⟩

Premises used: Function.comp, And.intro, Exists.intro
-- 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
refine_1 : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
refine_2 : pathELength I (γ ∘ η) a b < r
refine_3 : γ ∘ η =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x
refine_4 : γ ∘ η =ᶠ[𝓝 b] fun (x : ℝ) ↦ y
⊢ ∃ (γ : ℝ → M),
    γ a = x ∧
      γ b = y ∧
        ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun (x_1 : ℝ) ↦ x) ∧ γ =ᶠ[𝓝 b] fun (x : ℝ) ↦ y

Tactic:
refine ⟨γ ∘ η, A' _ haa', B' _ hb'b, ?_, ?_, ?_, ?_⟩
-- 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
refine_1 : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ η) univ
⊢ ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)

Tactic:
rw [← contMDiffOn_univ]

Premises used: contMDiffOn_univ
-- 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
refine_1 : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) 1 η univ
refine_1₁ : univ ⊆ η ⁻¹' Icc 0 1
⊢ ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ η) univ

Tactic:
apply γ_smooth.comp

Premises used: ContMDiffOn.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 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 : ContDiff ℝ 1 η
⊢ ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) 1 η univ

Tactic:
rw [contMDiffOn_univ, contMDiff_iff_contDiff]

Premises used: contMDiff_iff_contDiff, contMDiffOn_univ
-- 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
⊢ 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 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 : Membership.mem (γ := Set ℝ) univ t
⊢ t ∈ η ⁻¹' Icc 0 1

Tactic:
⟨Real.smoothTransition.nonneg _, Real.smoothTransition.le_one _⟩

Premises used: Set.Mem, setOf, Real.smoothTransition.le_one, Set.Icc, Set.preimage, And.intro, Real.smoothTransition.nonneg
-- 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 : Membership.mem (γ := Set ℝ) univ t
⊢ t ∈ η ⁻¹' Icc 0 1

Tactic:
exact ⟨Real.smoothTransition.nonneg _, Real.smoothTransition.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 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 γ 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 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 : pathELength I (γ ∘ η) a b = pathELength I γ 0 1
⊢ pathELength I (γ ∘ η) a b < r

Tactic:
convert! hγ using 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 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 : pathELength I (γ ∘ η) a b = pathELength I γ (η a) (η b)
⊢ pathELength I (γ ∘ η) a b = pathELength I γ 0 1

Tactic:
rw [← A a haa', ← B b hb'b]
-- 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 : MonotoneOn η (Icc a b)
h₁ : DifferentiableOn ℝ η (Icc a b)
h₂ : MDiff[Icc (η a) (η b)] γ
⊢ pathELength I (γ ∘ η) a b = pathELength I γ (η a) (η b)

Tactic:
apply pathELength_comp_of_monotoneOn hab.le

Premises used: LT.lt.le, Manifold.pathELength_comp_of_monotoneOn
-- 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 : Monotone η
⊢ MonotoneOn η (Icc a b)

Tactic:
apply Monotone.monotoneOn

Premises used: Monotone.monotoneOn
-- 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 : Monotone (β := ℝ) fun (t : ℝ) ↦ (b' - a')⁻¹ * (t - a')
⊢ Monotone η

Tactic:
apply Real.smoothTransition.monotone.comp

Premises used: Monotone.comp, Real.smoothTransition.monotone
-- 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 u : ℝ
htu : t ≤ u
h : 0 ≤ (b' - a')⁻¹
⊢ (b' - a')⁻¹ * (t - a') ≤ (b' - a')⁻¹ * (u - a')

Tactic:
gcongr
-- 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 : DifferentiableOn ℝ (F := ℝ) (fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition) (Icc a b)
⊢ DifferentiableOn ℝ η (Icc a b)

Tactic:
simp only [η]
-- 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
apply : ContDiff ℝ (F := ℝ) 1 fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
⊢ DifferentiableOn ℝ (F := ℝ) (fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition) (Icc a b)

Tactic:
apply (ContDiff.contDiffOn _).differentiableOn one_ne_zero

Premises used: ContDiff.contDiffOn, ContDiffOn.differentiableOn, one_ne_zero
-- 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
⊢ ContDiff ℝ (F := ℝ) 1 fun (t : ℝ) ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition

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 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 : MDiff[Icc 0 1] γ
⊢ MDiff[Icc (η a) (η b)] γ

Tactic:
rw [A a haa', B b hb'b]
-- 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
⊢ MDiff[Icc 0 1] γ

Tactic:
apply γ_smooth.mdifferentiableOn one_ne_zero

Premises used: 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 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 ∈ Iio a'
⊢ (γ ∘ η) t = x

Tactic:
A' t ht