case refine'_1
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

case refine'_2
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ x < y ↔ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
refine' ⟨fun h ↦ _, _⟩
case pos
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
h₁ : y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

case neg
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
case refine'_1
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
by_cases h₁ : y.1 ≤ x.1
no goals
case pos
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
h₁ : y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
exact Or.inr ⟨h.1.1, LE.le.lt_of_not_le h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩
no goals
case neg
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
exact Or.inl ⟨LE.le.lt_of_not_le h.1.1 h₁, h.1.2⟩
case refine'_2.inl.intro
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

case refine'_2.inr.intro
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y
case refine'_2
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y
rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
no goals
case refine'_2.inl.intro
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y
exact ⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_le h.1⟩
no goals
case refine'_2.inr.intro
ι : Type ?u.107734
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.107745
r : α → α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
a a₁ a₂ : α
b b₁ b₂ : β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y
exact ⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_le h.2⟩