[GOAL]
m k : ℕ
⊢ hyperoperation 0 m k = Nat.succ k
[PROOFSTEP]
rw [hyperoperation, Nat.succ_eq_add_one]
[GOAL]
n m : ℕ
⊢ hyperoperation (n + 3) m 0 = 1
[PROOFSTEP]
rw [hyperoperation]
[GOAL]
n m k : ℕ
⊢ hyperoperation (n + 1) m (k + 1) = hyperoperation n m (hyperoperation (n + 1) m k)
[PROOFSTEP]
rw [hyperoperation]
[GOAL]
⊢ hyperoperation 1 = fun x x_1 => x + x_1
[PROOFSTEP]
ext m k
[GOAL]
case h.h
m k : ℕ
⊢ hyperoperation 1 m k = m + k
[PROOFSTEP]
induction' k with bn bih
[GOAL]
case h.h.zero
m : ℕ
⊢ hyperoperation 1 m Nat.zero = m + Nat.zero
[PROOFSTEP]
rw [Nat.add_zero m, hyperoperation]
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ hyperoperation 1 m (Nat.succ bn) = m + Nat.succ bn
[PROOFSTEP]
rw [hyperoperation_recursion, bih, hyperoperation_zero]
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 1 m bn = m + bn
⊢ Nat.succ (m + bn) = m + Nat.succ bn
[PROOFSTEP]
exact Nat.add_assoc m bn 1
[GOAL]
⊢ hyperoperation 2 = fun x x_1 => x * x_1
[PROOFSTEP]
ext m k
[GOAL]
case h.h
m k : ℕ
⊢ hyperoperation 2 m k = m * k
[PROOFSTEP]
induction' k with bn bih
[GOAL]
case h.h.zero
m : ℕ
⊢ hyperoperation 2 m Nat.zero = m * Nat.zero
[PROOFSTEP]
rw [hyperoperation]
[GOAL]
case h.h.zero
m : ℕ
⊢ 0 = m * Nat.zero
[PROOFSTEP]
exact (Nat.mul_zero m).symm
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ hyperoperation 2 m (Nat.succ bn) = m * Nat.succ bn
[PROOFSTEP]
rw [hyperoperation_recursion, hyperoperation_one, bih]
  -- porting note: was `ring`
