Theorem: fac_pos (LeanCourse/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean)

State before:
n : ℕ
⊢ 0 < fac n
Tactic:
induction' n with n ih
State after:
case zero

⊢ 0 < fac 0

case succ
n : ℕ
ih : 0 < fac n
⊢ 0 < fac (n + 1)

State before:
case succ
n : ℕ
ih : 0 < fac n
⊢ 0 < fac (n + 1)
Tactic:
rw [fac]
State after:
case succ
n : ℕ
ih : 0 < fac n
⊢ 0 < (n + 1) * fac n

State before:
case succ
n : ℕ
ih : 0 < fac n
⊢ 0 < (n + 1) * fac n
Tactic:
exact mul_pos n.succ_pos ih
State after:
no goals

State before:
case zero

⊢ 0 < fac 0
Tactic:
rw [fac]
State after:
case zero

⊢ 0 < 1

State before:
case zero

⊢ 0 < 1
Tactic:
exact zero_lt_one
State after:
no goals