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 y : M
hx : y ∈ (extChartAt I x).source
h'x : (↑(extChartAt I x) : M → E) y ∈ interior (range (↑I : H → E))
s : Set M
h : s ∈ 𝓝 y
⊢ (↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) '' s ∈
    𝓝 ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) y)

Tactic:
exact extend_image_nhds_mem_nhds_of_mem_interior_range _ (by simpa using hx) h'x h

Premises used: OpenPartialHomeomorph.extend_image_nhds_mem_nhds_of_mem_interior_range
-- 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
inst_6 : I.Boundaryless
x : M
hx : s ∈ 𝓝 x
rw :
  (↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) '' s ∈
    𝓝 ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) x)
⊢ (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [extChartAt]

Premises used: extChartAt
-- 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
inst_6 : I.Boundaryless
x : M
hx : s ∈ 𝓝 x
⊢ (↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) '' s ∈
    𝓝 ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) x)

Tactic:
extend_image_nhds_mem_nhds_of_boundaryless _ (mem_chart_source H x) hx

Premises used: mem_chart_source, OpenPartialHomeomorph.extend_image_nhds_mem_nhds_of_boundaryless
-- 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
inst_6 : I.Boundaryless
x : M
hx : s ∈ 𝓝 x
⊢ (↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) '' s ∈
    𝓝 ((↑(OpenPartialHomeomorph.extend (chartAt H x) I) : M → E) x)

Tactic:
exact extend_image_nhds_mem_nhds_of_boundaryless _ (mem_chart_source H x) hx

Premises used: mem_chart_source, OpenPartialHomeomorph.extend_image_nhds_mem_nhds_of_boundaryless
-- 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
⊢ (extChartAt I x).target ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
extChartAt_target_mem_nhdsWithin' (mem_extChartAt_source x)

Premises used: extChartAt_target_mem_nhdsWithin', mem_extChartAt_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
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
rw : (extChartAt I x).target ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)
⊢ (extChartAt I x).target ∈ 𝓝[range (↑I : H → E)] y

Tactic:
rw [← (extChartAt I x).right_inv hy]

Premises used: extChartAt, PartialEquiv.right_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
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
hy₁ : (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source
⊢ (extChartAt I x).target ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y)

Tactic:
apply extChartAt_target_mem_nhdsWithin'

