awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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'))
h :
  Membership.mem (γ := Set (M × N))
      (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) p →
    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
⊢ Membership.mem (γ := Set (M × N))
      (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) p ↔
    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
have h₁ : 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 →
  Membership.mem (γ := Set (M × N))
    (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
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 :
  Membership.mem (γ := Set (M × N))
    (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) p
⊢ 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
have hp₁ : (I.prod J).IsInteriorPoint p
Tactic: replace hp : (I.prod J).IsInteriorPoint p := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
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 : (I.prod J).IsInteriorPoint p
⊢ 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
have hp₁ : (↑(extChartAt (I.prod J) p) : M × N → E × E') p ∈ interior (range (↑I : H → E)) ×ˢ interior (range (↑J : H' → E'))
Tactic: rw [IsInteriorPoint, ← aux] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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
⊢ Membership.mem (γ := Set (M × N))
    (ModelWithCorners.interior (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) p
have h : (I.prod J).IsInteriorPoint p
Tactic: change (I.prod J).IsInteriorPoint p
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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
⊢ (I.prod J).IsInteriorPoint p
have h : ((↑(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: rw [IsInteriorPoint, ← aux, mem_prod]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
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
⊢ ((↑(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'))
have h : p.1 ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∧
  p.2 ∈ ModelWithCorners.interior.{u_1, u_5, u_6, u_7} (𝕜 := 𝕜) (E := E') (H := H') (I := J) N
Tactic: obtain h := Set.mem_prod.mp hp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
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 :
  p.1 ∈ ModelWithCorners.interior.{u_1, u_2, u_3, u_4} (𝕜 := 𝕜) (E := E) (H := H) (I := I) M ∧
    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'))
have 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
Tactic: rw [ModelWithCorners.interior] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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'
⊢ (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)ᶜ
have 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)ᶜ
Tactic: rw [interior_prod]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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'
⊢ (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)ᶜ
have 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)ᶜ
Tactic: rw [compl_prod_eq_union]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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)ᶜ :=
  ⋯
⊢ 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
have 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
Tactic: rw [h, I.compl_interior, J.compl_interior, union_comm]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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)) (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))
have 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))
Tactic: rw [boundary_prod, Boundaryless.boundary_eq_empty (I := I)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
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 (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))
have this : Eq (α := Set (M × N)) (Set.prod ∅ univ) ∅
Tactic: have : Set.prod (∅ : Set M) (univ : Set N) = ∅ := Set.empty_prod
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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) ∅
⊢ 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))
have 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))
Tactic: rw [this, union_empty]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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))
⊢ 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))
have 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))
Tactic: rw [this, union_empty]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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)) (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)
have 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)
Tactic: rw [boundary_prod, Boundaryless.boundary_eq_empty (I := J)]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (hypothesis)
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 ∅ ∪ (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)
have this : Eq (α := Set (M × N)) (Set.prod univ ∅) ∅
Tactic: have : Set.prod (univ : Set M) (∅ : Set N) = ∅ := Set.prod_empty
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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 ∅) ∅
⊢ 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)
have 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)
Tactic: rw [this, empty_union]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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)
⊢ 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)
have 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)
Tactic: rw [this, empty_union]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary (goal)
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
⊢ BoundarylessManifold (I.prod J) (M × N)
have h : Eq (α := Set (M × N)) (ModelWithCorners.boundary (𝕜 := 𝕜) (E := E × E') (H := ModelProd H H') (I := I.prod J) (M × N)) ∅
Tactic: apply Boundaryless.of_boundary_eq_empty