case mk.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.18624
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
ha : (a₁, b₁).fst ≤ (a₂, b₂).fst
hb : (a₁, b₁).snd ≤ (a₂, b₂).snd
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)
α : Type u_1
β : Type u_2
γ : Type ?u.18624
inst✝¹ : PartialOrder α
inst✝ : Preorder β
⊢ Monotone ↑toLex
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ ⟨ha, hb⟩
case mk.mk.intro.inl
α : Type u_1
β : Type u_2
γ : Type ?u.18624
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
ha : (a₁, b₁).fst ≤ (a₁, b₂).fst
hb : (a₁, b₁).snd ≤ (a₁, b₂).snd
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₁, b₂)

case mk.mk.intro.inr
α : Type u_1
β : Type u_2
γ : Type ?u.18624
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
ha✝ : (a₁, b₁).fst ≤ (a₂, b₂).fst
hb : (a₁, b₁).snd ≤ (a₂, b₂).snd
ha : (a₁, b₁).fst < (a₂, b₂).fst
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)
case mk.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.18624
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
ha : (a₁, b₁).fst ≤ (a₂, b₂).fst
hb : (a₁, b₁).snd ≤ (a₂, b₂).snd
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)
obtain rfl | ha : a₁ = a₂ ∨ _ := ha.eq_or_lt
no goals
case mk.mk.intro.inl
α : Type u_1
β : Type u_2
γ : Type ?u.18624
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
ha : (a₁, b₁).fst ≤ (a₁, b₂).fst
hb : (a₁, b₁).snd ≤ (a₁, b₂).snd
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₁, b₂)
exact right _ hb
no goals
case mk.mk.intro.inr
α : Type u_1
β : Type u_2
γ : Type ?u.18624
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
ha✝ : (a₁, b₁).fst ≤ (a₂, b₂).fst
hb : (a₁, b₁).snd ≤ (a₂, b₂).snd
ha : (a₁, b₁).fst < (a₂, b₂).fst
⊢ ↑toLex (a₁, b₁) ≤ ↑toLex (a₂, b₂)
exact left _ _ ha