Theorem: pow_two_le_fac (LeanCourse/Lectures/Lecture7.lean)

State before:
n : ℕ
⊢ 2 ^ n ≤ fac (n + 1)
Tactic:
induction n
State after:
case zero

⊢ 2 ^ 0 ≤ fac (0 + 1)

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

State before:
⊢ 2 ^ 0 ≤ fac (0 + 1)
Tactic:
case zero =>
  norm_num
State after:
no goals

State before:
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ (k + 1) ≤ fac (k + 1 + 1)
Tactic:
case succ k ih =>
  rw [fac, pow_add, mul_comm]
  gcongr
  linarith
State after:
no goals

State before:
⊢ 2 ^ 0 ≤ fac (0 + 1)
Tactic:
norm_num
State after:
no goals

State before:
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ (k + 1) ≤ fac (k + 1 + 1)
Tactic:
rw [fac, pow_add, mul_comm]
State after:
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ 1 * 2 ^ k ≤ (k + 1 + 1) * fac (k + 1)

State before:
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ 1 * 2 ^ k ≤ (k + 1 + 1) * fac (k + 1)
Tactic:
gcongr
State after:
case h₁
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ 1 ≤ k + 1 + 1

State before:
case h₁
k : ℕ
ih : 2 ^ k ≤ fac (k + 1)
⊢ 2 ^ 1 ≤ k + 1 + 1
Tactic:
linarith
State after:
no goals