Premises used: extChartAt_target_mem_nhdsWithin'
-- 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
⊢ (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source

Tactic:
(extChartAt I x).map_target hy

Premises used: PartialEquiv.map_target, extChartAt
-- 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
⊢ (↑(extChartAt I x).symm : E → M) y ∈ (extChartAt I x).source

Tactic:
exact (extChartAt I x).map_target hy

Premises used: PartialEquiv.map_target, extChartAt
-- 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
y : E
x : M
hy : y ∈ (extChartAt I x).target
rw : (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝[range (↑I : H → E)] y ⊔ 𝓝[(range (↑I : H → E))ᶜ] y
⊢ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝 y

Tactic:
rw [← nhdsWithin_univ, ← union_compl_self (range I), nhdsWithin_union]

Premises used: nhdsWithin_univ, Set.union_compl_self, ModelWithCorners.toFun', nhdsWithin_union, Set.range
-- 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
y : E
x : M
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝[range (↑I : H → E)] y ⊔ 𝓝[(range (↑I : H → E))ᶜ] y

Tactic:
Filter.union_mem_sup (extChartAt_target_mem_nhdsWithin_of_mem hy) self_mem_nhdsWithin

Premises used: extChartAt_target_mem_nhdsWithin_of_mem, self_mem_nhdsWithin, Filter.union_mem_sup
-- 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
y : E
x : M
hy : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ ∈ 𝓝[range (↑I : H → E)] y ⊔ 𝓝[(range (↑I : H → E))ᶜ] y

Tactic:
exact Filter.union_mem_sup (extChartAt_target_mem_nhdsWithin_of_mem hy) self_mem_nhdsWithin

Premises used: extChartAt_target_mem_nhdsWithin_of_mem, self_mem_nhdsWithin, Filter.union_mem_sup
-- 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
inst_6 : I.Boundaryless
x : M
simp_rw :
  IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((↑I.symm : E → H) ⁻¹' (toPartialEquiv (chartAt H x)).target)
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (extChartAt I x).target

Tactic:
simp_rw [extChartAt_target, I.range_eq_univ, inter_univ]

Premises used: Set.inter_univ, extChartAt_target, ModelWithCorners.range_eq_univ
-- 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
inst_6 : I.Boundaryless
x : M
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((↑I.symm : E → H) ⁻¹' (toPartialEquiv (chartAt H x)).target)

Tactic:
(OpenPartialHomeomorph.open_target _).preimage I.continuous_symm

Premises used: ModelWithCorners.continuous_symm, OpenPartialHomeomorph.open_target, IsOpen.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
inst_6 : I.Boundaryless
x : M
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ((↑I.symm : E → H) ⁻¹' (toPartialEquiv (chartAt H x)).target)

Tactic:
exact (OpenPartialHomeomorph.open_target _).preimage I.continuous_symm

Premises used: ModelWithCorners.continuous_symm, OpenPartialHomeomorph.open_target, IsOpen.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
inst_6 : I.Boundaryless
x : M
⊢ (extChartAt I x).target ∈ 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
extChartAt_target_mem_nhdsWithin x

Premises used: extChartAt_target_mem_nhdsWithin
-- 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
inst_6 : I.Boundaryless
x : M
h : 𝓝 ((↑(extChartAt I x) : M → E) x) = 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x
⊢ (extChartAt I x).target ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)

Tactic:
convert! extChartAt_target_mem_nhdsWithin x

Premises used: extChartAt_target_mem_nhdsWithin
-- 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
inst_6 : I.Boundaryless
x : M
⊢ 𝓝 ((↑(extChartAt I x) : M → E) x) = 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
simp only [I.range_eq_univ, nhdsWithin_univ]

Premises used: nhdsWithin_univ, ModelWithCorners.range_eq_univ
-- 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
inst_6 : I.Boundaryless
x : M
y : E
m : y ∈ (extChartAt I x).target
⊢ (extChartAt I x).target ∈ 𝓝 y

Tactic:
(isOpen_extChartAt_target x).mem_nhds m

Premises used: isOpen_extChartAt_target, 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
inst_5 : ChartedSpace H M
x : M
⊢ (extChartAt I x).target ⊆ range (↑I : H → E)

Tactic:
simp only [mfld_simps]
-- 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
z : E
hz : z ∈ (extChartAt I x).target
rw :
  𝓝[(extChartAt I x).target] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) z) =
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) z)
⊢ 𝓝[(extChartAt I x).target] z = 𝓝[range (↑I : H → E)] z

Tactic:
rw [← PartialEquiv.right_inv (extChartAt I x) hz]

Premises used: extChartAt, PartialEquiv.right_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
inst_5 : ChartedSpace H M
x : M
z : E
hz : z ∈ (extChartAt I x).target
⊢ 𝓝[(extChartAt I x).target] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) z) =
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) z)

Tactic:
nhdsWithin_extChartAt_target_eq' ((extChartAt I x).map_target hz)

Premises used: PartialEquiv.map_target, extChartAt, nhdsWithin_extChartAt_target_eq'
-- 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
z : E
hz : z ∈ (extChartAt I x).target
⊢ 𝓝[(extChartAt I x).target] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) z) =
    𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) z)

Tactic:
exact nhdsWithin_extChartAt_target_eq' ((extChartAt I x).map_target hz)

Premises used: PartialEquiv.map_target, extChartAt, nhdsWithin_extChartAt_target_eq'
-- 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
⊢ 𝓝[(extChartAt I x).target] (↑(extChartAt I x) : M → E) x = 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x

Tactic:
nhdsWithin_extChartAt_target_eq' (mem_extChartAt_source x)

Premises used: mem_extChartAt_source, nhdsWithin_extChartAt_target_eq'
-- 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 y : M
hy : y ∈ (extChartAt I x).source
⊢ (extChartAt I x).target =ᶠ[𝓝 ((↑(extChartAt I x) : M → E) y)] range (↑I : H → E)

