case Adj.h.h.a
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ Adj (hasse (α × β)) x y ↔ Adj (hasse α □ hasse β) x y
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
⊢ hasse (α × β) = hasse α □ hasse β
ext (x y)
no goals
case Adj.h.h.a
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
x y : α × β
⊢ Adj (hasse (α × β)) x y ↔ Adj (hasse α □ hasse β) x y
simp_rw [boxProd_adj, hasse_adj, Prod.covby_iff, or_and_right, @eq_comm _ y.1, @eq_comm _ y.2,
  or_or_or_comm]