rcases lt_or_eq_of_le ha with (ha | rfl) <;> rcases lt_or_eq_of_le hb with (hb | rfl)
n a₁ a₂ b₁ b₂ : ℕ
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁.pair b₁ ≤ a₂.pair b₂
case inl.inl
n a₁ a₂ b₁ b₂ : ℕ
ha✝ : a₁ ≤ a₂
hb✝ : b₁ ≤ b₂
ha : a₁ < a₂
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₂.pair b₂

case inl.inr
n a₁ a₂ b₁ : ℕ
ha✝ : a₁ ≤ a₂
ha : a₁ < a₂
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₂.pair b₁

case inr.inl
n a₁ b₁ b₂ : ℕ
hb✝ : b₁ ≤ b₂
ha : a₁ ≤ a₁
hb : b₁ < b₂
⊢ a₁.pair b₁ ≤ a₁.pair b₂

case inr.inr
n a₁ b₁ : ℕ
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
⊢ a₁.pair b₁ ≤ a₁.pair b₁