case refine'_1
α : Type u_2
β : Type u_1
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₂

case refine'_2
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂
refine' ⟨fun h => _, _⟩
case refine'_1.inl
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ : α
b b₁ b₂ : β
x y : α × β
h : (a₁, b₁) ⋖ (a₁, b₂)
⊢ a₁ ⋖ a₁ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₁

case refine'_1.inr
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ : β
x y : α × β
h : (a₁, b₁) ⋖ (a₂, b₁)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₁ ∨ b₁ ⋖ b₁ ∧ a₁ = a₂
case refine'_1
α : Type u_2
β : Type u_1
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₂
obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovby h.wcovby
no goals
case refine'_1.inl
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ : α
b b₁ b₂ : β
x y : α × β
h : (a₁, b₁) ⋖ (a₁, b₂)
⊢ a₁ ⋖ a₁ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₁
exact Or.inr ⟨mk_covby_mk_iff_right.1 h, rfl⟩
no goals
case refine'_1.inr
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ : β
x y : α × β
h : (a₁, b₁) ⋖ (a₂, b₁)
⊢ a₁ ⋖ a₂ ∧ b₁ = b₁ ∨ b₁ ⋖ b₁ ∧ a₁ = a₂
exact Or.inl ⟨mk_covby_mk_iff_left.1 h, rfl⟩
case refine'_2.inl.intro
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ : β
x y : α × β
h : a₁ ⋖ a₂
⊢ (a₁, b₁) ⋖ (a₂, b₁)

case refine'_2.inr.intro
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ : α
b b₁ b₂ : β
x y : α × β
h : b₁ ⋖ b₂
⊢ (a₁, b₁) ⋖ (a₁, b₂)
case refine'_2
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ → (a₁, b₁) ⋖ (a₂, b₂)
rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
no goals
case refine'_2.inl.intro
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ a₂ : α
b b₁ : β
x y : α × β
h : a₁ ⋖ a₂
⊢ (a₁, b₁) ⋖ (a₂, b₁)
exact mk_covby_mk_iff_left.2 h
no goals
case refine'_2.inr.intro
α : Type u_2
β : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a a₁ : α
b b₁ b₂ : β
x y : α × β
h : b₁ ⋖ b₂
⊢ (a₁, b₁) ⋖ (a₁, b₂)
exact mk_covby_mk_iff_right.2 h