Theorem: pow_two_le_fac (LeanCourse/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 ^ (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:
sorry
State after:
no goals

State before:
case zero

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