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 : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this_1 : (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞))
h'y : riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this : edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c / (↑C : ℝ≥0∞)
⊢ (↑C : ℝ≥0∞) ≠ 0 ∨ edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) ≠ ∞

Tactic:
exact Or.inl (mod_cast C_pos.ne')

Premises used: Or.inl
-- 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 : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this_1 : (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞))
h'y : riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this : edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c / (↑C : ℝ≥0∞)
⊢ (↑C : ℝ≥0∞) ≠ ∞ ∨ edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) ≠ 0

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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
rcases :
  ∀ (C : ℝ≥0) (C_pos : C > 0)
    (hC :
      ∀ᶠ (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 | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s
⊢ ∃ c > 0, {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s

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

Premises used: eventually_enorm_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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
⊢ s ∩
        {x_1 : M |
          (fun (y : M) ↦
              enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
                  (mfderiv% (↑(extChartAt I x) : M → E) y) <
                (↑C : ℝ≥0∞))
            x_1} ∩
      (extChartAt I x).source ∈
    𝓝 x

Tactic:
have := Filter.inter_mem (Filter.inter_mem hs hC) (extChartAt_source_mem_nhds (I := I) 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
this :
  s ∩
        {x_1 : M |
          (fun (y : M) ↦
              enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
                  (mfderiv% (↑(extChartAt I x) : M → E) y) <
                (↑C : ℝ≥0∞))
            x_1} ∩
      (extChartAt I x).source ∈
    𝓝 x
rcases :
  ∀ (u : Set M) (u_mem : u ∈ 𝓝 x) (u_closed : IsClosed[inst_3] u)
    (hu :
      u ⊆
        s ∩
            {x_1 : M |
              (fun (y : M) ↦
                  enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
                      (mfderiv% (↑(extChartAt I x) : M → E) y) <
                    (↑C : ℝ≥0∞))
                x_1} ∩
          (extChartAt I x).source),
    ∃ u ∈ 𝓝 x,
      IsClosed[inst_3] u ∧
        u ⊆ s ∧
          u ⊆
              {y : M |
                enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
                    (mfderiv% (↑(extChartAt I x) : M → E) y) <
                  (↑C : ℝ≥0∞)} ∧
            u ⊆ (extChartAt I x).source
⊢ ∃ u ∈ 𝓝 x,
    IsClosed[inst_3] u ∧
      u ⊆ s ∧
        u ⊆
            {y : M |
              enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
                  (mfderiv% (↑(extChartAt I x) : M → E) y) <
                (↑C : ℝ≥0∞)} ∧
          u ⊆ (extChartAt I x).source

Tactic:
rcases exists_mem_nhds_isClosed_subset this with ⟨u, u_mem, u_closed, hu⟩

Premises used: exists_mem_nhds_isClosed_subset
-- 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
this :
  s ∩
        {x_1 : M |
          (fun (y : M) ↦
              enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
                  (mfderiv% (↑(extChartAt I x) : M → E) y) <
                (↑C : ℝ≥0∞))
            x_1} ∩
      (extChartAt I x).source ∈
    𝓝 x
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
hu :
  u ⊆
    s ∩
        {x_1 : M |
          (fun (y : M) ↦
              enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
                  (mfderiv% (↑(extChartAt I x) : M → E) y) <
                (↑C : ℝ≥0∞))
            x_1} ∩
      (extChartAt I x).source
⊢ (u ⊆ s ∧
      u ⊆
        {x_1 : M |
          enorm (E := TangentSpace I x_1 →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) x_1))
              (mfderiv% (↑(extChartAt I x) : M → E) x_1) <
            (↑C : ℝ≥0∞)}) ∧
    u ⊆ (extChartAt I x).source

Tactic:
simp only [subset_inter_iff] at hu

Premises used: Set.subset_inter_iff
-- 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
this :
  s ∩
        {x_1 : M |
          (fun (y : M) ↦
              enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
                  (mfderiv% (↑(extChartAt I x) : M → E) y) <
                (↑C : ℝ≥0∞))
            x_1} ∩
      (extChartAt I x).source ∈
    𝓝 x
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
hu :
  (u ⊆ s ∧
      u ⊆
        {x_1 : M |
          enorm (E := TangentSpace I x_1 →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) x_1))
              (mfderiv% (↑(extChartAt I x) : M → E) x_1) <
            (↑C : ℝ≥0∞)}) ∧
    u ⊆ (extChartAt I x).source
⊢ ∃ u ∈ 𝓝 x,
    IsClosed[inst_3] u ∧
      u ⊆ s ∧
        u ⊆
            {y : M |
              enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
                  (mfderiv% (↑(extChartAt I x) : M → E) y) <
                (↑C : ℝ≥0∞)} ∧
          u ⊆ (extChartAt I x).source

Tactic:
⟨u, u_mem, u_closed, hu.1.1, hu.1.2, hu.2⟩

