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
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
G : Type u_8
G' : Type u_9
F : Type u_10
F' : Type u_11
N : Type u_12
N' : Type u_13
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup F'
inst_14 : NormedSpace 𝕜 F'
inst_15 : TopologicalSpace G
inst_16 : TopologicalSpace N
inst_17 : TopologicalSpace G'
inst_18 : TopologicalSpace N'
J : ModelWithCorners 𝕜 F G
J' : ModelWithCorners 𝕜 F' G'
inst_19 : ChartedSpace G N
inst_20 : ChartedSpace G' N'
f : M → N
g : M' → N'
x : M
x' : M'
p : E × E'
⊢ (writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) p).2 =
    (Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g) p).2

Tactic:
simp [writtenInExtChartAt, I.toPartialEquiv.prod_symm, (chartAt H x).toPartialEquiv.prod_symm]

Premises used: chartAt, ModelWithCorners.toPartialEquiv, PartialEquiv.prod_symm, writtenInExtChartAt, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x : H
⊢ (↑(extChartAt I x) : H → E) = (↑I : H → E)

Tactic:
rfl

Premises used: setOf, Set.inter, ModelWithCorners.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
H : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
x y : H
⊢ (↑(extChartAt I x) : H → E) y = (↑I : H → E) y

Tactic:
rfl

