awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
obtain :
  ∀ (x : M) (h1 : x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
    (h2 : x ∈ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M), False
⊢ False

Tactic:
obtain ⟨x, h1, h2⟩ := not_disjoint_iff.mp h

Premises used: Set.not_disjoint_iff, Iff.mp
-- 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
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)
x : M
h1 : x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
h2 : x ∈ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
rw :
  (↑(extChartAt I x) : M → E) x ∈ interior (range (↑I : H → E)) ∧
    (↑(extChartAt I x) : M → E) x ∈ frontier (range (↑I : H → E))
rw₁ : Set E
⊢ False

Tactic:
rw [← mem_empty_iff_false (extChartAt I x x),
    ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff]

Premises used: extChartAt, disjoint_interior_frontier, Set.mem_inter_iff, Set.disjoint_iff_inter_eq_empty, Iff.mp, Set.mem_empty_iff_false, PartialEquiv.toFun
-- 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
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)
x : M
h1 : x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
h2 : x ∈ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
⊢ (↑(extChartAt I x) : M → E) x ∈ interior (range (↑I : H → E)) ∧
    (↑(extChartAt I x) : M → E) x ∈ frontier (range (↑I : H → E))

Tactic:
⟨h1, h2⟩

Premises used: And.intro
-- 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 → I.IsInteriorPoint x

Tactic:
simpa only [or_iff_not_imp_right] using isInteriorPoint_or_isBoundaryPoint x (I := I)

Premises used: ModelWithCorners.isInteriorPoint_or_isBoundaryPoint, Classical.or_iff_not_imp_right
-- 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
refine : I.IsInteriorPoint x → ¬I.IsBoundaryPoint x
⊢ I.IsInteriorPoint x ↔ ¬I.IsBoundaryPoint x

Tactic:
refine ⟨?_,
    by simpa only [or_iff_not_imp_right] using isInteriorPoint_or_isBoundaryPoint x (I := I)⟩
-- 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
by_contra! : ∀ (h : I.IsInteriorPoint x ∧ I.IsBoundaryPoint x), False
⊢ I.IsInteriorPoint x → ¬I.IsBoundaryPoint x

Tactic:
by_contra! 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
x : M
h : I.IsInteriorPoint x ∧ I.IsBoundaryPoint x
rw :
  (↑(extChartAt I x) : M → E) x ∈ interior (range (↑I : H → E)) ∧
    (↑(extChartAt I x) : M → E) x ∈ frontier (range (↑I : H → E))
rw₁ : Set E
⊢ False

Tactic:
rw [← mem_empty_iff_false (extChartAt I x x),
    ← disjoint_iff_inter_eq_empty.mp disjoint_interior_frontier, mem_inter_iff]

Premises used: extChartAt, disjoint_interior_frontier, Set.mem_inter_iff, Set.disjoint_iff_inter_eq_empty, Iff.mp, Set.mem_empty_iff_false, PartialEquiv.toFun
-- 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
h : I.IsInteriorPoint x ∧ I.IsBoundaryPoint x
⊢ (↑(extChartAt I x) : M → E) x ∈ interior (range (↑I : H → E)) ∧
    (↑(extChartAt I x) : M → E) x ∈ frontier (range (↑I : H → E))

Tactic:
h

Premises used: ModelWithCorners.IsInteriorPoint, 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
⊢ I.IsBoundaryPoint x ↔ ¬I.IsInteriorPoint x

Tactic:
simp [isInteriorPoint_iff_not_isBoundaryPoint]

Premises used: ModelWithCorners.isInteriorPoint_iff_not_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
apply :
  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 =
    ⊥
⊢ (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:
apply compl_unique ?_ I.interior_union_boundary_eq_univ

Premises used: ModelWithCorners.interior_union_boundary_eq_univ, compl_unique
-- 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 =
    ⊥

Tactic:
disjoint_iff_inter_eq_empty.mp I.disjoint_interior_boundary

Premises used: Set.disjoint_iff_inter_eq_empty, Iff.mp, ModelWithCorners.disjoint_interior_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
⊢ 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:
exact disjoint_iff_inter_eq_empty.mp I.disjoint_interior_boundary

Premises used: Set.disjoint_iff_inter_eq_empty, Iff.mp, ModelWithCorners.disjoint_interior_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
rw :
  (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜᶜ =
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
rw₁ rw₂ :
  ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) 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)ᶜ =
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M