Tactic:
nhdsWithin_eq_iff_eventuallyEq.1 (nhdsWithin_extChartAt_target_eq' hy)

Premises used: nhdsWithin_eq_iff_eventuallyEq, Iff.mp, nhdsWithin_extChartAt_target_eq'
-- 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
z : E
hz : z ∈ (extChartAt I x).target
⊢ (extChartAt I x).target =ᶠ[𝓝 z] range (↑I : H → E)

Tactic:
nhdsWithin_eq_iff_eventuallyEq.1 (nhdsWithin_extChartAt_target_eq_of_mem hz)

Premises used: nhdsWithin_eq_iff_eventuallyEq, nhdsWithin_extChartAt_target_eq_of_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
inst_5 : ChartedSpace H M
x : M
⊢ (extChartAt I x).target =ᶠ[𝓝 ((↑(extChartAt I x) : M → E) x)] range (↑I : H → E)

Tactic:
nhdsWithin_eq_iff_eventuallyEq.1 (nhdsWithin_extChartAt_target_eq x)

Premises used: nhdsWithin_eq_iff_eventuallyEq, nhdsWithin_extChartAt_target_eq, 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
y : E
h : y ∈ (extChartAt I x).target
⊢ ContinuousAt (↑(extChartAt I x).symm : E → M) y

Tactic:
continuousAt_extend_symm' _ h

Premises used: extChartAt, OpenPartialHomeomorph.continuousAt_extend_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 x' : M
h : x' ∈ (extChartAt I x).source
⊢ ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x')

Tactic:
continuousAt_extChartAt_symm'' <| (extChartAt I x).map_source h

Premises used: extChartAt, PartialEquiv.map_source, 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
inst_5 : ChartedSpace H M
x : M
⊢ ContinuousAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x)

Tactic:
continuousAt_extChartAt_symm' (mem_extChartAt_source x)

Premises used: mem_extChartAt_source, 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
inst_5 : ChartedSpace H M
x : M
⊢ ContinuousOn (↑(extChartAt I x).symm : E → M) (extChartAt I x).target

Tactic:
fun _y hy => (continuousAt_extChartAt_symm'' hy).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, ContinuousOn, 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
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
rw : ∀ t ∈ 𝓝 y, (t ∩ interior (extChartAt I x).target).Nonempty
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (extChartAt I x).target)

Tactic:
rw [mem_closure_iff_nhds]

Premises used: mem_closure_iff_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
inst_5 : ChartedSpace H M
x : M
y : E
hy : y ∈ (extChartAt I x).target
t : Set E
ht : t ∈ 𝓝 y
⊢ t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∈ 𝓝 y

Tactic:
have A : t ∩ ((extChartAt I x).target ∪ (range I)ᶜ) ∈ 𝓝 y :=
    inter_mem ht (extChartAt_target_union_compl_range_mem_nhds_of_mem 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
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
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))

Tactic:
apply I.range_subset_closure_interior (extChartAt_target_subset_range x hy)

Premises used: extChartAt_target_subset_range, ModelWithCorners.range_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
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
⊢ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (interior (range (↑I : H → E)))

Tactic:
have B : y ∈ closure (interior (range I)) := by
    apply I.range_subset_closure_interior (extChartAt_target_subset_range x 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
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)))
⊢ (t ∩ ((extChartAt I x).target ∪ (range (↑I : H → E))ᶜ) ∩ interior (range (↑I : H → E))).Nonempty

Tactic:
mem_closure_iff_nhds.1 B _ A

Premises used: mem_closure_iff_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
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)))
obtain :
  ∀ (z : E) (hz : z ∈ interior (range (↑I : H → E))) (tz : z ∈ t)
    (h'z : z ∈ (extChartAt I x).target ∪ (range (↑I : H → E))ᶜ), (t ∩ interior (extChartAt I x).target).Nonempty
⊢ (t ∩ interior (extChartAt I x).target).Nonempty

Tactic:
obtain ⟨z, ⟨tz, h'z⟩, hz⟩ :
      (t ∩ ((extChartAt I x).target ∪ (range ↑I)ᶜ) ∩ interior (range I)).Nonempty :=
    mem_closure_iff_nhds.1 B _ A

Premises used: extChartAt, mem_closure_iff_nhds, PartialEquiv.target, Compl.compl, ModelWithCorners.toFun', Inter.inter, Set.Nonempty, interior, Iff.mp, Set.range, Union.union
-- 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))ᶜ
⊢ (t ∩ interior (extChartAt I x).target).Nonempty

Tactic:
⟨z, ⟨tz, ?_⟩⟩

Premises used: Set.Nonempty, And.intro, Exists.intro