awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
simp_rw : Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) x) (-1)
simp_rw₁ : Eq (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) (∏ x : (ZMod p)ˣ, x)) (-1)
simp_rw₂ : Eq (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) (-1)) (-1)
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (-1)
have simp_rw₃ : Eq (α := ZMod p) (↑(-1) : ZMod p) (-1)
Tactic: simp_rw [← Units.coeHom_apply, ← map_prod (Units.coeHom (ZMod p)),
          prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
simp_rw : Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) x) (-1)
simp_rw₁ : Eq (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) (∏ x : (ZMod p)ˣ, x)) (-1)
simp_rw₂ : Eq (α := ZMod p) ((Units.coeHom (ZMod p) : (a : (ZMod p)ˣ) → ZMod p) (-1)) (-1)
simp_rw₃ : Eq (α := ZMod p) (↑(-1) : ZMod p) (-1)
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (-1)
have simp_rw₄ : Eq (α := ZMod p) (-(↑1 : ZMod p)) (-1)
Tactic: simp_rw [← Units.coeHom_apply, ← map_prod (Units.coeHom (ZMod p)),
          prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := ZMod p) (↑(p - 1)! : ZMod p) (-1)
have ZMod : Eq (α := ZMod p) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p)) (∏ x : (ZMod p)ˣ, (↑x : ZMod p))
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, ← map_prod (Units.coeHom (ZMod p)),
          prod_univ_units_id_eq_neg_one, Units.coeHom_apply, Units.val_neg, Units.val_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := ZMod p) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p)) (∏ x : (ZMod p)ˣ, (↑x : ZMod p))
have hp : 0 < p
Tactic: have hp : 0 < p := (Fact.out (p := p.Prime)).pos
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
⊢ Eq (α := ZMod p) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p)) (∏ x : (ZMod p)ˣ, (↑x : ZMod p))
have symm : Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))
Tactic: symm
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))
have refine_1 : ∀ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
  (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha ∈
    Ico 1 (p - 1).succ
Tactic: refine prod_bij (fun a _ => (a : ZMod p).val) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
refine_1 :
  ∀ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha ∈
      Ico 1 (p - 1).succ
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))
have refine_2 : ∀ (a₁ : (ZMod p)ˣ) (ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁) (a₂ : (ZMod p)ˣ)
  (ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂),
  Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
      ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂) →
    a₁ = a₂
Tactic: refine prod_bij (fun a _ => (a : ZMod p).val) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
refine_1 :
  ∀ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha ∈
      Ico 1 (p - 1).succ
refine_2 :
  ∀ (a₁ : (ZMod p)ˣ) (ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁) (a₂ : (ZMod p)ˣ)
    (ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂),
    Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
        ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂) →
      a₁ = a₂
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))
have refine_3 : ∀ b ∈ Ico 1 (p - 1).succ,
  ∃ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha = b
Tactic: refine prod_bij (fun a _ => (a : ZMod p).val) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
refine_1 :
  ∀ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha ∈
      Ico 1 (p - 1).succ
refine_2 :
  ∀ (a₁ : (ZMod p)ˣ) (ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁) (a₂ : (ZMod p)ˣ)
    (ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂),
    Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
        ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂) →
      a₁ = a₂