Tactic:
rw [← compl_interior, compl_compl]

Premises used: compl_compl, ModelWithCorners.compl_interior
-- 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
h : I.IsInteriorPoint x
rw :
  ∃ t ⊆ range (↑I : H → E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑(extChartAt I x) : M → E) x ∈ t
⊢ range (↑I : H → E) ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [mem_nhds_iff]

Premises used: mem_nhds_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
h : I.IsInteriorPoint x
⊢ ∃ t ⊆ range (↑I : H → E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑(extChartAt I x) : M → E) x ∈ t

Tactic:
⟨interior (range I), interior_subset, isOpen_interior, h⟩

Premises used: interior_subset, isOpen_interior, ModelWithCorners.toFun', And.intro, interior, Exists.intro, Set.range
-- 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
h : I.IsInteriorPoint x
⊢ ∃ t ⊆ range (↑I : H → E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∧ (↑(extChartAt I x) : M → E) x ∈ t

Tactic:
exact ⟨interior (range I), interior_subset, isOpen_interior, 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
inst_6 : I.Boundaryless
x : M
r : interior (OpenPartialHomeomorph.extend (chartAt H x) I).target =
  (OpenPartialHomeomorph.extend (chartAt H x) I).target :=
  ⋯
⊢ extChartAt I x = OpenPartialHomeomorph.extend (chartAt H x) I

Tactic:
have : extChartAt I x = (chartAt H x).extend I := rfl
-- 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
inst_6 : I.Boundaryless
x : M
r : interior (OpenPartialHomeomorph.extend (chartAt H x) I).target =
  (OpenPartialHomeomorph.extend (chartAt H x) I).target :=
  ⋯
this : extChartAt I x = OpenPartialHomeomorph.extend (chartAt H x) I
⊢ interior (extChartAt I x).target = (extChartAt I x).target

Tactic:
rw [← this] at r
-- 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
inst_6 : I.Boundaryless
x : M
r : interior (OpenPartialHomeomorph.extend (chartAt H x) I).target =
  (OpenPartialHomeomorph.extend (chartAt H x) I).target :=
  ⋯
this : extChartAt I x = OpenPartialHomeomorph.extend (chartAt H x) I
r₁ : interior (extChartAt I x).target = (extChartAt I x).target
⊢ extChartAt I x = OpenPartialHomeomorph.extend (chartAt H x) I

Tactic:
rw [← this] at r
-- 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
inst_6 : I.Boundaryless
x : M
r : interior (extChartAt I x).target = (extChartAt I x).target
this : extChartAt I x = OpenPartialHomeomorph.extend (chartAt H x) I
rw : (↑(extChartAt I x) : M → E) x ∈ (extChartAt I x).target
⊢ I.IsInteriorPoint x

Tactic:
rw [isInteriorPoint_iff, r]

Premises used: ModelWithCorners.isInteriorPoint_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
inst_6 : I.Boundaryless
x : M
r : interior (extChartAt I x).target = (extChartAt I x).target
this : extChartAt I x = OpenPartialHomeomorph.extend (chartAt H x) I
⊢ (↑(extChartAt I x) : M → E) x ∈ (extChartAt I x).target

Tactic:
PartialEquiv.map_source _ (mem_extChartAt_source _)

Premises used: PartialEquiv.map_source, mem_extChartAt_source
-- 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
inst_6 : I.Boundaryless
x : M
r : interior (extChartAt I x).target = (extChartAt I x).target
this : extChartAt I x = OpenPartialHomeomorph.extend (chartAt H x) I
⊢ (↑(extChartAt I x) : M → E) x ∈ (extChartAt I x).target

Tactic:
exact PartialEquiv.map_source _ (mem_extChartAt_source _)

Premises used: PartialEquiv.map_source, mem_extChartAt_source
-- 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
inst_6 : BoundarylessManifold I M
⊢ I.IsInteriorPoint x

Tactic:
BoundarylessManifold.isInteriorPoint' x

Premises used: BoundarylessManifold.isInteriorPoint'
-- 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
inst_6 : BoundarylessManifold I M
⊢ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = univ

Tactic:
eq_univ_of_forall fun _ => BoundarylessManifold.isInteriorPoint

Premises used: BoundarylessManifold.isInteriorPoint, Set.eq_univ_of_forall
-- 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
inst_6 : BoundarylessManifold I M
rw : (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ = ∅
rw₁ : Eq.{u_4 + 1} (α := Set M) univᶜ ∅
rw₂ rw₃ : Eq.{u_4 + 1} (α := Set M) univ univ
⊢ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅

Tactic:
rw [← I.compl_interior, I.interior_eq_univ, compl_empty_iff]

Premises used: ModelWithCorners.interior_eq_univ, ModelWithCorners.compl_interior, Set.compl_empty_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
inst_6 : BoundarylessManifold I M
⊢ IsEmpty.{u_4 + 1} (↑(ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M) : Type u_4)

Tactic:
isEmpty_coe_sort.mpr Boundaryless.boundary_eq_empty

Premises used: Iff.mpr, ModelWithCorners.Boundaryless.boundary_eq_empty, Set.isEmpty_coe_sort
-- 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.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅ ↔ BoundarylessManifold I M

Tactic:
⟨fun h ↦ { isInteriorPoint' := ?_ }, fun a ↦ boundary_eq_empty⟩

Premises used: ModelWithCorners.Boundaryless.boundary_eq_empty, BoundarylessManifold.mk, Iff.intro
-- 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
refine :
  ∀ (h : ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅) (x : M),
    I.IsInteriorPoint x
⊢ ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅ ↔ BoundarylessManifold I M

Tactic:
refine ⟨fun h ↦ { isInteriorPoint' := ?_ }, fun a ↦ boundary_eq_empty⟩
-- 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
h : ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅
x : M
rw :
  ∀ (h : ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = univ) (x : M),
    x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M
⊢ x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M

Tactic:
rw [← compl_interior, compl_empty_iff] at h

Premises used: ModelWithCorners.compl_interior, Set.compl_empty_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
h : ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = univ
x : M
rw : Membership.mem (γ := Set M) univ x
⊢ x ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M

Tactic:
rw [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
h : ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = univ
x : M
⊢ Membership.mem (γ := Set M) univ x

Tactic:
trivial
-- 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
h : ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M = ∅
⊢ BoundarylessManifold I M

Tactic:
(Boundaryless.iff_boundary_eq_empty (I := I)).mp h

Premises used: ModelWithCorners.Boundaryless.iff_boundary_eq_empty, Iff.mp
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)
contrapose :
  ∀ (hfx : f x ∉ interior s), ¬Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)
⊢ f x ∈ interior s

Tactic:
contrapose hfx
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
have :
  ∀ (F : StrongDual ℝ H)
    (hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)),
    ¬Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)
⊢ ¬Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)

Tactic:
have ⟨F, hF⟩ := geometric_hahn_banach_open_point hs.interior isOpen_interior hfx
-- Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Goal:
E : Type u_5
H : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup H
inst_3 : NormedSpace ℝ H
f : E → H
x : E
hf : DifferentiableAt ℝ f x
u : Set E
hu : u ∈ 𝓝 x
s : Set H
hs : Convex ℝ s
hs' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs'' : (interior s).Nonempty
hfus : MapsTo f u s
hfx : f x ∉ interior s
F : StrongDual ℝ H
hF : ∀ a ∈ interior s, LT.lt (α := ℝ) ((F : (a : H) → ℝ) a : ℝ) ((F : (a : H) → ℝ) (f x) : ℝ)
h : ∀ (y : E), Eq (α := ℝ) ((F : (a : H) → ℝ) ((fderiv ℝ f x : (a : E) → H) y : H) : ℝ) (0 : ℝ)
have : ∀ (y : H) (hy : y ∈ interior s), ¬Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)
⊢ ¬Surjective.{u_5 + 1, u_6 + 1} (α := E) (β := H) (⇑(fderiv ℝ f x) : (a : E) → H)

Tactic:
have ⟨y, hy⟩ := hs''