Theorem: pow_two_le_fac (LeanCourse/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean)

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

⊢ 2 ^ (Nat.zero - 1) ≤ fac Nat.zero

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

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

⊢ 2 ^ (Nat.succ 0 - 1) ≤ fac (Nat.succ 0)

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

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

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

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

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

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

State before:
case zero

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

State before:
case succ.zero

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

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