refine_3 :
  ∀ b ∈ Ico 1 (p - 1).succ,
    ∃ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
      (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha = b
⊢ Eq (α := ZMod p) (∏ x : (ZMod p)ˣ, (↑x : ZMod p)) (∏ x ∈ Ico 1 (p - 1).succ, (↑x : ZMod p))
have refine_4 : ∀ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
  (↑a : ZMod p) =
    (↑((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) : ZMod p)
Tactic: refine prod_bij (fun a _ => (a : ZMod p).val) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
⊢ (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha ∈
    Ico 1 (p - 1).succ
have refine_1 : LE.le (α := ℕ) 1 ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) ∧
  (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha < p
Tactic: rw [mem_Ico, ← Nat.succ_sub hp, Nat.add_one_sub_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
⊢ LE.le (α := ℕ) 1
      ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) ∧
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha < p
have refine_1 : LE.le (α := ℕ) 1 ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
refine_1 :
  LE.le (α := ℕ) 1 ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha)
⊢ LE.le (α := ℕ) 1
      ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) ∧
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha < p
have refine_1₁ : (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha < p
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
⊢ LE.le (α := ℕ) 1 ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha)
have refine_1 : Ne (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) 0
Tactic: apply Nat.pos_of_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
⊢ Ne (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) 0
have refine_1 : (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha ≠ val (n := p) 0
Tactic: rw [← @val_zero p]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a₁ : (ZMod p)ˣ
ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁
a₂ : (ZMod p)ˣ
ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂
h :
  Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
    ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂)
⊢ a₁ = a₂
have refine_2 : (↑a₁ : ZMod p) = (↑a₂ : ZMod p)
Tactic: rw [Units.ext_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ∈ Ico 1 (p - 1).succ
⊢ ∃ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha = b
have hb₁ : b ≠ 0 ∧ b < p
Tactic: rw [mem_Ico, Nat.succ_le_iff, ← succ_sub hp, Nat.add_one_sub_one, pos_iff_ne_zero] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ∃ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha = b
have refine_3 : Ne (α := ZMod p) (↑b : ZMod p) 0
Tactic: refine ⟨Units.mk0 b ?_, Finset.mem_univ _, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
refine_3 : Ne (α := ZMod p) (↑b : ZMod p) 0
⊢ ∃ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha = b
have refine_3₁ : (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val)
    (Units.mk0 (↑b : ZMod p) sorry) sorry =
  b
Tactic: refine ⟨Units.mk0 b ?_, Finset.mem_univ _, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : Eq (α := ZMod p) (↑b : ZMod p) 0
⊢ False
have refine_3 : b = 0
Tactic: apply hb.1
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : Eq (α := ZMod p) (↑b : ZMod p) 0
⊢ b = 0
have h₁ : val (n := p) (↑b : ZMod p) = val (n := p) 0
Tactic: apply_fun val at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
| Eq (α := ZMod p) (∏ x ∈ Ico 1 p, (↑x : ZMod p)) (-1)
have a : ∏ x ∈ Ico 1 p, (↑x : ZMod p)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ∏ x ∈ Ico 1 p, (↑x : ZMod p)
| Eq (α := ZMod p) (∏ x ∈ Ico 1 p, (↑x : ZMod p)) (-1)
have a₁ : -1
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
| ∏ x ∈ Ico 1 p, (↑x : ZMod p)
have a : Ico 1 p
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : Ico 1 p
| ∏ x ∈ Ico 1 p, (↑x : ZMod p)
have a₁ : fun (x : ℕ) ↦ (↑x : ZMod p)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
| Ico 1 p
have a : Ico 1 (p - succ 0).succ
Tactic: rw [← Nat.add_one_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
| Eq (α := ZMod p) (∏ x ∈ Ico 1 p, (↑x : ZMod p)) (-1)
have a : Ico 1 (p - succ 0).succ
Tactic: congr
    congr
    rw [← Nat.add_one_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : Ico 1 (p - succ 0).succ
| Eq (α := ZMod p) (∏ x ∈ Ico 1 p, (↑x : ZMod p)) (-1)
have a₁ : fun (x : ℕ) ↦ (↑x : ZMod p)
Tactic: congr
    congr
    rw [← Nat.add_one_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : Ico 1 (p - succ 0).succ
a₁ : fun (x : ℕ) ↦ (↑x : ZMod p)
| Eq (α := ZMod p) (∏ x ∈ Ico 1 p, (↑x : ZMod p)) (-1)
have a₂ : -1
Tactic: congr
    congr
    rw [← Nat.add_one_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := ZMod p) (∏ x ∈ Ico 1 p, (↑x : ZMod p)) (-1)
have conv : Eq (α := ZMod p) (∏ x ∈ Ico 1 (p - succ 0).succ, (↑x : ZMod p)) (-1)
Tactic: conv =>
    congr
    congr
    rw [← Nat.add_one_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := ZMod p) (∏ x ∈ Ico 1 (p - succ 0).succ, (↑x : ZMod p)) (-1)
have rw : Eq (α := ZMod p) (↑(∏ i ∈ Ico 1 (p - succ 0).succ, i) : ZMod p) (-1)
Tactic: rw [← prod_natCast, Finset.prod_Ico_id_eq_factorial, wilsons_lemma]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Eq (α := ZMod p) (↑(∏ i ∈ Ico 1 (p - succ 0).succ, i) : ZMod p) (-1)
⊢ Eq (α := ZMod p) (∏ x ∈ Ico 1 (p - succ 0).succ, (↑x : ZMod p)) (-1)
have rw₁ : Eq (α := ZMod p) (↑(p - succ 0)! : ZMod p) (-1)
Tactic: rw [← prod_natCast, Finset.prod_Ico_id_eq_factorial, wilsons_lemma]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Eq (α := ZMod p) (↑(∏ i ∈ Ico 1 (p - succ 0).succ, i) : ZMod p) (-1)
rw₁ : Eq (α := ZMod p) (↑(p - succ 0)! : ZMod p) (-1)
⊢ Eq (α := ZMod p) (∏ x ∈ Ico 1 (p - succ 0).succ, (↑x : ZMod p)) (-1)
have rw₂ : Eq (α := ZMod p) (-1) (-1)
Tactic: rw [← prod_natCast, Finset.prod_Ico_id_eq_factorial, wilsons_lemma]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h1 : n ≠ 1
⊢ Prime n
have inl : ∀ (h : Eq (α := ZMod 0) (↑(HSub.hSub (α := ℕ) 0 1)! : ZMod 0) (-1)) (h1 : Ne (α := ℕ) 0 1), Prime 0
Tactic: rcases eq_or_ne n 0 with (rfl | h0)
Cleared hypotheses: n, h, h1
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h1 : n ≠ 1
inl : ∀ (h : Eq (α := ZMod 0) (↑(HSub.hSub (α := ℕ) 0 1)! : ZMod 0) (-1)) (h1 : Ne (α := ℕ) 0 1), Prime 0
⊢ Prime n
have inr : ∀ (h0 : n ≠ 0), Prime n
Tactic: rcases eq_or_ne n 0 with (rfl | h0)
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (hypothesis)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h1 : n ≠ 1
h0 : n ≠ 0
⊢ Prime n
have h1₁ : 1 < n
Tactic: replace h1 : 1 < n := n.two_le_iff.mpr ⟨h0, h1⟩
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
⊢ Prime n
have inr : ∀ (h2 : ¬Prime n), False
Tactic: by_contra h2
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
⊢ False
have inr : ∀ (m : ℕ) (hm1 : m ∣ n) (hm2 : 1 < m) (hm3 : m < n), False
Tactic: obtain ⟨m, hm1, hm2 : 1 < m, hm3⟩ := exists_dvd_of_not_prime2 h1 h2
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (hypothesis)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
⊢ False
have hm : m ∣ (n - 1)!
Tactic: have hm : m ∣ (n - 1)! := Nat.dvd_factorial (pos_of_gt hm2) (le_pred_of_lt hm3)
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-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
have inr : n ∣ (n - 1)! + 1
Tactic: refine hm2.ne' (Nat.dvd_one.mp ((Nat.dvd_add_right hm).mp (hm1.trans ?_)))
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-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
have inr : Eq (α := ZMod n) (↑((n - 1)! + 1) : ZMod n) 0
Tactic: rw [← ZMod.natCast_eq_zero_iff, cast_add, cast_one, h, neg_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
inr : Eq (α := ZMod n) (↑((n - 1)! + 1) : ZMod n) 0
⊢ n ∣ (n - 1)! + 1
have inr₁ : HAdd.hAdd (α := ZMod n) (↑(n - 1)! : ZMod n) (↑1 : ZMod n) = 0
Tactic: rw [← ZMod.natCast_eq_zero_iff, cast_add, cast_one, h, neg_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
inr : Eq (α := ZMod n) (↑((n - 1)! + 1) : ZMod n) 0
inr₁ : HAdd.hAdd (α := ZMod n) (↑(n - 1)! : ZMod n) (↑1 : ZMod n) = 0
⊢ n ∣ (n - 1)! + 1
have inr₂ : HAdd.hAdd (α := ZMod n) (↑(n - 1)! : ZMod n) 1 = 0
Tactic: rw [← ZMod.natCast_eq_zero_iff, cast_add, cast_one, h, neg_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
inr : Eq (α := ZMod n) (↑((n - 1)! + 1) : ZMod n) 0
inr₁ : HAdd.hAdd (α := ZMod n) (↑(n - 1)! : ZMod n) (↑1 : ZMod n) = 0
inr₂ : HAdd.hAdd (α := ZMod n) (↑(n - 1)! : ZMod n) 1 = 0
⊢ n ∣ (n - 1)! + 1
have inr₃ : HAdd.hAdd (α := ZMod n) (-1) 1 = 0
Tactic: rw [← ZMod.natCast_eq_zero_iff, cast_add, cast_one, h, neg_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
inr : Eq (α := ZMod n) (↑((n - 1)! + 1) : ZMod n) 0
inr₁ : HAdd.hAdd (α := ZMod n) (↑(n - 1)! : ZMod n) (↑1 : ZMod n) = 0
inr₂ : HAdd.hAdd (α := ZMod n) (↑(n - 1)! : ZMod n) 1 = 0
inr₃ : HAdd.hAdd (α := ZMod n) (-1) 1 = 0
⊢ n ∣ (n - 1)! + 1
have inr₄ : Eq (α := ZMod n) 0 0
Tactic: rw [← ZMod.natCast_eq_zero_iff, cast_add, cast_one, h, neg_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (goal)
Goal:
n : ℕ
h : n ≠ 1
⊢ Prime n ↔ Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
have refine : ∀ (h1 : Prime n), Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
Tactic: refine ⟨fun h1 => ?_, fun h2 => prime_of_fac_equiv_neg_one h2 h⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Wilson (hypothesis)
Goal:
n : ℕ
h : n ≠ 1
h1 : Prime n
⊢ Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
have this : Fact (Prime n)
Tactic: haveI := Fact.mk h1
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
x : ℝ
⊢ bernoulliFun 1 x = x - 1 / 2
have simp : HDiv.hDiv (α := ℝ) (-1) 2 + x = x - 2⁻¹
Tactic: simp [bernoulliFun, Polynomial.bernoulli_def, Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
x : ℝ
⊢ bernoulliFun 2 x = HPow.hPow (β := ℕ) x 2 - x + 6⁻¹
have simp : 6⁻¹ + -x + HPow.hPow (β := ℕ) x 2 = HPow.hPow (β := ℕ) x 2 - x + 6⁻¹
Tactic: simp [bernoulliFun, Polynomial.bernoulli_def, Finset.sum_range_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
⊢ bernoulliFun k 0 = (↑(bernoulli k) : ℝ)
have rw : Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = (↑(bernoulli k) : ℝ)
Tactic: rw [bernoulliFun, Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
rw : Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = (↑(bernoulli k) : ℝ)
⊢ bernoulliFun k 0 = (↑(bernoulli k) : ℝ)
have rw₁ : Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (Polynomial.eval 0 (Polynomial.bernoulli k)) : ℝ) ((↑(bernoulli k) : ℝ) : ℝ)
Tactic: rw [bernoulliFun, Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
rw : Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = (↑(bernoulli k) : ℝ)
rw₁ :
  Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (Polynomial.eval 0 (Polynomial.bernoulli k)) : ℝ)
    ((↑(bernoulli k) : ℝ) : ℝ)
⊢ bernoulliFun k 0 = (↑(bernoulli k) : ℝ)
have rw₂ : Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli k) : ℝ) ((↑(bernoulli k) : ℝ) : ℝ)
Tactic: rw [bernoulliFun, Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
rw : Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = (↑(bernoulli k) : ℝ)
rw₁ :
  Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (Polynomial.eval 0 (Polynomial.bernoulli k)) : ℝ)
    ((↑(bernoulli k) : ℝ) : ℝ)
rw₂ : Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli k) : ℝ) ((↑(bernoulli k) : ℝ) : ℝ)
⊢ bernoulliFun k 0 = (↑(bernoulli k) : ℝ)
have rw₃ : Eq (α := ℝ) (↑(bernoulli k) : ℝ) (↑(bernoulli k) : ℝ)
Tactic: rw [bernoulliFun, Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 1
⊢ bernoulliFun k 1 = bernoulliFun k 0
have rw : bernoulliFun k 1 = (↑(bernoulli k) : ℝ)
Tactic: rw [bernoulliFun_eval_zero, bernoulliFun, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one,
    bernoulli_eq_bernoulli'_of_ne_one hk, eq_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 1
rw : bernoulliFun k 1 = (↑(bernoulli k) : ℝ)
⊢ bernoulliFun k 1 = bernoulliFun k 0
have rw₁ : Polynomial.eval 1 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = (↑(bernoulli k) : ℝ)
Tactic: rw [bernoulliFun_eval_zero, bernoulliFun, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one,
    bernoulli_eq_bernoulli'_of_ne_one hk, eq_ratCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ZetaValues (goal)
Goal:
k : ℕ
hk : k ≠ 1
rw : bernoulliFun k 1 = (↑(bernoulli k) : ℝ)
rw₁ : Polynomial.eval 1 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = (↑(bernoulli k) : ℝ)
⊢ bernoulliFun k 1 = bernoulliFun k 0
have rw₂ : Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (Polynomial.eval 1 (Polynomial.bernoulli k)) : ℝ) ((↑(bernoulli k) : ℝ) : ℝ)
Tactic: rw [bernoulliFun_eval_zero, bernoulliFun, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one,
    bernoulli_eq_bernoulli'_of_ne_one hk, eq_ratCast]