rcases k with (_ | _ | _)
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ≤ k
case intro.inl.intro.zero
n2 : 2 < 2 ^ Nat.zero
⊢ 2 ≤ Nat.zero

case intro.inl.intro.succ.zero
n2 : 2 < 2 ^ Nat.succ Nat.zero
⊢ 2 ≤ Nat.succ Nat.zero

case intro.inl.intro.succ.succ
n✝ : ℕ
n2 : 2 < 2 ^ Nat.succ (Nat.succ n✝)
⊢ 2 ≤ Nat.succ (Nat.succ n✝)