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

case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ hyperoperation 2 m (Nat.succ bn) = m * Nat.succ bn
case h.h
m k : ℕ
⊢ hyperoperation 2 m k = m * k
induction' k with bn bih
case h.h.zero
m : ℕ
⊢ 0 = m * Nat.zero
case h.h.zero
m : ℕ
⊢ hyperoperation 2 m Nat.zero = m * Nat.zero
rw [hyperoperation]
no goals
case h.h.zero
m : ℕ
⊢ 0 = m * Nat.zero
exact (Nat.mul_zero m).symm
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 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 2 m bn = m * bn
⊢ hyperoperation 2 m (Nat.succ bn) = m * Nat.succ bn
rw [hyperoperation_recursion, hyperoperation_one, bih]
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m + m * bn = m * Nat.succ bn
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ (fun x x_1 => x + x_1) m (m * bn) = m * Nat.succ bn
dsimp only
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m * 1 + m * bn = m * Nat.succ bn
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m + m * bn = m * Nat.succ bn
nth_rewrite 1 [← mul_one m]
no goals
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m * 1 + m * bn = m * Nat.succ bn
rw [← mul_add, add_comm, Nat.succ_eq_add_one]