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 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
h :
  ∀ (y : M)
    (hy :
      norm (E := E →L[ℝ] TangentSpace I y)
          (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
            (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
        C)
    (h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source),
    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
⊢ ∀ᶠ (y : M) in 𝓝 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

Tactic:
filter_upwards [hC, hx] with y hy 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 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
y : M
hy :
  norm (E := E →L[ℝ] TangentSpace I y)
      (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
        (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
    C
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ norm (E := E →L[ℝ] TangentSpace I y)
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y) :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) <
    C

Tactic:
rw [TangentBundle.symmL_trivializationAt h'y] at hy

Premises used: TangentBundle.symmL_trivializationAt
-- 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 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
y : M
hy :
  norm (E := E →L[ℝ] TangentSpace I y)
      (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
        (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
    C
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
hy₁ :
  norm (E := E →L[ℝ] TangentSpace I y)
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y) :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) <
    C
⊢ y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
rw [TangentBundle.symmL_trivializationAt h'y] at hy

Premises used: TangentBundle.symmL_trivializationAt
-- 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 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
y : M
hy :
  norm (E := E →L[ℝ] TangentSpace I y)
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y) :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) <
    C
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ y ∈ (extChartAt I x).source

Tactic:
simpa using 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 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
y : M
hy :
  norm (E := E →L[ℝ] TangentSpace I y)
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y) :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) <
    C
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y

Tactic:
have A : (extChartAt I x).symm (extChartAt I x y) = y :=
    (extChartAt I x).left_inv (by simpa using 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 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
y : M
hy :
  norm (E := E →L[ℝ] TangentSpace I y)
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y) :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) <
    C
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
A : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y
⊢ norm (E := E →L[ℝ] TangentSpace I y)
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y) :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) 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 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
y : M
hy :
  norm (E := E →L[ℝ] TangentSpace I y)
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y) :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) <
    C
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
A : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y
h :
  (TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
        TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) =
      (E →L[ℝ] TangentSpace I y) →
    TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) = TangentSpace I y →
      Eq.{u_1 + 1} (α :=
        SeminormedAddCommGroup (TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))
        NormedAddCommGroup.toSeminormedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup
h₁ :
  (TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
        TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) =
      (E →L[ℝ] TangentSpace I y) →
    TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) = TangentSpace I y →
      HEq.{u_1 + 1} (α :=
          SeminormedAddCommGroup (TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))
          NormedAddCommGroup.toSeminormedAddCommGroup (β := SeminormedAddCommGroup (TangentSpace I y))
          NormedAddCommGroup.toSeminormedAddCommGroup →
        HEq.{u_1 + 1} (α :=
          NormedSpace ℝ (TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))
          InnerProductSpace.toNormedSpace (β := NormedSpace ℝ (TangentSpace I y)) InnerProductSpace.toNormedSpace
⊢ 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

Tactic:
convert! hy using 3
-- 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 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
y : M
hy :
  norm (E := E →L[ℝ] TangentSpace I y)
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y) :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) <
    C
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
A : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y
e_1 :
  (TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) =
    (E →L[ℝ] TangentSpace I y)
e_4 : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) = TangentSpace I y
⊢ Eq.{u_1 + 1} (α :=
    SeminormedAddCommGroup (TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))
    NormedAddCommGroup.toSeminormedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup

Tactic:
congr
-- 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 𝓝 x,
    norm (E := E →L[ℝ] TangentSpace I y)
        (Trivialization.symmL ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
hx : (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x
y : M
hy :
  norm (E := E →L[ℝ] TangentSpace I y)
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) y) :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
          TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) <
    C
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
A : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y) = y
e_1 :
  (TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y) →L[ℝ]
      TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))) =
    (E →L[ℝ] TangentSpace I y)
e_4 : TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y)) = TangentSpace I y
e_6 :
  HEq.{u_1 + 1} (α :=
    SeminormedAddCommGroup (TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))
    NormedAddCommGroup.toSeminormedAddCommGroup (β := SeminormedAddCommGroup (TangentSpace I y))
    NormedAddCommGroup.toSeminormedAddCommGroup
⊢ HEq.{u_1 + 1} (α := NormedSpace ℝ (TangentSpace I ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) y))))
    InnerProductSpace.toNormedSpace (β := NormedSpace ℝ (TangentSpace I y)) InnerProductSpace.toNormedSpace

Tactic:
congr
-- 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 : M) in 𝓝 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),
    ∃ C > 0,
      ∀ᶠ (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,
      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:
rcases eventually_norm_mfderivWithin_symm_extChartAt_comp_lt I x with ⟨C, C_pos, hC⟩

Premises used: eventually_norm_mfderivWithin_symm_extChartAt_comp_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 : M) in 𝓝 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
⊢ ∃ C > 0,
    ∀ᶠ (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:
⟨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 : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 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
refine :
  ∀ᶠ (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,
      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:
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 : ℝ
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 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
⊢ 𝓝 x = 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))

Tactic:
simp
-- 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 𝓝 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
⊢ 𝓝 x = 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))

Tactic:
have : 𝓝 x = 𝓝 ((extChartAt I x).symm (extChartAt I x x)) := by simp
-- 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 𝓝 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))
⊢ ∀ᶠ (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

Tactic:
rw [this] at hC
-- 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 𝓝 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))
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
⊢ 𝓝 x = 𝓝 ((↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x))

Tactic:
rw [this] at hC