case zero

⊢ ack 3 zero = 2 ^ (zero + 3) - 3

case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ ack 3 (succ n) = 2 ^ (succ n + 3) - 3
n : ℕ
⊢ ack 3 n = 2 ^ (n + 3) - 3
induction' n with n IH
no goals
case zero

⊢ ack 3 zero = 2 ^ (zero + 3) - 3
rfl
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ ack 3 (succ n) = 2 ^ (succ n + 3) - 3
rw [ack_succ_succ, IH, ack_two, Nat.succ_add, Nat.pow_succ 2 (n + 3), mul_comm _ 2,
    Nat.mul_sub_left_distrib, ← Nat.sub_add_comm, two_mul 3, Nat.add_sub_add_right]
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)
have H : 2 * 3 ≤ 2 * 2 ^ 3 := by norm_num
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 * 2 ^ 3 ≤ 2 * 2 ^ (n + 3)
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 * 3 ≤ 2 * 2 ^ (n + 3)
apply H.trans
no goals
case succ
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
H : 2 * 3 ≤ 2 * 2 ^ 3
⊢ 2 * 2 ^ 3 ≤ 2 * 2 ^ (n + 3)
simp [pow_le_pow]
no goals
n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ 3
norm_num