awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E_1 H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
f : (↑unitInterval : Type) → M := fun (t : (↑unitInterval : Type)) ↦ (γ ∘ (⇑η : (a : ℝ) → ℝ)) (↑t : ℝ)
hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A :
  riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
E :
  pathELength I (M := M)
      (Function.comp (β := (↑unitInterval : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I (γ ∘ (⇑η : (a : ℝ) → ℝ)) 0 1
⊢ MDiff[Icc ((η : (a : ℝ) → ℝ) 0) ((η : (a : ℝ) → ℝ) 1)] γ

Tactic:
simpa [η, ContinuousAffineMap.coe_lineMap_eq] using hγ.mdifferentiableOn one_ne_zero

Premises used: ContinuousAffineMap.coe_lineMap_eq, one_ne_zero, ContMDiffOn.mdifferentiableOn
-- Module: Mathlib.Geometry.Manifold.Riemannian.PathELength
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E_1 H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : (x : M) → ENorm (TangentSpace I x)
inst_6 : ∀ (x : M), ENormSMulClass.{0, u_1} ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) I 1 (γ ∘ (⇑η : (a : ℝ) → ℝ)) (Icc 0 1)
f : (↑unitInterval : Type) → M := fun (t : (↑unitInterval : Type)) ↦ (γ ∘ (⇑η : (a : ℝ) → ℝ)) (↑t : ℝ)
hf : ContMDiff (E := EuclideanSpace ℝ (Fin 1)) (H := EuclideanHalfSpace 1) (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A :
  riemannianEDist I x y ≤
    ∫⁻ (x_1 : (↑unitInterval : Type)),
      enorm (E := TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
        ((mfderiv% (⇑g : (a : (↑unitInterval : Type)) → M) x_1 :
              (a : TangentSpace (𝓡∂ 1) x_1) → TangentSpace I ((g : (a : (↑unitInterval : Type)) → M) x_1))
            1 :
          TangentSpace I (M := M) ((g : (a : (↑unitInterval : Type)) → M) x_1 : M))
E :
  pathELength I (M := M)
      (Function.comp (β := (↑unitInterval : Type)) (⇑g : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 =
    pathELength I (γ ∘ (⇑η : (a : ℝ) → ℝ)) 0 1
⊢ MonotoneOn (α := ℝ) (β := ℝ) (⇑η : (a : ℝ) → ℝ) (Icc 0 1)

Tactic:
apply (AffineMap.lineMap_mono hab).monotoneOn

Premises used: AffineMap.lineMap_mono, 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)
x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
⊢ ∃ (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

Premises used: Manifold.riemannianEDist, exists_prop, iInf_lt_iff
-- 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)
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
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
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ γ 1 = y ∧ ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1) ∧ pathELength I γ 0 1 < r

Tactic:
rcases hr with ⟨γ, γ_smooth, 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)
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
⊢ Function.comp (α := ℝ) (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯) 0 = x

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)
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
⊢ Function.comp (α := ℝ) (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯) 1 = y

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)
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
refine :
  pathELength I (M := M)
      (Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 <
    r
⊢ ∃ (γ : ℝ → M), γ 0 = x ∧ γ 1 = y ∧ ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1) ∧ pathELength I γ 0 1 < r

Tactic:
refine ⟨γ ∘ (projIcc 0 1 zero_le_one), by simp, by simp,
    contMDiffOn_comp_projIcc_iff.2 γ_smooth, ?_⟩
-- 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)
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
rwa rwa₁ rwa₂ 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
⊢ pathELength I (M := M)
      (Function.comp (β := (↑unitInterval : Type)) (⇑γ : (a : (↑unitInterval : Type)) → M) (projIcc 0 1 ⋯)) 0 1 <
    r

Tactic:
rwa [← lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc]

Premises used: Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc
-- 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
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
⊢ ∃ (γ : ℝ → 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γ⟩

Premises used: Manifold.exists_lt_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 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
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
⊢ ∃ (γ : ℝ → 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⟩

Premises used: exists_between
-- 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
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
⊢ ∃ (γ : ℝ → 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⟩

Premises used: exists_between
-- 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
t : ℝ
ht : t < a'
simp : (b' - a')⁻¹ * (t - a') ≤ 0
⊢ η t = 0

Tactic:
simp only [η, Real.smoothTransition.zero_iff_nonpos]

Premises used: Real.smoothTransition.zero_iff_nonpos
-- 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
t : ℝ
ht : t < a'
ha : 0 ≤ (b' - a')⁻¹
hb : t - a' ≤ 0
⊢ (b' - a')⁻¹ * (t - a') ≤ 0

Tactic:
apply mul_nonpos_of_nonneg_of_nonpos

Premises used: mul_nonpos_of_nonneg_of_nonpos
-- 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
t : ℝ
ht : t < a'
⊢ 0 ≤ (b' - a')⁻¹

Tactic:
simpa using ha'b'.le

Premises used: LT.lt.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 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'
linarith : 0 < t - a' → t - a' + (0 - (t - a')) = 0
⊢ t - a' ≤ 0

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

Tactic:
simp [A t ht, hγx]
-- 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
⊢ ∀ (t : ℝ) (ht : t < a'), (γ ∘ η) t = x

Tactic:
have A' (t) (ht : t < a') : (γ ∘ η) t = x := by simp [A t ht, hγx]
-- 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
simp : 1 ≤ (t - a') / (b' - a')
⊢ η t = 1

Tactic:
simp only [η, Real.smoothTransition.eq_one_iff_one_le, inv_mul_eq_div]

Premises used: Real.smoothTransition.eq_one_iff_one_le, inv_mul_eq_div
-- 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
rw : b' - a' ≤ t - a'
rw₁ : 0 < b' - a'
⊢ 1 ≤ (t - a') / (b' - a')

Tactic:
rw [one_le_div₀]

Premises used: one_le_div₀
-- 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
linarith : t - a' < b' - a' → b' - t + (t - a' - (b' - a')) = 0
⊢ b' - a' ≤ t - a'

Tactic:
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
t : ℝ
ht : b' < t
linarith : b' - a' ≤ 0 → a' - b' + (b' - a' - 0) = 0
⊢ 0 < b' - a'

Tactic:
linarith