[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c : α
h : a ≤ b
⊢ ¬a ⩿ b ↔ ∃ c, a < c ∧ c < b
[PROOFSTEP]
simp_rw [Wcovby, h, true_and_iff, not_forall, exists_prop, not_not]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c : α
⊢ (∀ ⦃c : α⦄, a < c → ¬c < b) ↔ Ioo a b = ∅
[PROOFSTEP]
simp [eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected (range ↑f)
⊢ ↑f a ⩿ ↑f b
[PROOFSTEP]
refine' ⟨f.monotone hab.le, fun c ha hb => _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c✝ : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected (range ↑f)
c : (fun x => β) a
ha : ↑f a < c
hb : c < ↑f b
⊢ False
[PROOFSTEP]
obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c✝ : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected (range ↑f)
c : α
ha : ↑f a < ↑f c
hb : ↑f c < ↑f b
⊢ False
[PROOFSTEP]
rw [f.lt_iff_lt] at ha hb 
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c✝ : α
f : α ↪o β
hab : a ⩿ b
h : OrdConnected (range ↑f)
c : α
ha : a < c
hb : c < b
⊢ False
[PROOFSTEP]
exact hab.2 ha hb
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2 : a ≤ c
h3 : c ≤ b
⊢ c = a ∨ c = b
[PROOFSTEP]
rcases h2.eq_or_lt with (h2 | h2)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a = c
⊢ c = a ∨ c = b
[PROOFSTEP]
exact Or.inl h2.symm
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3 : c ≤ b
h2 : a < c
⊢ c = a ∨ c = b
[PROOFSTEP]
rcases h3.eq_or_lt with (h3 | h3)
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c = b
⊢ c = a ∨ c = b
[PROOFSTEP]
exact Or.inr h3
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
h2✝ : a ≤ c
h3✝ : c ≤ b
h2 : a < c
h3 : c < b
⊢ c = a ∨ c = b
[PROOFSTEP]
exact (h.2 h2 h3).elim
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b
[PROOFSTEP]
refine' ⟨fun h2 => h.eq_or_eq h2.1 h2.2, _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ c = a ∨ c = b → a ≤ c ∧ c ≤ b
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
b c : α
h : c ⩿ b
⊢ c ≤ c ∧ c ≤ b
case inr α : Type u_1 β : Type u_2 inst✝ : PartialOrder α a c : α h : a ⩿ c ⊢ a ≤ c ∧ c ≤ c
[PROOFSTEP]
exacts [⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ Icc a b = {a, b}
[PROOFSTEP]
ext c
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c✝ : α
h : a ⩿ b
c : α
⊢ c ∈ Icc a b ↔ c ∈ {a, b}
[PROOFSTEP]
exact h.le_and_le_iff
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ Ico a b ⊆ {a}
[PROOFSTEP]
rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ Ioc a b ⊆ {b}
[PROOFSTEP]
rw [← Icc_diff_left, h.Icc_eq, diff_singleton_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LT α
a b : α
h : a < b
⊢ ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b
[PROOFSTEP]
simp_rw [Covby, h, true_and_iff, not_forall, exists_prop, not_not]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a b c : α
⊢ (∀ ⦃c : α⦄, a < c → ¬c < b) ↔ Ioo a b = ∅
[PROOFSTEP]
simp [eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
⊢ a ⩿ b ↔ a ⋖ b ∨ a = b
[PROOFSTEP]
rw [le_antisymm_iff, wcovby_iff_covby_or_le_and_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⋖ b
⊢ Ico a b = {a}
[PROOFSTEP]
rw [← Ioo_union_left h.lt, h.Ioo_eq, empty_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
a b c : α
h : a ⋖ b
⊢ Ioc a b = {b}
[PROOFSTEP]
rw [← Ioo_union_right h.lt, h.Ioo_eq, empty_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b c : α
h : a ⋖ b
⊢ Ioi a = Ici b
[PROOFSTEP]
rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b c : α
h : a ⋖ b
⊢ Iio b = Iic a
[PROOFSTEP]
rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b c : α
h : a < b
⊢ ∃ a', a' > a ∧ ∃ b', b' < b ∧ ∀ (x : α), x < a' → ∀ (y : α), y > b' → x < y
[PROOFSTEP]
by_cases h' : a ⋖ b
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b c : α
h : a < b
h' : a ⋖ b
⊢ ∃ a', a' > a ∧ ∃ b', b' < b ∧ ∀ (x : α), x < a' → ∀ (y : α), y > b' → x < y
[PROOFSTEP]
exact ⟨b, h, a, h, fun x hx y hy => hx.trans_le <| h'.ge_of_gt hy⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b c : α
h : a < b
h' : ¬a ⋖ b
⊢ ∃ a', a' > a ∧ ∃ b', b' < b ∧ ∀ (x : α), x < a' → ∀ (y : α), y > b' → x < y
[PROOFSTEP]
rcases h.exists_lt_lt h' with ⟨c, ha, hb⟩
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b c✝ : α
h : a < b
h' : ¬a ⋖ b
c : α
ha : a < c
hb : c < b
⊢ ∃ a', a' > a ∧ ∃ b', b' < b ∧ ∀ (x : α), x < a' → ∀ (y : α), y > b' → x < y
[PROOFSTEP]
exact ⟨c, ha, c, hb, fun _ h₁ _ => lt_trans h₁⟩
[GOAL]
α : Type u_1
β : Type u_2
x : α
s : Set α
⊢ s ⩿ insert x s
[PROOFSTEP]
refine' wcovby_of_eq_or_eq (subset_insert x s) fun t hst h2t => _
[GOAL]
α : Type u_1
β : Type u_2
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
⊢ t = s ∨ t = insert x s
[PROOFSTEP]
by_cases h : x ∈ t
[GOAL]
case pos
α : Type u_1
β : Type u_2
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : x ∈ t
⊢ t = s ∨ t = insert x s
[PROOFSTEP]
exact Or.inr (subset_antisymm h2t <| insert_subset_iff.mpr ⟨h, hst⟩)
[GOAL]
case neg
α : Type u_1
β : Type u_2
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : ¬x ∈ t
⊢ t = s ∨ t = insert x s
[PROOFSTEP]
refine' Or.inl (subset_antisymm _ hst)
[GOAL]
case neg
α : Type u_1
β : Type u_2
x : α
s t : Set α
hst : s ≤ t
h2t : t ≤ insert x s
h : ¬x ∈ t
⊢ t ⊆ s
[PROOFSTEP]
rwa [← diff_singleton_eq_self h, diff_singleton_subset_iff]
[GOAL]
α : 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
[PROOFSTEP]
refine' fun h => of_not_not fun hab => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x ⩿ y
hab : ¬(x.fst = y.fst ∨ x.snd = y.snd)
⊢ False
[PROOFSTEP]
push_neg at hab 
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x ⩿ y
hab : x.fst ≠ y.fst ∧ x.snd ≠ y.snd
⊢ False
[PROOFSTEP]
exact h.2 (mk_lt_mk.2 <| Or.inl ⟨hab.1.lt_of_le h.1.1, le_rfl⟩) (mk_lt_mk.2 <| Or.inr ⟨le_rfl, hab.2.lt_of_le h.1.2⟩)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂
[PROOFSTEP]
refine' ⟨Wcovby.fst, (And.imp mk_le_mk_iff_left.2) fun h c h₁ h₂ => _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
⊢ False
[PROOFSTEP]
have : c.2 = b := h₂.le.2.antisymm h₁.le.2
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : (a₁, b) < c
h₂ : c < (a₂, b)
this : c.snd = b
⊢ False
[PROOFSTEP]
rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂ 
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : ∀ ⦃c : α⦄, a₁ < c → ¬c < a₂
c : α × β
h₁ : a₁ < c.fst
h₂ : c.fst < a₂
this : c.snd = b
⊢ False
[PROOFSTEP]
exact h h₁ h₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂
[PROOFSTEP]
simp_rw [covby_iff_wcovby_and_lt, mk_wcovby_mk_iff_left, mk_lt_mk_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂
[PROOFSTEP]
simp_rw [covby_iff_wcovby_and_lt, mk_wcovby_mk_iff_right, mk_lt_mk_iff_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : (a₁, b₁) ⩿ (a₂, b₂)
⊢ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂
[PROOFSTEP]
obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovby h
[GOAL]
case refine'_1.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ : α
b b₁ b₂ : β
x y : α × β
h : (a₁, b₁) ⩿ (a₁, b₂)
⊢ a₁ ⩿ a₁ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₁
[PROOFSTEP]
exact Or.inr ⟨mk_wcovby_mk_iff_right.1 h, rfl⟩
[GOAL]
case refine'_1.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ : β
x y : α × β
h : (a₁, b₁) ⩿ (a₂, b₁)
⊢ a₁ ⩿ a₂ ∧ b₁ = b₁ ∨ b₁ ⩿ b₁ ∧ a₁ = a₂
[PROOFSTEP]
exact Or.inl ⟨mk_wcovby_mk_iff_left.1 h, rfl⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⩿ (a₂, b₂)
[PROOFSTEP]
rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
[GOAL]
case refine'_2.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ : β
x y : α × β
h : a₁ ⩿ a₂
⊢ (a₁, b₁) ⩿ (a₂, b₁)
[PROOFSTEP]
exact mk_wcovby_mk_iff_left.2 h
[GOAL]
case refine'_2.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ : α
b b₁ b₂ : β
x y : α × β
h : b₁ ⩿ b₂
⊢ (a₁, b₁) ⩿ (a₁, b₂)
[PROOFSTEP]
exact mk_wcovby_mk_iff_right.2 h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : (a₁, b₁) ⋖ (a₂, b₂)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂
[PROOFSTEP]
obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovby h.wcovby
[GOAL]
case refine'_1.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ : α
b b₁ b₂ : β
x y : α × β
h : (a₁, b₁) ⋖ (a₁, b₂)
⊢ a₁ ⋖ a₁ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₁
[PROOFSTEP]
exact Or.inr ⟨mk_covby_mk_iff_right.1 h, rfl⟩
[GOAL]
case refine'_1.inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ : β
x y : α × β
h : (a₁, b₁) ⋖ (a₂, b₁)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₁ ∨ b₁ ⋖ b₁ ∧ a₁ = a₂
[PROOFSTEP]
exact Or.inl ⟨mk_covby_mk_iff_left.1 h, rfl⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)
[PROOFSTEP]
rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
[GOAL]
case refine'_2.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ : β
x y : α × β
h : a₁ ⋖ a₂
⊢ (a₁, b₁) ⋖ (a₂, b₁)
[PROOFSTEP]
exact mk_covby_mk_iff_left.2 h
[GOAL]
case refine'_2.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ : α
b b₁ b₂ : β
x y : α × β
h : b₁ ⋖ b₂
⊢ (a₁, b₁) ⋖ (a₁, b₂)
[PROOFSTEP]
exact mk_covby_mk_iff_right.2 h
[GOAL]
α : 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
[PROOFSTEP]
cases x
[GOAL]
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
[PROOFSTEP]
cases y
[GOAL]
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
[PROOFSTEP]
exact mk_wcovby_mk_iff
[GOAL]
α : 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
[PROOFSTEP]
cases x
[GOAL]
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
[PROOFSTEP]
cases y
[GOAL]
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
[PROOFSTEP]
exact mk_covby_mk_iff
