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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hy : x ∈ f.source
rwa : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = 𝓝[range (↑I : H → E)] ((↑I : H → E) ∘ (↑f : M → H)) x
rwa₁ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑I : H → E) ((↑f : M → H) x)
rwa₂ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = map (↑I : H → E) (𝓝 ((↑f : M → H) x))
rwa₃ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = map (↑I : H → E) (map (↑f : M → H) (𝓝 x))
rwa₄ : x ∈ f.source
rwa₅ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x)
rwa₆ : x ∈ f.source
rwa₇ : map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x) = map ((↑I : H → E) ∘ (↑f : M → H)) (𝓝 x)
rwa₈ rwa₉ rwa₁₀ : x ∈ f.source
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x

Tactic:
rwa [extend_coe, comp_apply, ← I.map_nhds_eq, ← f.map_nhds_eq, map_map]

Premises used: Filter.map_map, ModelWithCorners.map_nhds_eq, OpenPartialHomeomorph.extend_coe, Function.comp_apply, OpenPartialHomeomorph.map_nhds_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : (↑(f.extend I) : M → E) x ∈ interior (range (↑I : H → E))
rw : range (↑I : H → E) ∈ 𝓝 ((↑(f.extend I) : M → E) x)
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝 ((↑(f.extend I) : M → E) x)

Tactic:
rw [f.map_extend_nhds hx, nhdsWithin_eq_nhds]

Premises used: nhdsWithin_eq_nhds, OpenPartialHomeomorph.map_extend_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : (↑(f.extend I) : M → E) x ∈ interior (range (↑I : H → E))
⊢ range (↑I : H → E) ∈ 𝓝 ((↑(f.extend I) : M → E) x)

