awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∈ 𝓝 y
B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
z : E
hz : z ∈ interior (range (↑I : H → E))
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ
refine : z ∈ interior (extChartAt I x).target
⊢ (t ∩ interior (extChartAt I x).target).Nonempty

Tactic:
refine ⟨z, ⟨tz, ?_⟩⟩
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∈ 𝓝 y
B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
z : E
hz : z ∈ interior (range (↑I : H → E))
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ
⊢ z ∈ (extChartAt I x).target

Tactic:
simpa [interior_subset hz] using h'z

Premises used: interior_subset
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∈ 𝓝 y
B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
z : E
hz : z ∈ interior (range (↑I : H → E))
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ
⊢ z ∈ (extChartAt I x).target

Tactic:
have h''z : z ∈ (extChartAt I x).target := by simpa [interior_subset hz] using h'z
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∈ 𝓝 y
B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
z : E
hz : z ∈ interior (range (↑I : H → E))
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ
h''z : z ∈ (extChartAt I x).target
⊢ z ∈ interior (extChartAt I x).target

Tactic:
(extChartAt_target_eventuallyEq_of_mem h''z).symm.mem_interior hz

Premises used: Filter.EventuallyEq.mem_interior, extChartAt_target_eventuallyEq_of_mem, Filter.EventuallyEq.symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
A : t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∈ 𝓝 y
B : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))
z : E
hz : z ∈ interior (range (↑I : H → E))
tz : z ∈ t
h'z : z ∈ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ
h''z : z ∈ (extChartAt I x).target
⊢ z ∈ interior (extChartAt I x).target

Tactic:
exact (extChartAt_target_eventuallyEq_of_mem h''z).symm.mem_interior hz

Premises used: Filter.EventuallyEq.mem_interior, extChartAt_target_eventuallyEq_of_mem, Filter.EventuallyEq.symm
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
by_contra! : ∀ (H : interior (extChartAt I x).target = ∅), False
⊢ (interior (extChartAt I x).target).Nonempty

Tactic:
by_contra! H
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H_1 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H_1
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H_1
inst_5 : ChartedSpace H_1 M
x : M
H : interior (extChartAt I x).target = ∅
⊢ (↑(extChartAt I x) : M → E) x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x).target)

Tactic:
have := extChartAt_target_subset_closure_interior (mem_extChartAt_target (I := I) x)
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H_1 : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H_1
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H_1
inst_5 : ChartedSpace H_1 M
x : M
H : interior (extChartAt I x).target = ∅
this :
  (↑(extChartAt I x) : M → E) x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x).target)
⊢ False

Tactic:
simp only [H, closure_empty, mem_empty_iff_false] at this

Premises used: Set.mem_empty_iff_false, closure_empty
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
simp_rw :
  ∀ (o : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o →
      (↑(extChartAt I x₀) : M → E) x ∈ o →
        (o ∩ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty
⊢ (↑(extChartAt I x₀) : M → E) x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∩ (extChartAt I x₀).target))

Tactic:
simp_rw [mem_closure_iff, interior_inter, ← inter_assoc]

Premises used: mem_closure_iff, interior_inter, Set.inter_assoc
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
⊢ (↑(extChartAt I x₀) : M → E) ⁻¹' o ∈ 𝓝 x

Tactic:
apply (continuousAt_extChartAt' h'x).preimage_mem_nhds (o_open.mem_nhds ho)

Premises used: ContinuousAt.preimage_mem_nhds, continuousAt_extChartAt', IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
⊢ (↑(extChartAt I x₀) : M → E) ⁻¹' o ∈ 𝓝 x