Premises used: ModelWithCorners.toFun', rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
⊢ extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x y : E
⊢ (↑(extChartAt 𝓘(𝕜, E) x) : E → E) y = y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
x : M × M'
simp :
  (toPartialEquiv (chartAt H x.1)).prod (toPartialEquiv (chartAt H' x.2)) ≫ I.prod I'.toPartialEquiv =
    (toPartialEquiv (chartAt H x.1) ≫ I.toPartialEquiv).prod (toPartialEquiv (chartAt H' x.2) ≫ I'.toPartialEquiv)
⊢ extChartAt (I.prod I') x = (extChartAt I x.1).prod (extChartAt I' x.2)

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
E' : Type u_5
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
inst_4 : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
inst_7 : TopologicalSpace H'
inst_8 : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
inst_9 : ChartedSpace H M
inst_10 : ChartedSpace H' M'
x : M × M'
rw rw₁ :
  (toPartialEquiv (chartAt H x.1) ≫ I.toPartialEquiv).prod (toPartialEquiv (chartAt H' x.2) ≫ I'.toPartialEquiv) =
    (toPartialEquiv (chartAt H x.1) ≫ I.toPartialEquiv).prod (toPartialEquiv (chartAt H' x.2) ≫ I'.toPartialEquiv)
⊢ (toPartialEquiv (chartAt H x.1)).prod (toPartialEquiv (chartAt H' x.2)) ≫ I.prod I'.toPartialEquiv =
    (toPartialEquiv (chartAt H x.1) ≫ I.toPartialEquiv).prod (toPartialEquiv (chartAt H' x.2) ≫ I'.toPartialEquiv)

Tactic:
rw [PartialEquiv.prod_trans]

Premises used: PartialEquiv.prod_trans
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
H : Type u_4
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst_4 : TopologicalSpace H'
inst_5 : TopologicalSpace M'
inst_6 : ChartedSpace H' M'
inst_7 : ChartedSpace H H'
x : M'
⊢ extChartAt I x = toPartialEquiv (chartAt H' x) ≫ extChartAt I ((↑(chartAt H' x) : M' → H') x)

Tactic:
PartialEquiv.trans_assoc ..

Premises used: extChartAt, PartialEquiv.restr, PartialEquiv.trans, PartialEquiv.symm, OpenPartialHomeomorph.toFun', PartialEquiv.IsImage.restr, PartialEquiv.trans_assoc, PartialEquiv.trans', OpenPartialHomeomorph.extend
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
H : Type u_4
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst_4 : TopologicalSpace H'
inst_5 : TopologicalSpace M'
inst_6 : ChartedSpace H' M'
inst_7 : ChartedSpace H H'
x : M'
y : E
hy : y ∈ (extChartAt I x).target
this : ChartedSpace H M' := ChartedSpace.comp H H' M'
⊢ writtenInExtChartAt I I x (↑(chartAt H' x) : M' → H') y = y

Tactic:
simp_all only [mfld_simps, chartAt_comp]

Premises used: chartAt_comp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
𝕜 : Type u_1
E : Type u_2
H : Type u_4
M' : Type u_6
H' : Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst_4 : TopologicalSpace H'
inst_5 : TopologicalSpace M'
inst_6 : ChartedSpace H' M'
inst_7 : ChartedSpace H H'
x : M'
y : E
hy : y ∈ (extChartAt I x).target
this : ChartedSpace H M' := ChartedSpace.comp H H' M'
⊢ writtenInExtChartAt I I ((↑(chartAt H' x) : M' → H') x) (↑(OpenPartialHomeomorph.symm (chartAt H' x)) : H' → M') y = y

Tactic:
simp_all only [mfld_simps, chartAt_comp]

Premises used: chartAt_comp
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace 𝕜
inst_7 : FiniteDimensional 𝕜 E
⊢ ProperSpace E

Tactic:
have : ProperSpace E := FiniteDimensional.proper 𝕜 E
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace 𝕜
inst_7 : FiniteDimensional 𝕜 E
this : ProperSpace E
⊢ LocallyCompactSpace H

Tactic:
have : LocallyCompactSpace H := I.locallyCompactSpace
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace 𝕜
inst_7 : FiniteDimensional 𝕜 E
this_1 : ProperSpace E
this : LocallyCompactSpace H
⊢ LocallyCompactSpace M

Tactic:
ChartedSpace.locallyCompactSpace H M

Premises used: ChartedSpace.locallyCompactSpace
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace 𝕜
inst_7 : FiniteDimensional 𝕜 E
this_1 : ProperSpace E
this : LocallyCompactSpace H
⊢ LocallyCompactSpace M

Tactic:
exact ChartedSpace.locallyCompactSpace H M

Premises used: ChartedSpace.locallyCompactSpace
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
h : Nonempty M
inst_6 : LocallyCompactSpace M
rcases : ∀ (x : M), LocallyCompactSpace E
⊢ LocallyCompactSpace E

Tactic:
rcases h with ⟨x⟩
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
obtain : ∀ (y : E) (hy : y ∈ interior (extChartAt I x).target), LocallyCompactSpace E
⊢ LocallyCompactSpace E

Tactic:
obtain ⟨y, hy⟩ := interior_extChartAt_target_nonempty I x

Premises used: interior_extChartAt_target_nonempty
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
⊢ y ∈ (extChartAt I x).target

Tactic:
have h'y : y ∈ (extChartAt I x).target := interior_subset hy
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
obtain :
  ∀ (s : Set M) (hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)) (hss : s ⊆ (extChartAt I x).source)
    (hcom : IsCompact s), LocallyCompactSpace E
⊢ LocallyCompactSpace E

Tactic:
obtain ⟨s, hmem, hss, hcom⟩ :=
    LocallyCompactSpace.local_compact_nhds ((extChartAt I x).symm y) (extChartAt I x).source
      ((isOpen_extChartAt_source x).mem_nhds ((extChartAt I x).map_target h'y))

Premises used: PartialEquiv.map_target, extChartAt, PartialEquiv.symm, isOpen_extChartAt_source, LocallyCompactSpace.local_compact_nhds, IsOpen.mem_nhds, PartialEquiv.source, PartialEquiv.toFun
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
⊢ IsCompact ((↑(extChartAt I x) : M → E) '' s)

Tactic:
have : IsCompact <| (extChartAt I x) '' s :=
    hcom.image_of_continuousOn <| (continuousOn_extChartAt x).mono hss
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact ((↑(extChartAt I x) : M → E) '' s)
apply : (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 y
⊢ LocallyCompactSpace E

Tactic:
apply this.locallyCompactSpace_of_mem_nhds_of_addGroup (x := y)

Premises used: IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact ((↑(extChartAt I x) : M → E) '' s)
rw : (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))
⊢ (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 y

Tactic:
rw [← (extChartAt I x).right_inv h'y]

Premises used: extChartAt, PartialEquiv.right_inv
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact ((↑(extChartAt I x) : M → E) '' s)
apply : (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y) ∈ interior (range (↑I : H → E))
⊢ (↑(extChartAt I x) : M → E) '' s ∈ 𝓝 ((↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y))

Tactic:
apply extChartAt_image_nhds_mem_nhds_of_mem_interior_range
    (PartialEquiv.map_target (extChartAt I x) h'y) _ hmem

Premises used: PartialEquiv.map_target, extChartAt, extChartAt_image_nhds_mem_nhds_of_mem_interior_range
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact ((↑(extChartAt I x) : M → E) '' s)
simp : y ∈ interior (range (↑I : H → E))
⊢ (↑(extChartAt I x) : M → E) ((↑(extChartAt I x).symm : E → M) y) ∈ interior (range (↑I : H → E))

Tactic:
simp only [(extChartAt I x).right_inv h'y]

Premises used: extChartAt, PartialEquiv.right_inv
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact ((↑(extChartAt I x) : M → E) '' s)
⊢ y ∈ interior (range (↑I : H → E))

Tactic:
interior_mono (extChartAt_target_subset_range x) hy

Premises used: interior_mono, extChartAt_target_subset_range
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst_6 : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 ((↑(extChartAt I x).symm : E → M) y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact ((↑(extChartAt I x) : M → E) '' s)
⊢ y ∈ interior (range (↑I : H → E))

Tactic:
exact interior_mono (extChartAt_target_subset_range x) hy

Premises used: interior_mono, extChartAt_target_subset_range
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : CompleteSpace 𝕜
I : ModelWithCorners 𝕜 E H
inst_7 : Nonempty M
inst_8 : LocallyCompactSpace M
⊢ LocallyCompactSpace E

Tactic:
have := LocallyCompactSpace.of_locallyCompact_manifold M I
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : CompleteSpace 𝕜
I : ModelWithCorners 𝕜 E H
inst_7 : Nonempty M
inst_8 : LocallyCompactSpace M
this : LocallyCompactSpace E
⊢ FiniteDimensional 𝕜 E

Tactic:
FiniteDimensional.of_locallyCompactSpace 𝕜

Premises used: FiniteDimensional.of_locallyCompactSpace
-- Module: Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
Goal:
E : Type u_8
𝕜 : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_10
inst_3 : TopologicalSpace H
M : Type u_11
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : CompleteSpace 𝕜
I : ModelWithCorners 𝕜 E H
inst_7 : Nonempty M
inst_8 : LocallyCompactSpace M
this : LocallyCompactSpace E
⊢ FiniteDimensional 𝕜 E

Tactic:
exact FiniteDimensional.of_locallyCompactSpace 𝕜

Premises used: FiniteDimensional.of_locallyCompactSpace
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
⊢ I.IsInteriorPoint x ↔ (↑(extChartAt I x) : M → E) x ∈ interior (extChartAt I x).target

Tactic:
⟨fun h ↦ (chartAt H x).mem_interior_extend_target (mem_chart_target H x) h,
    fun h ↦ OpenPartialHomeomorph.interior_extend_target_subset_interior_range _ h⟩

Premises used: OpenPartialHomeomorph.mem_interior_extend_target, chartAt, OpenPartialHomeomorph.interior_extend_target_subset_interior_range, Iff.intro, mem_chart_target
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
⊢ I.IsBoundaryPoint x ↔ (↑(extChartAt I x) : M → E) x ∈ frontier (range (↑I : H → E))

Tactic:
Iff.rfl

Premises used: Iff.rfl, ModelWithCorners.IsBoundaryPoint
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
rw :
  (↑(extChartAt I x) : M → E) x ∉ interior (range (↑I : H → E)) →
    (↑(extChartAt I x) : M → E) x ∈ range (↑I : H → E) ∧ (↑(extChartAt I x) : M → E) x ∉ interior (range (↑I : H → E))
⊢ I.IsInteriorPoint x ∨ I.IsBoundaryPoint x

Tactic:
rw [IsInteriorPoint, or_iff_not_imp_left, I.isBoundaryPoint_iff, ← closure_diff_interior,
    I.isClosed_range.closure_eq, mem_diff]

Premises used: ModelWithCorners.IsInteriorPoint, IsClosed.closure_eq, Set.mem_diff, Classical.or_iff_not_imp_left, ModelWithCorners.isClosed_range, closure_diff_interior, ModelWithCorners.isBoundaryPoint_iff
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
⊢ (↑(extChartAt I x) : M → E) x ∉ interior (range (↑I : H → E)) →
    (↑(extChartAt I x) : M → E) x ∈ range (↑I : H → E) ∧ (↑(extChartAt I x) : M → E) x ∉ interior (range (↑I : H → E))

Tactic:
fun h ↦ ⟨mem_range_self _, h⟩

Premises used: Set.mem_range_self, chartAt, PartialEquiv.restr, ModelWithCorners.toPartialEquiv, PartialEquiv.symm, And.intro, PartialEquiv.source, PartialEquiv.toFun, OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
x : M
⊢ (↑(extChartAt I x) : M → E) x ∉ interior (range (↑I : H → E)) →
    (↑(extChartAt I x) : M → E) x ∈ range (↑I : H → E) ∧ (↑(extChartAt I x) : M → E) x ∉ interior (range (↑I : H → E))

Tactic:
exact fun h ↦ ⟨mem_range_self _, h⟩
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
⊢ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∪
      ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M =
    univ

Tactic:
eq_univ_of_forall fun x => (mem_union _ _ _).mpr (I.isInteriorPoint_or_isBoundaryPoint x)

Premises used: Set.mem_union, Iff.mpr, ModelWithCorners.isInteriorPoint_or_isBoundaryPoint, ModelWithCorners.interior, Set.eq_univ_of_forall, ModelWithCorners.boundary
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
by_contra :
  ∀
    (h :
      ¬Disjoint (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
          (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)),
    False
⊢ Disjoint (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
    (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)

Tactic:
by_contra h