Premises used: And.right, And.left, 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
this :
  s ∩
        {x_1 : M |
          (fun (y : M) ↦
              enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
                  (mfderiv% (↑(extChartAt I x) : M → E) y) <
                (↑C : ℝ≥0∞))
            x_1} ∩
      (extChartAt I x).source ∈
    𝓝 x
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
hu :
  (u ⊆ s ∧
      u ⊆
        {x_1 : M |
          enorm (E := TangentSpace I x_1 →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) x_1))
              (mfderiv% (↑(extChartAt I x) : M → E) x_1) <
            (↑C : ℝ≥0∞)}) ∧
    u ⊆ (extChartAt I x).source
⊢ ∃ u ∈ 𝓝 x,
    IsClosed[inst_3] u ∧
      u ⊆ s ∧
        u ⊆
            {y : M |
              enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
                  (mfderiv% (↑(extChartAt I x) : M → E) y) <
                (↑C : ℝ≥0∞)} ∧
          u ⊆ (extChartAt I x).source

Tactic:
exact ⟨u, u_mem, u_closed, hu.1.1, hu.1.2, hu.2⟩
-- 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
obtain :
  ∀ (u : Set M) (u_mem : u ∈ 𝓝 x) (u_closed : IsClosed[inst_3] u) (us : u ⊆ s)
    (hu :
      u ⊆
        {y : M |
          enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
              (mfderiv% (↑(extChartAt I x) : M → E) y) <
            (↑C : ℝ≥0∞)})
    (uc : u ⊆ (extChartAt I x).source), ∃ c > 0, {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s
⊢ ∃ c > 0, {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s

Tactic:
obtain ⟨u, u_mem, u_closed, us, hu, uc⟩ : ∃ u ∈ 𝓝 x, IsClosed u ∧ u ⊆ s
      ∧ u ⊆ {y | ‖mfderiv% (extChartAt I x) y‖ₑ < C} ∧ u ⊆ (extChartAt I x).source := by
    have := Filter.inter_mem (Filter.inter_mem hs hC) (extChartAt_source_mem_nhds (I := I) x)
    rcases exists_mem_nhds_isClosed_subset this with ⟨u, u_mem, u_closed, hu⟩
    simp only [subset_inter_iff] at hu
    exact ⟨u, u_mem, u_closed, hu.1.1, hu.1.2, hu.2⟩

Premises used: extChartAt, nhds, PartialEquiv.source
-- 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
⊢ u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
simpa [extChartAt_source I x] using uc

Premises used: extChartAt_source
-- 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
⊢ u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
have uc' : u ⊆ (chartAt H x).source := by simpa [extChartAt_source I x] using uc
-- 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ ∃ (v : Set M), (v ∈ 𝓝 x ∧ IsOpen[inst_3] v) ∧ v ⊆ u

Tactic:
(nhds_basis_opens' x).mem_iff.1 u_mem

Premises used: Filter.HasBasis.mem_iff, nhds_basis_opens', Iff.mp
-- 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
obtain :
  ∀ (v : Set M) (hv : v ⊆ u) (v_mem : v ∈ 𝓝 x) (v_open : IsOpen[inst_3] v),
    ∃ c > 0, {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s
⊢ ∃ c > 0, {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s

Tactic:
obtain ⟨v, ⟨v_mem, v_open⟩, hv⟩ : ∃ v, (v ∈ 𝓝 x ∧ IsOpen v) ∧ v ⊆ u :=
    (nhds_basis_opens' x).mem_iff.1 u_mem

Premises used: Filter.HasBasis.mem_iff, nhds_basis_opens', Iff.mp
-- 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
⊢ ∃ r > 0, ball ((↑(extChartAt I x) : M → E) x) r ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v

Tactic:
Metric.mem_nhds_iff.1 (extChartAt_preimage_mem_nhds v_mem)

Premises used: extChartAt_preimage_mem_nhds, Metric.mem_nhds_iff, Iff.mp
-- 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
obtain :
  ∀ (r : ℝ) (r_pos : r > 0) (hr : ball ((↑(extChartAt I x) : M → E) x) r ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v),
    ∃ c > 0, {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s
⊢ ∃ c > 0, {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s

Tactic:
obtain ⟨r, r_pos, hr⟩ : ∃ r > 0, ball (extChartAt I x x) r ⊆ (extChartAt I x).symm ⁻¹' v :=
    Metric.mem_nhds_iff.1 (extChartAt_preimage_mem_nhds v_mem)

Premises used: extChartAt, PartialEquiv.symm, extChartAt_preimage_mem_nhds, Metric.mem_nhds_iff, Iff.mp
-- 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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ
r_pos : r > 0
hr : ball ((↑(extChartAt I x) : M → E) x) r ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
⊢ 0 ≤ r

Tactic:
r_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
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (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∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ
r_pos : r > 0
hr : ball ((↑(extChartAt I x) : M → E) x) r ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
lift :
  ∀ (r : ℝ≥0) (r_pos : (↑r : ℝ) > 0)
    (hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v),
    ∃ c > 0, {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s
⊢ ∃ c > 0, {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s

Tactic:
lift r to ℝ≥0 using r_pos.le

Premises used: LT.lt.le