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

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

⊢ 0 < fac 0

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

State before:
⊢ 0 < fac 0
Tactic:
case zero =>
  rw [fac]
  norm_num
State after:
no goals

State before:
k : ℕ
ih : 0 < fac k
⊢ 0 < fac (k + 1)
Tactic:
case succ k ih =>
  rw [fac]
  positivity
State after:
no goals

State before:
⊢ 0 < fac 0
Tactic:
rw [fac]
State after:
⊢ 0 < 1

State before:
⊢ 0 < 1
Tactic:
norm_num
State after:
no goals

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

State before:
k : ℕ
ih : 0 < fac k
⊢ 0 < (k + 1) * fac k
Tactic:
positivity
State after:
no goals