feat(combinatorics/simple_graph/hasse): The Hasse diagram of α × β (#14978)

... is the box product of the Hasse diagrams of `α` and `β`.

Author: YaelDillies

src/combinatorics/simple_graph/hasse.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import combinatorics.simple_graph.connectivity
+import combinatorics.simple_graph.prod
 import data.fin.succ_pred
 import order.succ_pred.relation
 
@@ -47,6 +47,15 @@ def hasse_dual_iso : hasse αᵒᵈ ≃g hasse α :=
 
 end preorder
 
+section partial_order
+variables [partial_order α] [partial_order β]
+
+@[simp] lemma hasse_prod : hasse (α × β) = hasse α □ hasse β :=
+by { ext x y, simp_rw [box_prod_adj, hasse_adj, prod.covby_iff, or_and_distrib_right,
+  @eq_comm _ y.1, @eq_comm _ y.2, or_or_or_comm] }
+
+end partial_order
+
 section linear_order
 variables [linear_order α]
 

src/combinatorics/simple_graph/prod.lean

@@ -41,8 +41,8 @@ def box_prod (G : simple_graph α) (H : simple_graph β) : simple_graph (α × 
 
 infix ` □ `:70 := box_prod
 
-lemma box_prod_adj : (G □ H).adj x y ↔ G.adj x.1 y.1 ∧ x.2 = y.2 ∨ H.adj x.2 y.2 ∧ x.1 = y.1 :=
-iff.rfl
+@[simp] lemma box_prod_adj :
+  (G □ H).adj x y ↔ G.adj x.1 y.1 ∧ x.2 = y.2 ∨ H.adj x.2 y.2 ∧ x.1 = y.1 := iff.rfl
 
 @[simp] lemma box_prod_adj_left : (G □ H).adj (a₁, b) (a₂, b) ↔ G.adj a₁ a₂ :=
 by rw [box_prod_adj, and_iff_left rfl, or_iff_left (λ h : H.adj b b ∧ _, h.1.ne rfl)]