Theorem: fac_succ (LeanCourse/Lectures/Lecture7Before.lean)

State before:
n✝ n : ℕ
⊢ fac (n + 1) = (n + 1) * fac n
Tactic:
sorry
State after:
no goals