no goals
α : Type u_1
β : Type u_2
γ : Type ?u.9064
G : SimpleGraph α
H : SimpleGraph β
a₁ : α
b : β
a₂ : α
⊢ Adj (G □ H) (a₁, b) (a₂, b) ↔ Adj G a₁ a₂
simp only [boxProd_adj, and_true, SimpleGraph.irrefl, false_and, or_false]