case mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
y : α × β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ⋖ y ↔
    (fst✝, snd✝).fst ⋖ y.fst ∧ (fst✝, snd✝).snd = y.snd ∨ (fst✝, snd✝).snd ⋖ y.snd ∧ (fst✝, snd✝).fst = y.fst
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ x ⋖ y ↔ x.fst ⋖ y.fst ∧ x.snd = y.snd ∨ x.snd ⋖ y.snd ∧ x.fst = y.fst
cases x
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
⊢ (fst✝¹, snd✝¹) ⋖ (fst✝, snd✝) ↔
    (fst✝¹, snd✝¹).fst ⋖ (fst✝, snd✝).fst ∧ (fst✝¹, snd✝¹).snd = (fst✝, snd✝).snd ∨
      (fst✝¹, snd✝¹).snd ⋖ (fst✝, snd✝).snd ∧ (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst
case mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
y : α × β
fst✝ : α
snd✝ : β
⊢ (fst✝, snd✝) ⋖ y ↔
    (fst✝, snd✝).fst ⋖ y.fst ∧ (fst✝, snd✝).snd = y.snd ∨ (fst✝, snd✝).snd ⋖ y.snd ∧ (fst✝, snd✝).fst = y.fst
cases y
no goals
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
fst✝¹ : α
snd✝¹ : β
fst✝ : α
snd✝ : β
⊢ (fst✝¹, snd✝¹) ⋖ (fst✝, snd✝) ↔
    (fst✝¹, snd✝¹).fst ⋖ (fst✝, snd✝).fst ∧ (fst✝¹, snd✝¹).snd = (fst✝, snd✝).snd ∨
      (fst✝¹, snd✝¹).snd ⋖ (fst✝, snd✝).snd ∧ (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst
exact mk_covby_mk_iff