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
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1
refine_2 :
  ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, F) (⇑γ : (a : ℝ) → F) (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, F) ((γ : (a : ℝ) → F) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F)) =
    edist x y
⊢ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1 = edist x y

Tactic:
rw [pathELength_eq_lintegral_mfderivWithin_Icc]

Premises used: Manifold.pathELength_eq_lintegral_mfderivWithin_Icc
-- 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
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1
refine_2 :
  ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := F)
        ((fderivWithin ℝ (⇑γ : (a : ℝ) → F) (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, F) ((γ : (a : ℝ) → F) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F)) =
    edist x y
⊢ ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, F) (⇑γ : (a : ℝ) → F) (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, F) ((γ : (a : ℝ) → F) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F)) =
    edist x y

Tactic:
simp only [mfderivWithin_eq_fderivWithin, enorm_tangentSpace_vectorSpace]

Premises used: mfderivWithin_eq_fderivWithin, enorm_tangentSpace_vectorSpace
-- 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
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1
⊢ ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := F)
        ((fderivWithin ℝ (⇑γ : (a : ℝ) → F) (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, F) ((γ : (a : ℝ) → F) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F)) =
    edist x y

Tactic:
lintegral_fderiv_lineMap_eq_edist

Premises used: lintegral_fderiv_lineMap_eq_edist
-- 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
n : ℕ∞ω
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
F : Type u_4
inst_5 : NormedAddCommGroup F
inst_6 : InnerProductSpace ℝ F
x y : F
γ : ℝ →ᴬ[ℝ] F := ContinuousAffineMap.lineMap x y
this : riemannianEDist 𝓘(ℝ, F) x y ≤ pathELength 𝓘(ℝ, F) (M := F) (⇑γ : (a : ℝ) → F) 0 1
⊢ ∫⁻ (t : ℝ) in Icc 0 1,
      enorm (E := F)
        ((fderivWithin ℝ (⇑γ : (a : ℝ) → F) (Icc 0 1) t :
              (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, F) ((γ : (a : ℝ) → F) t))
            1 :
          TangentSpace 𝓘(ℝ, F) (M := F) ((γ : (a : ℝ) → F) t : F)) =
    edist x y

Tactic:
exact lintegral_fderiv_lineMap_eq_edist

Premises used: lintegral_fderiv_lineMap_eq_edist
-- 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 I y →L[ℝ] E)
            (Trivialization.continuousLinearMapAt ℝ (E := fun (x : M) ↦ TangentSpace I x)
              (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
          C),
    ∃ C > 0,
      ∀ᶠ (y : M) in 𝓝 x,
        norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
            (mfderiv% (↑(extChartAt I x) : M → E) y) <
          C
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        C

Tactic:
rcases eventually_norm_trivializationAt_lt E (fun (x : M) ↦ TangentSpace I x) x
    with ⟨C, C_pos, hC⟩

Premises used: TangentSpace, eventually_norm_trivializationAt_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 I y →L[ℝ] E)
        (Trivialization.continuousLinearMapAt ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → 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 I y →L[ℝ] E)
        (Trivialization.continuousLinearMapAt ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
refine :
  ∀ᶠ (y : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      C
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → 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 I y →L[ℝ] E)
        (Trivialization.continuousLinearMapAt ℝ (E := fun (x : M) ↦ TangentSpace I x)
          (trivializationAt E (fun (x : M) ↦ TangentSpace I x) x) y) <
      C
⊢ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x

Tactic:
have hx : (chartAt H x).source ∈ 𝓝 x := chart_source_mem_nhds H x
-- 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 I y →L[ℝ] E)
        (Trivialization.continuousLinearMapAt ℝ (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 := TangentSpace I y →L[ℝ] E)
          (Trivialization.continuousLinearMapAt ℝ (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 I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      C
⊢ ∀ᶠ (y : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(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 := TangentSpace I y →L[ℝ] E)
        (Trivialization.continuousLinearMapAt ℝ (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 := TangentSpace I y →L[ℝ] E)
      (Trivialization.continuousLinearMapAt ℝ (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
h h₁ h₂ h₃ :
  norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
      (Trivialization.continuousLinearMapAt ℝ (E := TangentSpace I) (trivializationAt E (TangentSpace I) x) y) <
    C
⊢ norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
      (mfderiv% (↑(extChartAt I x) : M → E) y) <
    C

Tactic:
rwa [← TangentBundle.continuousLinearMapAt_trivializationAt h'y]

Premises used: TangentBundle.continuousLinearMapAt_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
rcases :
  ∀ (C : ℝ) (C_pos : C > 0)
    (hC :
      ∀ᶠ (y : M) in 𝓝 x,
        norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
            (mfderiv% (↑(extChartAt I x) : M → E) y) <
          C),
    ∃ C > 0,
      ∀ᶠ (y : M) in 𝓝 x,
        enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
            (mfderiv% (↑(extChartAt I x) : M → E) y) <
          (↑C : ℝ≥0∞)
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)

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

Premises used: eventually_norm_mfderiv_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 : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → 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 : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      C
lift :
  ∀ (C : ℝ≥0) (C_pos : (↑C : ℝ) > 0)
    (hC :
      ∀ᶠ (y : M) in 𝓝 x,
        norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
            (mfderiv% (↑(extChartAt I x) : M → E) y) <
          (↑C : ℝ)),
    ∃ C > 0,
      ∀ᶠ (y : M) in 𝓝 x,
        enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
            (mfderiv% (↑(extChartAt I x) : M → E) y) <
          (↑C : ℝ≥0∞)
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → 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 : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → 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 : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ)
C_pos : 0 < C
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → 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 : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ)
C_pos : 0 < C
refine :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
⊢ ∃ C > 0,
    ∀ᶠ (y : M) in 𝓝 x,
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → 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 : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ)
C_pos : 0 < C
h :
  ∀ (y : M)
    (hy :
      norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ)),
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
⊢ ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → 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 : M) in 𝓝 x,
    norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ)
C_pos : 0 < C
y : M
hy :
  norm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
      (mfderiv% (↑(extChartAt I x) : M → 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 : ℝ) (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),
    ∃ C > 0,
      ∀ᶠ (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 : 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:
rcases eventually_norm_symmL_trivializationAt_lt E (fun (x : M) ↦ TangentSpace I x) x
    with ⟨C, C_pos, hC⟩

Premises used: eventually_norm_symmL_trivializationAt_lt, TangentSpace
-- 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
⊢ ∃ C > 0,
    ∀ᶠ (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:
⟨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 := 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
refine :
  ∀ᶠ (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 : 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:
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 := 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
⊢ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source ∈ 𝓝 x

Tactic:
have hx : (chartAt H x).source ∈ 𝓝 x := chart_source_mem_nhds H x