case h.h
m k : ℕ
⊢ hyperoperation 3 m k = m ^ k
⊢ hyperoperation 3 = fun x x_1 => x ^ x_1
ext (m k)
case h.h.zero
m : ℕ
⊢ hyperoperation 3 m Nat.zero = m ^ Nat.zero

case h.h.succ
m bn : ℕ
bih : hyperoperation 3 m bn = m ^ bn
⊢ hyperoperation 3 m (Nat.succ bn) = m ^ Nat.succ bn
case h.h
m k : ℕ
⊢ hyperoperation 3 m k = m ^ k
induction' k with bn bih
case h.h.zero
m : ℕ
⊢ 1 = m ^ Nat.zero
case h.h.zero
m : ℕ
⊢ hyperoperation 3 m Nat.zero = m ^ Nat.zero
rw [hyperoperation_ge_three_eq_one]
no goals
case h.h.zero
m : ℕ
⊢ 1 = m ^ Nat.zero
exact (pow_zero m).symm
case h.h.succ
m bn : ℕ
bih : hyperoperation 3 m bn = m ^ bn
⊢ (fun x x_1 => x * x_1) m (m ^ bn) = m ^ Nat.succ bn
case h.h.succ
m bn : ℕ
bih : hyperoperation 3 m bn = m ^ bn
⊢ hyperoperation 3 m (Nat.succ bn) = m ^ Nat.succ bn
rw [hyperoperation_recursion, hyperoperation_two, bih]
no goals
case h.h.succ
m bn : ℕ
bih : hyperoperation 3 m bn = m ^ bn
⊢ (fun x x_1 => x * x_1) m (m ^ bn) = m ^ Nat.succ bn
exact (pow_succ m bn).symm