case mk.mk
α : Type u_1
β : Type u_2
γ : Type ?u.19022
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ : β
a₂ : α
b₂ : β
h : (a₁, b₁) < (a₂, b₂)
⊢ ↑toLex (a₁, b₁) < ↑toLex (a₂, b₂)
α : Type u_1
β : Type u_2
γ : Type ?u.19022
inst✝¹ : PartialOrder α
inst✝ : Preorder β
⊢ StrictMono ↑toLex
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h
case mk.mk.inl
α : Type u_1
β : Type u_2
γ : Type ?u.19022
inst✝¹ : PartialOrder α
inst✝ : Preorder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) < (a₁, b₂)
⊢ ↑toLex (a₁, b₁) < ↑toLex (a₁, b₂)

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