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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux :
  interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
hp :
  p ∈
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
      ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
h :
  Membership.mem (γ := Set M) {x : M | I.IsInteriorPoint x} p.1 ∧
    p.2 ∈ ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
⊢ ((↑(extChartAt (I.prod J) p) : M × N → E × E') p).1 ∈ interior (range (↑I : H → E)) ∧
    ((↑(extChartAt (I.prod J) p) : M × N → E × E') p).2 ∈ interior (range (↑J : H' → E'))

Tactic:
h

Premises used: ModelWithCorners.IsInteriorPoint, Set.Mem, ModelWithCorners.interior, setOf, Set.sUnion, ModelWithCorners.toFun', 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
p : M × N
aux :
  interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E')) =
    interior (range (↑(I.prod J) : ModelProd H H' → E × E'))
hp :
  p ∈
    ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
      ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
h :
  Membership.mem (γ := Set M) {x : M | I.IsInteriorPoint x} p.1 ∧
    p.2 ∈ ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
⊢ ((↑(extChartAt (I.prod J) p) : M × N → E × E') p).1 ∈ interior (range (↑I : H → E)) ∧
    ((↑(extChartAt (I.prod J) p) : M × N → E × E') p).2 ∈ interior (range (↑J : H' → E'))

Tactic:
exact 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
rw rw₁ :
  (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
        ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N)ᶜ =
    (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
        ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N)ᶜ
⊢ (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N))ᶜ =
    (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
        ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N)ᶜ

Tactic:
rw [interior_prod]

Premises used: ModelWithCorners.interior_prod
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
rw rw₁ :
  SProd.sprod (β := Set N) (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ
        univ ∪
      SProd.sprod (α := Set M) univ
        (ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N)ᶜ =
    SProd.sprod (β := Set N) (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ
        univ ∪
      SProd.sprod (α := Set M) univ
        (ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N)ᶜ
⊢ (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ×ˢ
        ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N)ᶜ =
    SProd.sprod (β := Set N) (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ
        univ ∪
      SProd.sprod (α := Set M) univ
        (ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N)ᶜ

Tactic:
rw [compl_prod_eq_union]

Premises used: Set.compl_prod_eq_union
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
h : ModelWithCorners.boundary (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N) =
  SProd.sprod (β := Set N) (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ
      univ ∪
    SProd.sprod (α := Set M) univ
      (ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N)ᶜ :=
  ⋯
rw :
  SProd.sprod (α := Set M) univ
        (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N) ∪
      SProd.sprod (β := Set N) (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
        univ =
    Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N) ∪
      (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ
⊢ ModelWithCorners.boundary (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N) =
    Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N) ∪
      (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ

Tactic:
rw [h, I.compl_interior, J.compl_interior, union_comm]

Premises used: Set.union_comm, 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
h : ModelWithCorners.boundary (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N) =
  SProd.sprod (β := Set N) (ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)ᶜ
      univ ∪
    SProd.sprod (α := Set M) univ
      (ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N)ᶜ :=
  ⋯
⊢ SProd.sprod (α := Set M) univ
        (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N) ∪
      SProd.sprod (β := Set N) (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M)
        univ =
    Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N) ∪
      (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ

Tactic:
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
inst_11 : BoundarylessManifold I M
rw :
  Eq (α := Set (M × N))
    (Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N) ∪
      Set.prod ∅ univ)
    (Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N))
⊢ Eq (α := Set (M × N)) (ModelWithCorners.boundary (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N))
    (Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N))

Tactic:
rw [boundary_prod, Boundaryless.boundary_eq_empty (I := I)]

Premises used: ModelWithCorners.Boundaryless.boundary_eq_empty, ModelWithCorners.boundary_prod
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
inst_11 : BoundarylessManifold I M
⊢ Eq (α := Set (M × N)) (Set.prod ∅ univ) ∅

Tactic:
have : Set.prod (∅ : Set M) (univ : Set N) = ∅ := Set.empty_prod
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
inst_11 : BoundarylessManifold I M
this : Eq (α := Set (M × N)) (Set.prod ∅ univ) ∅
rw :
  Eq (α := Set (M × N))
    (Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N) ∪ ∅)
    (Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N))
rw₁ rw₂ :
  Eq (α := Set (M × N))
    (Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N))
    (Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N))
⊢ Eq (α := Set (M × N))
    (Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N) ∪
      Set.prod ∅ univ)
    (Set.prod univ (ModelWithCorners.boundary.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N))

Tactic:
rw [this, union_empty]

Premises used: Set.union_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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
inst_11 : BoundarylessManifold J N
rw :
  Eq (α := Set (M × N))
    (Set.prod univ ∅ ∪ (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ)
    ((ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ)
⊢ Eq (α := Set (M × N)) (ModelWithCorners.boundary (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N))
    ((ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ)

Tactic:
rw [boundary_prod, Boundaryless.boundary_eq_empty (I := J)]

Premises used: ModelWithCorners.Boundaryless.boundary_eq_empty, ModelWithCorners.boundary_prod
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
inst_11 : BoundarylessManifold J N
⊢ Eq (α := Set (M × N)) (Set.prod univ ∅) ∅

Tactic:
have : Set.prod (univ : Set M) (∅ : Set N) = ∅ := Set.prod_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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
inst_11 : BoundarylessManifold J N
this : Eq (α := Set (M × N)) (Set.prod univ ∅) ∅
rw :
  Eq (α := Set (M × N))
    (∅ ∪ (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ)
    ((ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ)
rw₁ rw₂ :
  Eq (α := Set (M × N))
    ((ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ)
    ((ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ)
⊢ Eq (α := Set (M × N))
    (Set.prod univ ∅ ∪ (ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ)
    ((ModelWithCorners.boundary.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M).prod univ)

Tactic:
rw [this, empty_union]

Premises used: Set.empty_union
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
x : M
y : N
inst_11 : BoundarylessManifold I M
inst_12 : BoundarylessManifold J N
h :
  Eq (α := Set (M × N)) (ModelWithCorners.boundary (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N))
    ∅
⊢ BoundarylessManifold (I.prod J) (M × N)

Tactic:
apply Boundaryless.of_boundary_eq_empty

Premises used: ModelWithCorners.Boundaryless.of_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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
x : M
y : N
inst_11 : BoundarylessManifold I M
inst_12 : BoundarylessManifold J N
h : Eq (α := Set (M × N)) (Set.prod univ ∅) ∅ ∧ Eq (α := Set (M × N)) (Set.prod ∅ univ) ∅
⊢ Eq (α := Set (M × N)) (ModelWithCorners.boundary (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N))
    ∅

Tactic:
simp only [boundary_prod, Boundaryless.boundary_eq_empty, union_empty_iff]

Premises used: Set.union_empty_iff, ModelWithCorners.Boundaryless.boundary_eq_empty, ModelWithCorners.boundary_prod
-- 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
x : M
y : N
inst_11 : BoundarylessManifold I M
inst_12 : BoundarylessManifold J N
⊢ Eq (α := Set (M × N)) (Set.prod univ ∅) ∅ ∧ Eq (α := Set (M × N)) (Set.prod ∅ univ) ∅

Tactic:
⟨Set.prod_empty, Set.empty_prod⟩

Premises used: Set.empty_prod, Set.prod_empty, 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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
N : Type u_7
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
x : M
y : N
inst_11 : BoundarylessManifold I M
inst_12 : BoundarylessManifold J N
⊢ Eq (α := Set (M × N)) (Set.prod univ ∅) ∅ ∧ Eq (α := Set (M × N)) (Set.prod ∅ univ) ∅

Tactic:
exact ⟨Set.prod_empty, Set.empty_prod⟩
-- 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
rw :
  (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
      (Sum.inl x) ∈
    interior
      (PartialEquiv.target (α := M ⊕ M')
        (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I))
⊢ I.IsInteriorPoint (M := M ⊕ M') (Sum.inl x)

Tactic:
rw [I.isInteriorPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inl]

Premises used: extChartAt, ChartedSpace.sum_chartAt_inl, 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
dsimp :
  (↑I : H → E) (extend Sum.inl (↑(chartAt H x) : M → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inl x)) ∈
    interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
⊢ (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
      (Sum.inl x) ∈
    interior
      (PartialEquiv.target (α := M ⊕ M')
        (OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I))

Tactic:
dsimp
-- 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
rw :
  (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)
⊢ (↑I : H → E) (extend Sum.inl (↑(chartAt H x) : M → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inl x)) ∈
    interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)

Tactic:
rw [Sum.inl_injective.extend_apply (chartAt H x)]

Premises used: chartAt, Sum.inl_injective, OpenPartialHomeomorph.toFun', Function.Injective.extend_apply
-- 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsInteriorPoint x
⊢ (↑I : H → E) ((↑(chartAt H x) : M → H) x) ∈
    interior (I.target ∩ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target)

Tactic:
simpa [I.isInteriorPoint_iff, extChartAt] using hx

Premises used: extChartAt, 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
rw :
  (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
      (Sum.inl x) ∈
    frontier (range (↑I : H → E))
⊢ I.IsBoundaryPoint (M := M ⊕ M') (Sum.inl x)

Tactic:
rw [I.isBoundaryPoint_iff, extChartAt, ChartedSpace.sum_chartAt_inl]

Premises used: extChartAt, ChartedSpace.sum_chartAt_inl, 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
M' : Type u_5
inst_6 : TopologicalSpace M'
inst_7 : ChartedSpace H M'
x : M
hx : I.IsBoundaryPoint x
dsimp :
  (↑I : H → E) (extend Sum.inl (↑(chartAt H x) : M → H) (fun (x_1 : M ⊕ M') ↦ Classical.arbitrary H) (Sum.inl x)) ∈
    frontier (range (↑I : H → E))
⊢ (↑(OpenPartialHomeomorph.extend (OpenPartialHomeomorph.lift_openEmbedding (chartAt H x) ⋯) I) : M ⊕ M' → E)
      (Sum.inl x) ∈
    frontier (range (↑I : H → E))

Tactic:
dsimp