[GOAL]
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
[PROOFSTEP]
dsimp only
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m + m * bn = m * Nat.succ bn
[PROOFSTEP]
nth_rewrite 1 [← mul_one m]
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 2 m bn = m * bn
⊢ m * 1 + m * bn = m * Nat.succ bn
[PROOFSTEP]
rw [← mul_add, add_comm, Nat.succ_eq_add_one]
[GOAL]
⊢ hyperoperation 3 = fun x x_1 => x ^ x_1
[PROOFSTEP]
ext m k
[GOAL]
case h.h
m k : ℕ
⊢ hyperoperation 3 m k = m ^ k
[PROOFSTEP]
induction' k with bn bih
[GOAL]
case h.h.zero
m : ℕ
⊢ hyperoperation 3 m Nat.zero = m ^ Nat.zero
[PROOFSTEP]
rw [hyperoperation_ge_three_eq_one]
[GOAL]
case h.h.zero
m : ℕ
⊢ 1 = m ^ Nat.zero
[PROOFSTEP]
exact (pow_zero m).symm
[GOAL]
case h.h.succ
m bn : ℕ
bih : hyperoperation 3 m bn = m ^ bn
⊢ hyperoperation 3 m (Nat.succ bn) = m ^ Nat.succ bn
[PROOFSTEP]
rw [hyperoperation_recursion, hyperoperation_two, bih]
[GOAL]
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
[PROOFSTEP]
exact (pow_succ m bn).symm
[GOAL]
n m : ℕ
⊢ hyperoperation (n + 2) m 1 = m
[PROOFSTEP]
induction' n with nn nih
[GOAL]
case zero
m : ℕ
⊢ hyperoperation (Nat.zero + 2) m 1 = m
[PROOFSTEP]
rw [hyperoperation_two]
[GOAL]
case zero
m : ℕ
⊢ (fun x x_1 => x * x_1) m 1 = m
[PROOFSTEP]
ring
[GOAL]
case succ
m nn : ℕ
nih : hyperoperation (nn + 2) m 1 = m
⊢ hyperoperation (Nat.succ nn + 2) m 1 = m
[PROOFSTEP]
rw [hyperoperation_recursion, hyperoperation_ge_three_eq_one, nih]
[GOAL]
n : ℕ
⊢ hyperoperation (n + 1) 2 2 = 4
[PROOFSTEP]
induction' n with nn nih
[GOAL]
case zero
⊢ hyperoperation (Nat.zero + 1) 2 2 = 4
[PROOFSTEP]
rw [hyperoperation_one]
[GOAL]
case succ
nn : ℕ
nih : hyperoperation (nn + 1) 2 2 = 4
⊢ hyperoperation (Nat.succ nn + 1) 2 2 = 4
[PROOFSTEP]
rw [hyperoperation_recursion, hyperoperation_ge_two_eq_self, nih]
[GOAL]
n : ℕ
⊢ ∀ (k : ℕ), hyperoperation (n + 3) 1 k = 1
[PROOFSTEP]
induction' n with nn nih
[GOAL]
case zero
⊢ ∀ (k : ℕ), hyperoperation (Nat.zero + 3) 1 k = 1
[PROOFSTEP]
intro k
[GOAL]
case zero
k : ℕ
⊢ hyperoperation (Nat.zero + 3) 1 k = 1
[PROOFSTEP]
rw [hyperoperation_three]
[GOAL]
case zero
k : ℕ
⊢ (fun x x_1 => x ^ x_1) 1 k = 1
[PROOFSTEP]
dsimp
[GOAL]
case zero
k : ℕ
⊢ 1 ^ k = 1
[PROOFSTEP]
rw [one_pow]
[GOAL]
case succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
⊢ ∀ (k : ℕ), hyperoperation (Nat.succ nn + 3) 1 k = 1
[PROOFSTEP]
intro k
[GOAL]
case succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
k : ℕ
⊢ hyperoperation (Nat.succ nn + 3) 1 k = 1
[PROOFSTEP]
cases k
[GOAL]
case succ.zero
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
⊢ hyperoperation (Nat.succ nn + 3) 1 Nat.zero = 1
[PROOFSTEP]
rw [hyperoperation_ge_three_eq_one]
[GOAL]
case succ.succ
nn : ℕ
nih : ∀ (k : ℕ), hyperoperation (nn + 3) 1 k = 1
n✝ : ℕ
⊢ hyperoperation (Nat.succ nn + 3) 1 (Nat.succ n✝) = 1
[PROOFSTEP]
rw [hyperoperation_recursion, nih]
[GOAL]
n k : ℕ
⊢ hyperoperation (n + 4) 0 k = if Even k then 1 else 0
[PROOFSTEP]
induction' k with kk kih
[GOAL]
case zero
n : ℕ
⊢ hyperoperation (n + 4) 0 Nat.zero = if Even Nat.zero then 1 else 0
[PROOFSTEP]
rw [hyperoperation_ge_three_eq_one]
[GOAL]
case zero
n : ℕ
⊢ 1 = if Even Nat.zero then 1 else 0
[PROOFSTEP]
simp only [even_zero, if_true]
[GOAL]
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 4) 0 (Nat.succ kk) = if Even (Nat.succ kk) then 1 else 0
[PROOFSTEP]
rw [hyperoperation_recursion]
[GOAL]
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (hyperoperation (n + 3 + 1) 0 kk) = if Even (Nat.succ kk) then 1 else 0
[PROOFSTEP]
rw [kih]
[GOAL]
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if Even (Nat.succ kk) then 1 else 0
[PROOFSTEP]
simp_rw [Nat.even_add_one]
[GOAL]
case succ
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
⊢ hyperoperation (n + 3) 0 (if Even kk then 1 else 0) = if ¬Even kk then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : Even kk
⊢ hyperoperation (n + 3) 0 1 = 0
[PROOFSTEP]
exact hyperoperation_ge_two_eq_self (n + 1) 0
[GOAL]
case neg
n kk : ℕ
kih : hyperoperation (n + 4) 0 kk = if Even kk then 1 else 0
h✝ : ¬Even kk
⊢ hyperoperation (n + 3) 0 0 = 1
[PROOFSTEP]
exact hyperoperation_ge_three_eq_one n 0
