case zero

⊢ zero ^ 2 ≤ 2 ^ (zero + 1) - 3

case succ
k : ℕ
hk : k ^ 2 ≤ 2 ^ (k + 1) - 3
⊢ succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
n : ℕ
⊢ n ^ 2 ≤ 2 ^ (n + 1) - 3
induction' n with k hk
no goals
case zero

⊢ zero ^ 2 ≤ 2 ^ (zero + 1) - 3
norm_num
case succ.zero
hk : zero ^ 2 ≤ 2 ^ (zero + 1) - 3
⊢ succ zero ^ 2 ≤ 2 ^ (succ zero + 1) - 3

case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ succ (succ k) ^ 2 ≤ 2 ^ (succ (succ k) + 1) - 3
case succ
k : ℕ
hk : k ^ 2 ≤ 2 ^ (k + 1) - 3
⊢ succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
cases' k with k k
no goals
case succ.zero
hk : zero ^ 2 ≤ 2 ^ (zero + 1) - 3
⊢ succ zero ^ 2 ≤ 2 ^ (succ zero + 1) - 3
norm_num
case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ (k + 1) ^ 2 + (2 * (k + 1) * 1 + 1 ^ 2) ≤ 2 ^ (k + 2) - 3 + 2 ^ (k + 2)

case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 3 ≤ 2 ^ (k + 2)
case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ succ (succ k) ^ 2 ≤ 2 ^ (succ (succ k) + 1) - 3
rw [succ_eq_add_one, add_sq, Nat.pow_succ 2, mul_comm _ 2, two_mul (2 ^ _),
    add_tsub_assoc_of_le, add_comm (2 ^ _), add_assoc]
case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 2 * (k + 1) * 1 + 1 ^ 2 ≤ 2 ^ (k + 2)
case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ (k + 1) ^ 2 + (2 * (k + 1) * 1 + 1 ^ 2) ≤ 2 ^ (k + 2) - 3 + 2 ^ (k + 2)
apply Nat.add_le_add hk
case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 2 * (k + 1) + 1 ≤ 2 ^ (k + 2)
case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 2 * (k + 1) * 1 + 1 ^ 2 ≤ 2 ^ (k + 2)
norm_num
case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 2 * (k + 1) < 2 ^ (k + 2)
case succ.succ
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 2 * (k + 1) + 1 ≤ 2 ^ (k + 2)
apply succ_le_of_lt
case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ k + 1 < 2 ^ (k + 1)
case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 2 * (k + 1) < 2 ^ (k + 2)
rw [Nat.pow_succ, mul_comm _ 2, mul_lt_mul_left (zero_lt_two' ℕ)]
no goals
case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ k + 1 < 2 ^ (k + 1)
apply lt_two_pow
case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 3 ≤ 2 ^ k * 2 * 2
case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 3 ≤ 2 ^ (k + 2)
rw [Nat.pow_succ, Nat.pow_succ]
no goals
case succ.succ.h
k : ℕ
hk : succ k ^ 2 ≤ 2 ^ (succ k + 1) - 3
⊢ 3 ≤ 2 ^ k * 2 * 2
linarith [one_le_pow k 2 zero_lt_two]