Tactic:
have : (extChartAt I x₀) ⁻¹' o ∈ 𝓝 x := by
      apply (continuousAt_extChartAt' h'x).preimage_mem_nhds (o_open.mem_nhds ho)
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
this : (↑(extChartAt I x₀) : M → E) ⁻¹' o ∈ 𝓝 x
⊢ ((↑(extChartAt I x₀) : M → E) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty

Tactic:
(mem_closure_iff_nhds.1 hx) _ (inter_mem this ?_)

Premises used: mem_closure_iff_nhds, Filter.inter_mem, Iff.mp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
this : (↑(extChartAt I x₀) : M → E) ⁻¹' o ∈ 𝓝 x
refine : (extChartAt I x₀).source ∈ 𝓝 x
⊢ ((↑(extChartAt I x₀) : M → E) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty

Tactic:
refine (mem_closure_iff_nhds.1 hx) _ (inter_mem this ?_)

Premises used: mem_closure_iff_nhds, Filter.inter_mem, Iff.mp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
this : (↑(extChartAt I x₀) : M → E) ⁻¹' o ∈ 𝓝 x
⊢ (extChartAt I x₀).source ∈ 𝓝 x

Tactic:
apply (isOpen_extChartAt_source x₀).mem_nhds h'x

Premises used: isOpen_extChartAt_source, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
obtain :
  ∀ (y : M) (ys : y ∈ interior s) (yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o) (hy : y ∈ (extChartAt I x₀).source),
    (o ∩ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty
⊢ (o ∩ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty

Tactic:
obtain ⟨y, ⟨yo, hy⟩, ys⟩ :
      ((extChartAt I x₀) ⁻¹' o ∩ (extChartAt I x₀).source ∩ interior s).Nonempty := by
    have : (extChartAt I x₀) ⁻¹' o ∈ 𝓝 x := by
      apply (continuousAt_extChartAt' h'x).preimage_mem_nhds (o_open.mem_nhds ho)
    refine (mem_closure_iff_nhds.1 hx) _ (inter_mem this ?_)
    apply (isOpen_extChartAt_source x₀).mem_nhds h'x

Premises used: extChartAt, Inter.inter, Set.Nonempty, Set.preimage, interior, PartialEquiv.source, PartialEquiv.toFun
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
simp : (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
⊢ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)

Tactic:
simp only [interior_mem_nhds]

Premises used: interior_mem_nhds
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
apply : s ∈ 𝓝 ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) y))
⊢ (↑(extChartAt I x₀).symm : E → M) ⁻¹' s ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)

Tactic:
apply (continuousAt_extChartAt_symm' hy).preimage_mem_nhds

Premises used: ContinuousAt.preimage_mem_nhds, continuousAt_extChartAt_symm'
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
simp : s ∈ 𝓝 y
⊢ s ∈ 𝓝 ((↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) y))

Tactic:
simp only [hy, PartialEquiv.left_inv]

Premises used: PartialEquiv.left_inv
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ s ∈ 𝓝 y

Tactic:
mem_interior_iff_mem_nhds.mp ys

Premises used: mem_interior_iff_mem_nhds, Iff.mp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ s ∈ 𝓝 y

Tactic:
exact mem_interior_iff_mem_nhds.mp ys

Premises used: mem_interior_iff_mem_nhds, Iff.mp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)

Tactic:
have A : interior (↑(extChartAt I x₀).symm ⁻¹' s) ∈ 𝓝 (extChartAt I x₀ y) := by
    simp only [interior_mem_nhds]
    apply (continuousAt_extChartAt_symm' hy).preimage_mem_nhds
    simp only [hy, PartialEquiv.left_inv]
    exact mem_interior_iff_mem_nhds.mp ys
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
a : (↑(extChartAt I x₀) : M → E) y ∈ (extChartAt I x₀).target
⊢ (↑(extChartAt I x₀) : M → E) y ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x₀).target)

Tactic:
apply extChartAt_target_subset_closure_interior (x := x₀)

Premises used: extChartAt_target_subset_closure_interior
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
⊢ (↑(extChartAt I x₀) : M → E) y ∈ (extChartAt I x₀).target

Tactic:
(extChartAt I x₀).map_source hy

Premises used: extChartAt, PartialEquiv.map_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
⊢ (↑(extChartAt I x₀) : M → E) y ∈ (extChartAt I x₀).target

Tactic:
exact (extChartAt I x₀).map_source hy

Premises used: extChartAt, PartialEquiv.map_source
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
⊢ (↑(extChartAt I x₀) : M → E) y ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x₀).target)

Tactic:
have B : (extChartAt I x₀) y ∈ closure (interior (extChartAt I x₀).target) := by
    apply extChartAt_target_subset_closure_interior (x := x₀)
    exact (extChartAt I x₀).map_source hy
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
B :
  (↑(extChartAt I x₀) : M → E) y ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x₀).target)
⊢ (o ∩ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty

Tactic:
mem_closure_iff_nhds.1 B _ (inter_mem (o_open.mem_nhds yo) A)

Premises used: mem_closure_iff_nhds, Filter.inter_mem, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst_5 : ChartedSpace H M
x₀ x : M
hx : x ∈ closure[inst_4] (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o
ho : (↑(extChartAt I x₀) : M → E) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ (↑(extChartAt I x₀) : M → E) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
A : interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) y)
B :
  (↑(extChartAt I x₀) : M → E) y ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x₀).target)
⊢ (o ∩ interior ((↑(extChartAt I x₀).symm : E → M) ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty

Tactic:
exact mem_closure_iff_nhds.1 B _ (inter_mem (o_open.mem_nhds yo) A)

Premises used: mem_closure_iff_nhds, Filter.inter_mem, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst_4] ((extChartAt I x).source ∩ (↑(extChartAt I x) : M → E) ⁻¹' s)

Tactic:
isOpen_extend_preimage' _ hs

Premises used: OpenPartialHomeomorph.isOpen_extend_preimage'
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : ChartedSpace H M
x : M
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rw : IsOpen[inst_4] ((extChartAt I x).source ∩ (↑(extChartAt I x) : M → E) ⁻¹' s)
⊢ IsOpen[inst_4] ((toPartialEquiv (chartAt H x)).source ∩ (↑(extChartAt I x) : M → E) ⁻¹' s)

Tactic:
rw [← extChartAt_source I]

Premises used: extChartAt_source