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

State before:
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = -1
Tactic:
have := (Nat.prime_iff_fac_equiv_neg_one (?_ : p ≠ 1)).1 hp
State after:
case refine_2
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
this : ↑(Nat.factorial (p - 1)) = -1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = -1

case refine_1
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
⊢ p ≠ 1

State before:
case refine_2
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
this : ↑(Nat.factorial (p - 1)) = -1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = -1
Tactic:
rw [← this, hn]
State after:
case refine_2
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
this : ↑(Nat.factorial (p - 1)) = -1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = ↑(Nat.factorial (4 * n + 1 - 1))

State before:
case refine_2
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
this : ↑(Nat.factorial (p - 1)) = -1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = ↑(Nat.factorial (4 * n + 1 - 1))
Tactic:
simp
State after:
case refine_2
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
this : ↑(Nat.factorial (p - 1)) = -1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = ↑(Nat.factorial (4 * n))

State before:
case refine_2
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
this : ↑(Nat.factorial (p - 1)) = -1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = ↑(Nat.factorial (4 * n))
Tactic:
rw [factorial_eq_prod, Nat.cast_prod]
State after:
no goals

State before:
case refine_1
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
⊢ p ≠ 1
Tactic:
exact Nat.Prime.ne_one hp
State after:
no goals