awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)),
    norm (E :=
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
          ((↑(extChartAt I x) : M → E) y)) <
      C
this : 𝓝 x = 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
⊢ ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)

Tactic:
have : ContinuousAt (extChartAt I x).symm (extChartAt I x x) := continuousAt_extChartAt_symm _
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)),
    norm (E :=
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
          ((↑(extChartAt I x) : M → E) y)) <
      C
this_1 : 𝓝 x = 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
this : ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)
h :
  ∀ (y : E)
    (hy :
      y ∈
        (↑(extChartAt I x).symm : E → M) ⁻¹'
          {x_1 : M |
            norm (E :=
                TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) x_1) →L[ℝ]
                  TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x_1)))
                (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
                  ((↑(extChartAt I x) : M → E) x_1)) <
              C})
    (h'y : y ∈ (extChartAt I x).target),
    norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      C
⊢ ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      C

Tactic:
filter_upwards [nhdsWithin_le_nhds (this.preimage_mem_nhds hC),
    extChartAt_target_mem_nhdsWithin x] with y hy h'y

Premises used: extChartAt_target_mem_nhdsWithin, ContinuousAt.preimage_mem_nhds, nhdsWithin_le_nhds
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)),
    norm (E :=
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
          ((↑(extChartAt I x) : M → E) y)) <
      C
this_1 : 𝓝 x = 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
this : ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)
y : E
hy :
  y ∈
    (↑(extChartAt I x).symm : E → M) ⁻¹'
      {x_1 : M |
        norm (E :=
            TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) x_1) →L[ℝ]
              TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x_1)))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
              ((↑(extChartAt I x) : M → E) x_1)) <
          C}
h'y : y ∈ (extChartAt I x).target
⊢ y = (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)

Tactic:
simp [-extChartAt, h'y]

Premises used: extChartAt
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)),
    norm (E :=
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
          ((↑(extChartAt I x) : M → E) y)) <
      C
this_1 : 𝓝 x = 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
this : ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)
y : E
hy :
  y ∈
    (↑(extChartAt I x).symm : E → M) ⁻¹'
      {x_1 : M |
        norm (E :=
            TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) x_1) →L[ℝ]
              TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x_1)))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
              ((↑(extChartAt I x) : M → E) x_1)) <
          C}
h'y : y ∈ (extChartAt I x).target
⊢ y = (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)

Tactic:
have : y = (extChartAt I x) ((extChartAt I x).symm y) := by simp [-extChartAt, h'y]
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)),
    norm (E :=
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
          ((↑(extChartAt I x) : M → E) y)) <
      C
this_1 : 𝓝 x = 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
this_2 : ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)
y : E
hy :
  norm (E :=
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)) →L[ℝ]
        TangentSpace I
          ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))))
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))) <
    C
h'y : y ∈ (extChartAt I x).target
this : y = (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
⊢ norm (E :=
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)) →L[ℝ]
        TangentSpace I
          ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))))
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))) <
    C

Tactic:
hy
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)),
    norm (E :=
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
          ((↑(extChartAt I x) : M → E) y)) <
      C
this_1 : 𝓝 x = 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))
this_2 : ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)
y : E
hy :
  norm (E :=
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)) →L[ℝ]
        TangentSpace I
          ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))))
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))) <
    C
h'y : y ∈ (extChartAt I x).target
this : y = (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
⊢ norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
    C

Tactic:
convert! hy
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
rcases :
  ∀ (C : ℝ) (C_pos : C > 0)
    (hC :
      ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
        norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
          C),
    ∃ C > 0,
      ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
        enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
          (↑C : ℝ≥0∞)
⊢ ∃ C > 0,
    ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
      enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
          (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
        (↑C : ℝ≥0∞)

Tactic:
rcases eventually_norm_mfderivWithin_symm_extChartAt_lt I x with ⟨C, C_pos, hC⟩

Premises used: eventually_norm_mfderivWithin_symm_extChartAt_lt
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      C
⊢ 0 ≤ C

Tactic:
C_pos.le

Premises used: LT.lt.le
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      C
lift :
  ∀ (C : ℝ≥0) (C_pos : (↑C : ℝ) > 0)
    (hC :
      ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
        norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
          (↑C : ℝ)),
    ∃ C > 0,
      ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
        enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
          (↑C : ℝ≥0∞)
⊢ ∃ C > 0,
    ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
      enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
          (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
        (↑C : ℝ≥0∞)

Tactic:
lift C to ℝ≥0 using C_pos.le

Premises used: LT.lt.le
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : (↑C : ℝ) > 0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ)
⊢ 0 < C

Tactic:
simp only [gt_iff_lt, NNReal.coe_pos] at C_pos

Premises used: gt_iff_lt, NNReal.coe_pos
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ≥0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ)
C_pos : 0 < C
⊢ ∃ C > 0,
    ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
      enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
          (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
        (↑C : ℝ≥0∞)

Tactic:
⟨C, C_pos, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ≥0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ)
C_pos : 0 < C
refine :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ≥0∞)
⊢ ∃ C > 0,
    ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
      enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
          (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
        (↑C : ℝ≥0∞)

Tactic:
refine ⟨C, C_pos, ?_⟩
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ≥0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ)
C_pos : 0 < C
h :
  ∀ (y : E)
    (hy :
      norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
          (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
        (↑C : ℝ)),
    enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ≥0∞)
⊢ ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ≥0∞)

Tactic:
filter_upwards [hC] with y hy
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ≥0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ)
C_pos : 0 < C
y : E
hy :
  norm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
    (↑C : ℝ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact_mod_cast hy
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
rcases :
  ∀ (C : ℝ≥0) (C_pos : C > 0)
    (hC :
      ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
        enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
          (↑C : ℝ≥0∞)),
    ∃ C > 0,
      ∀ᶠ (y : M) in 𝓝 x,
        riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)

Tactic:
rcases eventually_enorm_mfderivWithin_symm_extChartAt_lt I x with ⟨C, C_pos, hC⟩

Premises used: eventually_enorm_mfderivWithin_symm_extChartAt_lt
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ≥0∞)
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)

Tactic:
⟨C, C_pos, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
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 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ≥0∞)
refine :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)

Tactic:
refine ⟨C, C_pos, ?_⟩