Theorem: Section15Sheet7Solutions.factorial_eq_prod (FormalisingMathematics2024/Solutions/Section15numberTheory/Sheet8.lean)

State before:
n : ℕ
⊢ Nat.factorial n = ∏ i in Finset.Icc 1 n, i
Tactic:
induction' n with d hd
State after:
case zero

⊢ Nat.factorial Nat.zero = ∏ i in Finset.Icc 1 Nat.zero, i

case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ Nat.factorial (Nat.succ d) = ∏ i in Finset.Icc 1 (Nat.succ d), i

State before:
case zero

⊢ Nat.factorial Nat.zero = ∏ i in Finset.Icc 1 Nat.zero, i
Tactic:
rfl
State after:
no goals

State before:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ Nat.factorial (Nat.succ d) = ∏ i in Finset.Icc 1 (Nat.succ d), i
Tactic:
rw [Nat.factorial_succ, hd]
State after:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i = ∏ i in Finset.Icc 1 (Nat.succ d), i

State before:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i = ∏ i in Finset.Icc 1 (Nat.succ d), i
Tactic:
rw [Finset.Icc_eq_cons_Ico (show 1 ≤ d + 1 by linarith)]
State after:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i =
    ∏ i in Finset.cons (d + 1) (Finset.Ico 1 (d + 1)) (_ : d + 1 ∉ Finset.Ico 1 (d + 1)), i

State before:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i =
    ∏ i in Finset.cons (d + 1) (Finset.Ico 1 (d + 1)) (_ : d + 1 ∉ Finset.Ico 1 (d + 1)), i
Tactic:
rw [Finset.prod_cons]
State after:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i = (d + 1) * ∏ x in Finset.Ico 1 (d + 1), x

State before:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i = (d + 1) * ∏ x in Finset.Ico 1 (d + 1), x
Tactic:
congr
State after:
no goals

State before:
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ 1 ≤ d + 1
Tactic:
linarith
State after:
no goals