-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
/-- If `M` is boundaryless, `∂(M×N) = M × ∂N`. -/
lemma boundary_of_boundaryless_left [BoundarylessManifold I M] :
    (I.prod J).boundary (M × N) = Set.prod (univ : Set M) (J.boundary N)

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'
inst✝ : BoundarylessManifold I M
this : ∅.prod univ = ∅
⊢ univ.prod (ModelWithCorners.boundary N) ∪ ∅.prod univ = univ.prod (ModelWithCorners.boundary N)

Tactic:
rw [this, union_empty]

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'
inst✝ : BoundarylessManifold I M
⊢ ModelWithCorners.boundary (M × N) = univ.prod (ModelWithCorners.boundary N)

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

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'
inst✝ : BoundarylessManifold I M
⊢ univ.prod (ModelWithCorners.boundary N) ∪ ∅.prod univ = univ.prod (ModelWithCorners.boundary N)

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'
inst✝ : BoundarylessManifold I M
⊢ univ.prod (ModelWithCorners.boundary N) ∪ ∅.prod univ = univ.prod (ModelWithCorners.boundary N)

Tactic:
have : Set.prod (∅ : Set M) (univ : Set N) = ∅ := Set.empty_prod

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'
inst✝ : BoundarylessManifold I M
this : ∅.prod univ = ∅
⊢ univ.prod (ModelWithCorners.boundary N) ∪ ∅.prod univ = univ.prod (ModelWithCorners.boundary N)