Theorem: pow_two_le_fac (MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean)

State before:
n : ℕ
⊢ 2 ^ (n - 1) ≤ fac n
Tactic:
rcases n with _ | n
State after:
case zero

⊢ 2 ^ (0 - 1) ≤ fac 0

case succ
n : ℕ
⊢ 2 ^ (n + 1 - 1) ≤ fac (n + 1)

State before:
case succ
n : ℕ
⊢ 2 ^ (n + 1 - 1) ≤ fac (n + 1)
Tactic:
induction' n with n ih
State after:
case succ.zero

⊢ 2 ^ (0 + 1 - 1) ≤ fac (0 + 1)

case succ.succ
n : ℕ
ih : 2 ^ (n + 1 - 1) ≤ fac (n + 1)
⊢ 2 ^ (n + 1 + 1 - 1) ≤ fac (n + 1 + 1)

State before:
case succ.succ
n : ℕ
ih : 2 ^ (n + 1 - 1) ≤ fac (n + 1)
⊢ 2 ^ (n + 1 + 1 - 1) ≤ fac (n + 1 + 1)
Tactic:
simp at *
State after:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 ^ (n + 1) ≤ fac (n + 1 + 1)

State before:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 ^ (n + 1) ≤ fac (n + 1 + 1)
Tactic:
rw [pow_succ', fac]
State after:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 * 2 ^ n ≤ (n + 1 + 1) * fac (n + 1)

State before:
case succ.succ
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 * 2 ^ n ≤ (n + 1 + 1) * fac (n + 1)
Tactic:
apply Nat.mul_le_mul _ ih
State after:
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 ≤ n + 1 + 1

State before:
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 2 ≤ n + 1 + 1
Tactic:
repeat' apply Nat.succ_le_succ
State after:
case a.a
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 0 ≤ n

State before:
case a.a
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 0 ≤ n
Tactic:
apply zero_le
State after:
no goals

State before:
case zero

⊢ 2 ^ (0 - 1) ≤ fac 0
Tactic:
simp [fac]
State after:
no goals

State before:
case succ.zero

⊢ 2 ^ (0 + 1 - 1) ≤ fac (0 + 1)
Tactic:
simp [fac]
State after:
no goals

State before:
case a
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 1 ≤ n + 1
Tactic:
apply Nat.succ_le_succ
State after:
case a.a
n : ℕ
ih : 2 ^ n ≤ fac (n + 1)
⊢ 0 ≤ n