-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
/-- The boundary of `M × N` is `∂M × N ∪ (M × ∂N)`. -/
lemma boundary_prod :
    (I.prod J).boundary (M × N) = Set.prod univ (J.boundary N) ∪ Set.prod (I.boundary M) univ

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
⊢ (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ =
    (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ

Tactic:
rw [compl_prod_eq_union]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
h : ModelWithCorners.boundary (M × N) =
  (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ :=
  Trans.trans
    (Trans.trans (Trans.trans rfl (Eq.symm compl_interior))
      (Eq.mpr
        (id (congrArg (fun _a => _aᶜ = (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ) interior_prod))
        (Eq.refl (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ)))
    (Eq.mpr
      (id
        (congrArg (fun _a => _a = (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ)
          (compl_prod_eq_union (ModelWithCorners.interior M) (ModelWithCorners.interior N))))
      (Eq.refl ((ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ)))
⊢ ModelWithCorners.boundary (M × N) = univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod univ

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

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
h : ModelWithCorners.boundary (M × N) =
  (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ :=
  Trans.trans
    (Trans.trans (Trans.trans rfl (Eq.symm compl_interior))
      (Eq.mpr
        (id (congrArg (fun _a => _aᶜ = (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ) interior_prod))
        (Eq.refl (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ)))
    (Eq.mpr
      (id
        (congrArg (fun _a => _a = (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ)
          (compl_prod_eq_union (ModelWithCorners.interior M) (ModelWithCorners.interior N))))
      (Eq.refl ((ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ)))
⊢ univ ×ˢ ModelWithCorners.boundary N ∪ ModelWithCorners.boundary M ×ˢ univ =
    univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod univ

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
h : ModelWithCorners.boundary (M × N) =
  (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ :=
  Trans.trans
    (Trans.trans (Trans.trans rfl (Eq.symm compl_interior))
      (Eq.mpr
        (id (congrArg (fun _a => _aᶜ = (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ) interior_prod))
        (Eq.refl (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ)))
    (Eq.mpr
      (id
        (congrArg (fun _a => _a = (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ)
          (compl_prod_eq_union (ModelWithCorners.interior M) (ModelWithCorners.interior N))))
      (Eq.refl ((ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ)))
⊢ univ ×ˢ ModelWithCorners.boundary N ∪ ModelWithCorners.boundary M ×ˢ univ =
    univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod univ

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
⊢ (ModelWithCorners.interior (M × N))ᶜ = (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ

Tactic:
rw [interior_prod]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
⊢ ModelWithCorners.boundary (M × N) = univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod univ

Tactic:
let h := calc (I.prod J).boundary (M × N)
  _ = ((I.prod J).interior (M × N))ᶜ := compl_interior.symm
  _ = ((I.interior M) ×ˢ (J.interior N))ᶜ := by rw [interior_prod]
  _ = (I.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (J.interior N)ᶜ := by rw [compl_prod_eq_union]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
h : ModelWithCorners.boundary (M × N) =
  (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ :=
  Trans.trans
    (Trans.trans (Trans.trans rfl (Eq.symm compl_interior))
      (Eq.mpr
        (id (congrArg (fun _a => _aᶜ = (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ) interior_prod))
        (Eq.refl (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ)))
    (Eq.mpr
      (id
        (congrArg (fun _a => _a = (ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ)
          (compl_prod_eq_union (ModelWithCorners.interior M) (ModelWithCorners.interior N))))
      (Eq.refl ((ModelWithCorners.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (ModelWithCorners.interior N)ᶜ)))
⊢ ModelWithCorners.boundary (M × N) = univ.prod (ModelWithCorners.boundary N) ∪ (ModelWithCorners.boundary M).prod univ