exact ⟨Nat.lt_succ_of_le (Nat.unpair_left_le n),
  by { intro i hi
       have : i < n.unpair.2 := lt_of_mem_list n.unpair.2 i hi
       exact lt_trans this (Nat.lt_succ_of_le $ Nat.unpair_right_le n) }⟩
n : ℕ
this : n.unpair.2 < n + 1
⊢ n.unpair.1 < n + 1 ∧ ∀ a ∈ ofNat (List ℕ) n.unpair.2, a < n + 1
no goals