case zero

⊢ hyperoperation (Nat.zero + 1) 2 2 = 4

case succ
nn : ℕ
nih : hyperoperation (nn + 1) 2 2 = 4
⊢ hyperoperation (Nat.succ nn + 1) 2 2 = 4
n : ℕ
⊢ hyperoperation (n + 1) 2 2 = 4
induction' n with nn nih
no goals
case zero

⊢ hyperoperation (Nat.zero + 1) 2 2 = 4
rw [hyperoperation_one]
no goals
case succ
nn : ℕ
nih : hyperoperation (nn + 1) 2 2 = 4
⊢ hyperoperation (Nat.succ nn + 1) 2 2 = 4
rw [hyperoperation_recursion, hyperoperation_ge_two_eq_self, nih]