no goals
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂
simp_rw [covby_iff_wcovby_and_lt, mk_wcovby_mk_iff_right, mk_lt_mk_iff_right]