Tactic:
mem_of_superset (isOpen_interior.mem_nhds h'x) interior_subset

Premises used: interior_subset, isOpen_interior, IsOpen.mem_nhds, Filter.mem_of_superset
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : (↑(f.extend I) : M → E) x ∈ interior (range (↑I : H → E))
⊢ range (↑I : H → E) ∈ 𝓝 ((↑(f.extend I) : M → E) x)

Tactic:
exact mem_of_superset (isOpen_interior.mem_nhds h'x) interior_subset

Premises used: interior_subset, isOpen_interior, IsOpen.mem_nhds, Filter.mem_of_superset
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : I.Boundaryless
x : M
hx : x ∈ f.source
rw : 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x = 𝓝 ((↑(f.extend I) : M → E) x)
rw₁ : 𝓝[univ] (↑(f.extend I) : M → E) x = 𝓝 ((↑(f.extend I) : M → E) x)
rw₂ rw₃ : 𝓝 ((↑(f.extend I) : M → E) x) = 𝓝 ((↑(f.extend I) : M → E) x)
⊢ map (↑(f.extend I) : M → E) (𝓝 x) = 𝓝 ((↑(f.extend I) : M → E) x)

Tactic:
rw [f.map_extend_nhds hx, I.range_eq_univ, nhdsWithin_univ]

Premises used: nhdsWithin_univ, OpenPartialHomeomorph.map_extend_nhds, 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
rw : (↑(f.extend I) : M → E) '' (f.extend I).source ∈ map (↑(f.extend I) : M → E) (𝓝 y)
⊢ (f.extend I).target ∈ 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y

Tactic:
rw [← PartialEquiv.image_source_eq_target, ← map_extend_nhds f hy]

Premises used: PartialEquiv.image_source_eq_target, OpenPartialHomeomorph.map_extend_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ (↑(f.extend I) : M → E) '' (f.extend I).source ∈ map (↑(f.extend I) : M → E) (𝓝 y)

Tactic:
image_mem_map (extend_source_mem_nhds _ hy)

Premises used: OpenPartialHomeomorph.extend_source_mem_nhds, Filter.image_mem_map
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ (↑(f.extend I) : M → E) '' (f.extend I).source ∈ map (↑(f.extend I) : M → E) (𝓝 y)

Tactic:
exact image_mem_map (extend_source_mem_nhds _ hy)

Premises used: OpenPartialHomeomorph.extend_source_mem_nhds, Filter.image_mem_map
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
rw : (↑f : M → H) ⁻¹' f.target ∈ 𝓝 x
⊢ (↑I : H → E) '' f.target ∈ 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) x

Tactic:
rw [← f.map_extend_nhds hx, Filter.mem_map,
    f.extend_coe, Set.preimage_comp, I.preimage_image f.target]

Premises used: ModelWithCorners.preimage_image, PartialEquiv.target, OpenPartialHomeomorph.map_extend_nhds, Set.preimage_comp, OpenPartialHomeomorph.extend_coe, OpenPartialHomeomorph.toPartialEquiv, Filter.mem_map
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
⊢ (↑f : M → H) ⁻¹' f.target ∈ 𝓝 x

Tactic:
(f.continuousAt hx).preimage_mem_nhds (f.open_target.mem_nhds (f.map_source hx))

Premises used: OpenPartialHomeomorph.continuousAt, ContinuousAt.preimage_mem_nhds, OpenPartialHomeomorph.map_source, IsOpen.mem_nhds, OpenPartialHomeomorph.open_target
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
⊢ (↑f : M → H) ⁻¹' f.target ∈ 𝓝 x

Tactic:
exact (f.continuousAt hx).preimage_mem_nhds (f.open_target.mem_nhds (f.map_source hx))

Premises used: OpenPartialHomeomorph.continuousAt, ContinuousAt.preimage_mem_nhds, OpenPartialHomeomorph.map_source, IsOpen.mem_nhds, OpenPartialHomeomorph.open_target
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
rw : (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s ∈ 𝓝 x
⊢ (↑(f.extend I) : M → E) '' s ∈ 𝓝 ((↑(f.extend I) : M → E) x)

Tactic:
rw [← f.map_extend_nhds_of_boundaryless hx, Filter.mem_map]

Premises used: OpenPartialHomeomorph.map_extend_nhds_of_boundaryless, Filter.mem_map
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
⊢ ∀ a ∈ s, a ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s

Tactic:
subset_preimage_image (f.extend I) s

Premises used: Set.Subset, PartialEquiv.toFun, Set.subset_preimage_image, OpenPartialHomeomorph.extend
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst_5 : I.Boundaryless
x : M
hx : x ∈ f.source
s : Set M
h : s ∈ 𝓝 x
h₁ :
  ∀ (a : M),
    Membership.mem (γ := Set M) {x : M | x ∈ s → x ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s} a
h₂ : ∀ a ∈ s, a ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s
⊢ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s ∈ 𝓝 x

Tactic:
filter_upwards [h] using subset_preimage_image (f.extend I) s

Premises used: PartialEquiv.toFun, Set.subset_preimage_image, OpenPartialHomeomorph.extend
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : (↑(f.extend I) : M → E) x ∈ interior (range (↑I : H → E))
s : Set M
h : s ∈ 𝓝 x
rw : (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s ∈ 𝓝 x
⊢ (↑(f.extend I) : M → E) '' s ∈ 𝓝 ((↑(f.extend I) : M → E) x)

Tactic:
rw [← f.map_extend_nhds_of_mem_interior_range hx h'x, Filter.mem_map]

Premises used: OpenPartialHomeomorph.map_extend_nhds_of_mem_interior_range, Filter.mem_map
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : (↑(f.extend I) : M → E) x ∈ interior (range (↑I : H → E))
s : Set M
h : s ∈ 𝓝 x
⊢ ∀ a ∈ s, a ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s

Tactic:
subset_preimage_image (f.extend I) s

Premises used: Set.Subset, PartialEquiv.toFun, Set.subset_preimage_image, OpenPartialHomeomorph.extend
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
h'x : (↑(f.extend I) : M → E) x ∈ interior (range (↑I : H → E))
s : Set M
h : s ∈ 𝓝 x
h₁ :
  ∀ (a : M),
    Membership.mem (γ := Set M) {x : M | x ∈ s → x ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s} a
h₂ : ∀ a ∈ s, a ∈ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s
⊢ (↑(f.extend I) : M → E) ⁻¹' (↑(f.extend I) : M → E) '' s ∈ 𝓝 x

Tactic:
filter_upwards [h] using subset_preimage_image (f.extend I) s

Premises used: PartialEquiv.toFun, Set.subset_preimage_image, OpenPartialHomeomorph.extend
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (f.extend I).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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
rw : (↑I.symm : E → H) ⁻¹' f.target ∩ interior (range (↑I : H → E)) ⊆ interior (range (↑I : H → E))
⊢ interior (f.extend I).target ⊆ interior (range (↑I : H → E))

Tactic:
rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq]

Premises used: interior_inter, OpenPartialHomeomorph.extend_target, ModelWithCorners.continuous_symm, IsOpen.interior_eq, 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (↑I.symm : E → H) ⁻¹' f.target ∩ interior (range (↑I : H → E)) ⊆ interior (range (↑I : H → E))

Tactic:
inter_subset_right

Premises used: Set.inter_subset_right
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (↑I.symm : E → H) ⁻¹' f.target ∩ interior (range (↑I : H → E)) ⊆ interior (range (↑I : H → E))

Tactic:
exact inter_subset_right

Premises used: Set.inter_subset_right
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : H
hy : y ∈ f.target
hy' : (↑I : H → E) y ∈ interior (range (↑I : H → E))
rw : (↑I.symm : E → H) ((↑I : H → E) y) ∈ f.target ∧ (↑I : H → E) y ∈ interior (range (↑I : H → E))
⊢ (↑I : H → E) y ∈ interior (f.extend I).target

Tactic:
rw [f.extend_target, interior_inter, (f.open_target.preimage I.continuous_symm).interior_eq,
    mem_inter_iff, mem_preimage]

Premises used: interior_inter, Set.mem_inter_iff, OpenPartialHomeomorph.extend_target, ModelWithCorners.continuous_symm, IsOpen.interior_eq, OpenPartialHomeomorph.open_target, IsOpen.preimage, Set.mem_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : H
hy : y ∈ f.target
hy' : (↑I : H → E) y ∈ interior (range (↑I : H → E))
⊢ (↑I.symm : E → H) ((↑I : H → E) y) ∈ f.target ∧ (↑I : H → E) y ∈ interior (range (↑I : H → E))

Tactic:
⟨mem_of_eq_of_mem (I.left_inv (y)) hy, hy'⟩

Premises used: And.intro, Set.mem_of_eq_of_mem, ModelWithCorners.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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : H
hy : y ∈ f.target
hy' : (↑I : H → E) y ∈ interior (range (↑I : H → E))
⊢ (↑I.symm : E → H) ((↑I : H → E) y) ∈ f.target ∧ (↑I : H → E) y ∈ interior (range (↑I : H → E))

Tactic:
exact ⟨mem_of_eq_of_mem (I.left_inv (y)) hy, 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ 𝓝[(f.extend I).target] (↑(f.extend I) : M → E) y = 𝓝[range (↑I : H → E)] (↑(f.extend I) : M → E) y

Tactic:
(nhdsWithin_mono _ (extend_target_subset_range _)).antisymm <|
    nhdsWithin_le_of_mem (extend_target_mem_nhdsWithin _ hy)

Premises used: OpenPartialHomeomorph.extend_target_mem_nhdsWithin, LE.le.antisymm, nhdsWithin_le_of_mem, OpenPartialHomeomorph.extend_target_subset_range, nhdsWithin_mono
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ (f.extend I).target =ᶠ[𝓝 ((↑(f.extend I) : M → E) y)] range (↑I : H → E)

Tactic:
nhdsWithin_eq_iff_eventuallyEq.1 (nhdsWithin_extend_target_eq _ hy)

Premises used: nhdsWithin_eq_iff_eventuallyEq, OpenPartialHomeomorph.nhdsWithin_extend_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : E
h : x ∈ (f.extend I).target
⊢ ContinuousAt (↑(f.extend I).symm : E → M) x

Tactic:
(f.continuousAt_symm h.2).comp I.continuous_symm.continuousAt

Premises used: OpenPartialHomeomorph.toFun', Continuous.continuousAt, ModelWithCorners.continuous_symm, And.right, ContinuousAt.comp, OpenPartialHomeomorph.continuousAt_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ ContinuousOn (↑(f.extend I).symm : E → M) (f.extend I).target

Tactic:
fun _ h =>
  (continuousAt_extend_symm' _ h).continuousWithinAt

Premises used: OpenPartialHomeomorph.continuousAt_extend_symm', ContinuousAt.continuousWithinAt, ContinuousOn
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
X : Type u_8
inst_5 : TopologicalSpace X
g : M → X
s : Set M
x : M
rw :
  ContinuousWithinAt (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(f.extend I) : M → E) x) ↔
    ContinuousWithinAt ((g ∘ (↑f.symm : H → M)) ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' (↑f.symm : H → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑f : M → H) x))
⊢ ContinuousWithinAt (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(f.extend I) : M → E) x) ↔
    ContinuousWithinAt (g ∘ (↑f.symm : H → M)) ((↑f.symm : H → M) ⁻¹' s) ((↑f : M → H) x)

Tactic:
rw [← I.symm_continuousWithinAt_comp_right_iff]

Premises used: ModelWithCorners.symm_continuousWithinAt_comp_right_iff
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
X : Type u_8
inst_5 : TopologicalSpace X
g : M → X
s : Set M
x : M
⊢ ContinuousWithinAt (g ∘ (↑(f.extend I).symm : E → M)) ((↑(f.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(f.extend I) : M → E) x) ↔
    ContinuousWithinAt ((g ∘ (↑f.symm : H → M)) ∘ (↑I.symm : E → H))
      ((↑I.symm : E → H) ⁻¹' (↑f.symm : H → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑f : M → H) x))

Tactic:
rfl
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst_4] ((f.extend I).source ∩ (↑(f.extend I) : M → E) ⁻¹' s)

Tactic:
(continuousOn_extend f).isOpen_inter_preimage (isOpen_extend_source _) hs

Premises used: OpenPartialHomeomorph.isOpen_extend_source, ContinuousOn.isOpen_inter_preimage, OpenPartialHomeomorph.continuousOn_extend
-- 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rw : IsOpen[inst_4] ((f.extend I).source ∩ (↑(f.extend I) : M → E) ⁻¹' s)
⊢ IsOpen[inst_4] (f.source ∩ (↑(f.extend I) : M → E) ⁻¹' s)

Tactic:
rw [← extend_source f (I := I)]

Premises used: OpenPartialHomeomorph.extend_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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst_4] ((f.extend I).source ∩ (↑(f.extend I) : M → E) ⁻¹' s)

Tactic:
isOpen_extend_preimage' f 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsOpen[inst_4] ((f.extend I).source ∩ (↑(f.extend I) : M → E) ⁻¹' s)

Tactic:
exact isOpen_extend_preimage' f 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
f : OpenPartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
y : M
hy : y ∈ f.source
set :
  let e := f.extend I;
  map (↑e : M → E) (𝓝[s] y) = 𝓝[(↑e : M → E) '' (e.source ∩ s)] (↑e : M → E) y
⊢ map (↑(f.extend I) : M → E) (𝓝[s] y) =
    𝓝[(↑(f.extend I) : M → E) '' ((f.extend I).source ∩ s)] (↑(f.extend I) : M → E) y

Tactic:
set e := f.extend I

Premises used: OpenPartialHomeomorph.extend