-- Mathlib/NumberTheory/Wilson.lean
theorem wilsons_lemma : ((p - 1)! : ZMod p) = -1

Proof state:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a : (ZMod p)ˣ) (ha : a ∈ univ), (fun a x => (↑a).val) a ha ∈ Ico 1 (p - 1).succ

Tactic:
intro a ha

Result:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => (↑a).val) a ha ∈ Ico 1 (p - 1).succ

Proof state:
case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : ↑b = 0
⊢ b = 0

Tactic:
apply_fun val at h

Result:
case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : (↑b).val = val 0
⊢ b = 0

Proof state:
case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha✝ : a ∈ univ
⊢ ↑a = ↑((fun a x => (↑a).val) a ha✝)

Tactic:
simp only [cast_id, natCast_val]

Result:
no goals

Proof state:
case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ∈ Ico 1 (p - 1).succ
⊢ ∃ a, ∃ (ha : a ∈ univ), (fun a x => (↑a).val) a ha = b

Tactic:
rw [mem_Ico, Nat.succ_le_iff, ← succ_sub hp, Nat.add_one_sub_one, pos_iff_ne_zero] at hb

Result:
case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ∃ a, ∃ (ha : a ∈ univ), (fun a x => (↑a).val) a ha = b

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (Units.coeHom (ZMod p)) (∏ x : (ZMod p)ˣ, x) = -1

Tactic:
simp_rw [prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]

Result:
no goals

Proof state:
case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : (↑b).val = val 0
⊢ b = 0

Tactic:
simpa only [val_cast_of_lt hb.right, val_zero] using h

Result:
no goals

Proof state:
case refine_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (fun a x => (↑a).val) a ha

Tactic:
apply Nat.pos_of_ne_zero

Result:
case refine_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => (↑a).val) a ha ≠ 0

Proof state:
case refine_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
h : (fun a x => (↑a).val) a ha = val 0
⊢ False

Tactic:
apply Units.ne_zero a (val_injective p h)

Result:
no goals

Proof state:
case refine_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => (↑a).val) a ha ≠ val 0

Tactic:
intro h

Result:
case refine_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
h : (fun a x => (↑a).val) a ha = val 0
⊢ False

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∏ x ∈ Ico 1 (p - 1).succ, ↑x = ∏ x : (ZMod p)ˣ, ↑x

Tactic:
symm

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∏ x : (ZMod p)ˣ, ↑x = ∏ x ∈ Ico 1 (p - 1).succ, ↑x

Proof state:
case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ∃ a, ∃ (ha : a ∈ univ), (fun a x => (↑a).val) a ha = b

Tactic:
refine ⟨Units.mk0 b ?_, Finset.mem_univ _, ?_⟩

Result:
case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ↑b ≠ 0

case refine_3.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ (fun a x => (↑a).val) (Units.mk0 ↑b ?refine_3.refine_1) ⋯ = b

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x : (ZMod p)ˣ, (Units.coeHom (ZMod p)) x = -1

Tactic:
rw [← map_prod (Units.coeHom (ZMod p))]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ (Units.coeHom (ZMod p)) (∏ x : (ZMod p)ˣ, x) = -1

Proof state:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (fun a x => (↑a).val) a ha ∧ (fun a x => (↑a).val) a ha < p

Tactic:
constructor

Result:
case refine_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (fun a x => (↑a).val) a ha

case refine_1.right
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => (↑a).val) a ha < p

Proof state:
case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ↑b ≠ 0

Tactic:
intro h

Result:
case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : ↑b = 0
⊢ False

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(p - 1)! = -1

Tactic:
refine
  calc
    ((p - 1)! : ZMod p) = ∏ x ∈ Ico 1 (succ (p - 1)), (x : ZMod p) := by
      rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]
    _ = ∏ x : (ZMod p)ˣ, (x : ZMod p) := ?_
    _ = -1 := by
      simp_rw [← Units.coeHom_apply]
      rw [← map_prod (Units.coeHom (ZMod p))]
      simp_rw [prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x ∈ Ico 1 (p - 1).succ, ↑x = ∏ x : (ZMod p)ˣ, ↑x

Proof state:
case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : ↑b = 0
⊢ False

Tactic:
apply hb.1

Result:
case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : ↑b = 0
⊢ b = 0

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x ∈ Ico 1 (p - 1).succ, ↑x = ∏ x : (ZMod p)ˣ, ↑x

Tactic:
have hp : 0 < p := (Fact.out (p := p.Prime)).pos

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∏ x ∈ Ico 1 (p - 1).succ, ↑x = ∏ x : (ZMod p)ˣ, ↑x

Proof state:
case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a : (ZMod p)ˣ) (ha : a ∈ univ), ↑a = ↑((fun a x => (↑a).val) a ha)

Tactic:
rintro a -

Result:
case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha✝ : a ∈ univ
⊢ ↑a = ↑((fun a x => (↑a).val) a ha✝)

Proof state:
case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
a₂✝ : (ZMod p)ˣ
ha₂✝ : a₂✝ ∈ univ
h : (fun a x => (↑a).val) a₁✝ ha₁✝ = (fun a x => (↑a).val) a₂✝ ha₂✝
⊢ ↑a₁✝ = ↑a₂✝

Tactic:
exact val_injective p h

Result:
no goals

Proof state:
case refine_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => (↑a).val) a ha ≠ 0

Tactic:
rw [← @val_zero p]

Result:
case refine_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => (↑a).val) a ha ≠ val 0

Proof state:
case refine_3.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ (fun a x => (↑a).val) (Units.mk0 ↑b ⋯) ⋯ = b

Tactic:
simp only [val_cast_of_lt hb.right, Units.val_mk0]

Result:
no goals

Proof state:
case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a₁ : (ZMod p)ˣ) (ha₁ : a₁ ∈ univ) (a₂ : (ZMod p)ˣ) (ha₂ : a₂ ∈ univ),
    (fun a x => (↑a).val) a₁ ha₁ = (fun a x => (↑a).val) a₂ ha₂ → a₁ = a₂

Tactic:
intro _ _ _ _ h

Result:
case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
a₂✝ : (ZMod p)ˣ
ha₂✝ : a₂✝ ∈ univ
h : (fun a x => (↑a).val) a₁✝ ha₁✝ = (fun a x => (↑a).val) a₂✝ ha₂✝
⊢ a₁✝ = a₂✝

Proof state:
case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
a₂✝ : (ZMod p)ˣ
ha₂✝ : a₂✝ ∈ univ
h : (fun a x => (↑a).val) a₁✝ ha₁✝ = (fun a x => (↑a).val) a₂✝ ha₂✝
⊢ a₁✝ = a₂✝

Tactic:
rw [Units.ext_iff]

Result:
case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
a₂✝ : (ZMod p)ˣ
ha₂✝ : a₂✝ ∈ univ
h : (fun a x => (↑a).val) a₁✝ ha₁✝ = (fun a x => (↑a).val) a₂✝ ha₂✝
⊢ ↑a₁✝ = ↑a₂✝

Proof state:
case refine_1.right
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => (↑a).val) a ha < p

Tactic:
exact val_lt _

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(p - 1)! = ∏ x ∈ Ico 1 (p - 1).succ, ↑x

Tactic:
rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]

Result:
no goals