[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(p - 1)! = -1
[PROOFSTEP]
refine'
  calc
    ((p - 1)! : ZMod p) = ∏ x in 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
      -- Porting note: `simp` is less powerful.
              -- simp_rw [← Units.coeHom_apply, ← (Units.coeHom (ZMod p)).map_prod,
              --   prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
      simp_rw [← Units.coeHom_apply]
      rw [← (Units.coeHom (ZMod p)).map_prod]
      simp_rw [prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(p - 1)! = ∏ x in Ico 1 (succ (p - 1)), ↑x
[PROOFSTEP]
rw [← Finset.prod_Ico_id_eq_factorial, prod_natCast]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x : (ZMod p)ˣ, ↑x = -1
[PROOFSTEP]
simp_rw [← Units.coeHom_apply]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x : (ZMod p)ˣ, ↑(Units.coeHom (ZMod p)) x = -1
[PROOFSTEP]
rw [← (Units.coeHom (ZMod p)).map_prod]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(Units.coeHom (ZMod p)) (∏ x : (ZMod p)ˣ, x) = -1
[PROOFSTEP]
simp_rw [prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x in Ico 1 (succ (p - 1)), ↑x = ∏ x : (ZMod p)ˣ, ↑x
[PROOFSTEP]
have hp : 0 < p := (Fact.out (p := p.Prime)).pos
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∏ x in Ico 1 (succ (p - 1)), ↑x = ∏ x : (ZMod p)ˣ, ↑x
[PROOFSTEP]
symm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∏ x : (ZMod p)ˣ, ↑x = ∏ x in Ico 1 (succ (p - 1)), ↑x
[PROOFSTEP]
refine' prod_bij (fun a _ => (a : ZMod p).val) _ _ _ _
[GOAL]
case refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a : (ZMod p)ˣ) (ha : a ∈ univ), (fun a x => val ↑a) a ha ∈ Ico 1 (succ (p - 1))
[PROOFSTEP]
intro a ha
[GOAL]
case refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => val ↑a) a ha ∈ Ico 1 (succ (p - 1))
[PROOFSTEP]
rw [mem_Ico, ← Nat.succ_sub hp, Nat.succ_sub_one]
[GOAL]
case refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (fun a x => val ↑a) a ha ∧ (fun a x => val ↑a) a ha < p
[PROOFSTEP]
constructor
[GOAL]
case refine'_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ 1 ≤ (fun a x => val ↑a) a ha
[PROOFSTEP]
apply Nat.pos_of_ne_zero
[GOAL]
case refine'_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => val ↑a) a ha ≠ 0
[PROOFSTEP]
rw [← @val_zero p]
[GOAL]
case refine'_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => val ↑a) a ha ≠ val 0
[PROOFSTEP]
intro h
[GOAL]
case refine'_1.left.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
h : (fun a x => val ↑a) a ha = val 0
⊢ False
[PROOFSTEP]
apply Units.ne_zero a (val_injective p h)
[GOAL]
case refine'_1.right
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (fun a x => val ↑a) a ha < p
[PROOFSTEP]
exact val_lt _
[GOAL]
case refine'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a : (ZMod p)ˣ) (ha : a ∈ univ), ↑a = ↑((fun a x => val ↑a) a ha)
[PROOFSTEP]
rintro a -
[GOAL]
case refine'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha✝ : a ∈ univ
⊢ ↑a = ↑((fun a x => val ↑a) a ha✝)
[PROOFSTEP]
simp only [cast_id, nat_cast_val]
[GOAL]
case refine'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (a₁ a₂ : (ZMod p)ˣ) (ha₁ : a₁ ∈ univ) (ha₂ : a₂ ∈ univ),
    (fun a x => val ↑a) a₁ ha₁ = (fun a x => val ↑a) a₂ ha₂ → a₁ = a₂
[PROOFSTEP]
intro _ _ _ _ h
[GOAL]
case refine'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ a₂✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
ha₂✝ : a₂✝ ∈ univ
h : (fun a x => val ↑a) a₁✝ ha₁✝ = (fun a x => val ↑a) a₂✝ ha₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
rw [Units.ext_iff]
[GOAL]
case refine'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ a₂✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
ha₂✝ : a₂✝ ∈ univ
h : (fun a x => val ↑a) a₁✝ ha₁✝ = (fun a x => val ↑a) a₂✝ ha₂✝
⊢ ↑a₁✝ = ↑a₂✝
[PROOFSTEP]
exact val_injective p h
[GOAL]
case refine'_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ (b : ℕ), b ∈ Ico 1 (succ (p - 1)) → ∃ a ha, b = (fun a x => val ↑a) a ha
[PROOFSTEP]
intro b hb
[GOAL]
case refine'_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ∈ Ico 1 (succ (p - 1))
⊢ ∃ a ha, b = (fun a x => val ↑a) a ha
[PROOFSTEP]
rw [mem_Ico, Nat.succ_le_iff, ← succ_sub hp, succ_sub_one, pos_iff_ne_zero] at hb 
[GOAL]
case refine'_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ∃ a ha, b = (fun a x => val ↑a) a ha
[PROOFSTEP]
refine' ⟨Units.mk0 b _, Finset.mem_univ _, _⟩
[GOAL]
case refine'_4.refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ↑b ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case refine'_4.refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : ↑b = 0
⊢ False
[PROOFSTEP]
apply hb.1
[GOAL]
case refine'_4.refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : ↑b = 0
⊢ b = 0
[PROOFSTEP]
apply_fun val at h 
[GOAL]
case refine'_4.refine'_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : val ↑b = val 0
⊢ b = 0
[PROOFSTEP]
simpa only [val_cast_of_lt hb.right, val_zero] using h
[GOAL]
case refine'_4.refine'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ b = (fun a x => val ↑a) (Units.mk0 ↑b (_ : ↑b = 0 → False)) (_ : Units.mk0 ↑b (_ : ↑b = 0 → False) ∈ univ)
[PROOFSTEP]
simp only [val_cast_of_lt hb.right, Units.val_mk0]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x in Ico 1 p, ↑x = -1
[PROOFSTEP]
conv =>
  congr
  congr
  rw [← succ_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
| ∏ x in Ico 1 p, ↑x = -1
[PROOFSTEP]
  congr
  congr
  rw [← succ_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
| ∏ x in Ico 1 p, ↑x = -1
[PROOFSTEP]
  congr
  congr
  rw [← succ_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
| ∏ x in Ico 1 p, ↑x = -1
[PROOFSTEP]
congr
[GOAL]
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
| ∏ x in Ico 1 p, ↑x
case a p : ℕ inst✝ : Fact (Nat.Prime p) | -1
[PROOFSTEP]
congr
[GOAL]
case a.s
p : ℕ
inst✝ : Fact (Nat.Prime p)
| Ico 1 p
case a.f
p : ℕ
inst✝ : Fact (Nat.Prime p)
| fun x => ↑x
case a p : ℕ inst✝ : Fact (Nat.Prime p) | -1
[PROOFSTEP]
rw [← succ_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∏ x in Ico 1 (succ (p - succ 0)), ↑x = -1
[PROOFSTEP]
rw [← prod_natCast, Finset.prod_Ico_id_eq_factorial, wilsons_lemma]
[GOAL]
n : ℕ
h : ↑(n - 1)! = -1
h1 : n ≠ 1
⊢ Prime n
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | h0)
[GOAL]
case inl
h : ↑(0 - 1)! = -1
h1 : 0 ≠ 1
⊢ Prime 0
[PROOFSTEP]
norm_num at h 
[GOAL]
case inr
n : ℕ
h : ↑(n - 1)! = -1
h1 : n ≠ 1
h0 : n ≠ 0
⊢ Prime n
[PROOFSTEP]
replace h1 : 1 < n := n.two_le_iff.mpr ⟨h0, h1⟩
[GOAL]
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
⊢ Prime n
[PROOFSTEP]
by_contra h2
[GOAL]
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
⊢ False
[PROOFSTEP]
obtain ⟨m, hm1, hm2 : 1 < m, hm3⟩ := exists_dvd_of_not_prime2 h1 h2
[GOAL]
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
⊢ False
[PROOFSTEP]
have hm : m ∣ (n - 1)! := Nat.dvd_factorial (pos_of_gt hm2) (le_pred_of_lt hm3)
[GOAL]
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ False
[PROOFSTEP]
refine' hm2.ne' (Nat.dvd_one.mp ((Nat.dvd_add_right hm).mp (hm1.trans _)))
[GOAL]
case inr.intro.intro.intro
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ n ∣ (n - 1)! + 1
[PROOFSTEP]
rw [← ZMod.nat_cast_zmod_eq_zero_iff_dvd, cast_add, cast_one, h, add_left_neg]
[GOAL]
n : ℕ
h : n ≠ 1
⊢ Prime n ↔ ↑(n - 1)! = -1
[PROOFSTEP]
refine' ⟨fun h1 => _, fun h2 => prime_of_fac_equiv_neg_one h2 h⟩
[GOAL]
n : ℕ
h : n ≠ 1
h1 : Prime n
⊢ ↑(n - 1)! = -1
[PROOFSTEP]
haveI := Fact.mk h1
[GOAL]
n : ℕ
h : n ≠ 1
h1 : Prime n
this : Fact (Prime n)
⊢ ↑(n - 1)! = -1
[PROOFSTEP]
exact ZMod.wilsons_lemma n
