internlm/Lean-Github huggingface dataset:
Theorem: Section15Sheet7Solutions.wilson_theorem
Proof 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]
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.wilson_theorem
Proof 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
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
p : ℕ
hp : Nat.Prime p
hp2 : ∃ n, p = 4 * n + 1
⊢ ∃ i, i ^ 2 = -1
Tactic:
cases' hp2 with n hn
Proof state after:
case intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
⊢ ∃ i, i ^ 2 = -1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
⊢ ∃ i, i ^ 2 = -1
Tactic:
set i := ∏ j in Finset.Icc 1 (2 * n), (j : ZMod p) with hi
Proof state after:
case intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
⊢ ∃ i, i ^ 2 = -1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
⊢ ∃ i, i ^ 2 = -1
Tactic:
have h1 : ∏ j in Finset.Icc 1 (2 * n), (-1 : ZMod p) = 1
Proof state after:
case h1
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
⊢ ∏ j in Finset.Icc 1 (2 * n), -1 = 1

case intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
⊢ ∃ i, i ^ 2 = -1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
⊢ ∃ i, i ^ 2 = -1
Tactic:
have h2 : ∏ j in Finset.Icc 1 (2 * n), (-j : ZMod p) = i
Proof state after:
case h2
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
⊢ ∏ j in Finset.Icc 1 (2 * n), -↑j = i

case intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
⊢ ∃ i, i ^ 2 = -1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
⊢ ∃ i, i ^ 2 = -1
Tactic:
have h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), (j : ZMod p) = i
Proof state after:
case h3
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
⊢ ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i

case intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ ∃ i, i ^ 2 = -1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ ∃ i, i ^ 2 = -1
Tactic:
use i
Proof state after:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ i ^ 2 = -1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ i ^ 2 = -1
Tactic:
rw [pow_two]
Proof state after:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ i * i = -1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ i * i = -1
Tactic:
nth_rw 1 [hi]
Proof state after:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ (∏ j in Finset.Icc 1 (2 * n), ↑j) * i = -1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ (∏ j in Finset.Icc 1 (2 * n), ↑j) * i = -1
Tactic:
rw [← h3]
Proof state after:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ (∏ j in Finset.Icc 1 (2 * n), ↑j) * ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = -1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ (∏ j in Finset.Icc 1 (2 * n), ↑j) * ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = -1
Tactic:
rw [← Finset.prod_union]
Proof state after:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ ∏ x in Finset.Icc 1 (2 * n) ∪ Finset.Icc (2 * n + 1) (4 * n), ↑x = -1

case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ Disjoint (Finset.Icc 1 (2 * n)) (Finset.Icc (2 * n + 1) (4 * n))
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h1
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
⊢ ∏ j in Finset.Icc 1 (2 * n), -1 = 1
Tactic:
rw [Finset.prod_const]
Proof state after:
case h1
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
⊢ (-1) ^ Finset.card (Finset.Icc 1 (2 * n)) = 1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h1
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
⊢ (-1) ^ Finset.card (Finset.Icc 1 (2 * n)) = 1
Tactic:
simp only [Nat.add_succ_sub_one, add_zero, Nat.card_Icc]
Proof state after:
case h1
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
⊢ (-1) ^ (2 * n) = 1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h1
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
⊢ (-1) ^ (2 * n) = 1
Tactic:
rw [pow_mul, neg_one_pow_two, one_pow]
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h2
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
⊢ ∏ j in Finset.Icc 1 (2 * n), -↑j = i
Tactic:
conv_lhs => rhs; ext; rw [neg_eq_neg_one_mul]
Proof state after:
case h2
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
⊢ ∏ x in Finset.Icc 1 (2 * n), -1 * ↑x = i
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h2
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
⊢ ∏ x in Finset.Icc 1 (2 * n), -1 * ↑x = i
Tactic:
rw [Finset.prod_mul_distrib, h1, one_mul]
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h3
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
⊢ ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
Tactic:
rw [← h2]
Proof state after:
case h3
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
⊢ ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = ∏ j in Finset.Icc 1 (2 * n), -↑j
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h3
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
⊢ ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = ∏ j in Finset.Icc 1 (2 * n), -↑j
Tactic:
apply Finset.prod_bij' (fun j _ => p - j) (fun j _ => p - j)  <;>
rintro a ha <;>
rw [Finset.mem_Icc] at *
Proof state after:
case h3.hi
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ 1 ≤ p - a ∧ p - a ≤ 2 * n

case h3.hj
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 1 ≤ a ∧ a ≤ 2 * n
⊢ 2 * n + 1 ≤ p - a ∧ p - a ≤ 4 * n

case h3.left_inv
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ p - (p - a) = a

case h3.right_inv
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 1 ≤ a ∧ a ≤ 2 * n
⊢ p - (p - a) = a

case h3.h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ ↑a = -↑(p - a)
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h3.hi
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ 1 ≤ p - a ∧ p - a ≤ 2 * n

case h3.hj
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 1 ≤ a ∧ a ≤ 2 * n
⊢ 2 * n + 1 ≤ p - a ∧ p - a ≤ 4 * n

case h3.left_inv
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ p - (p - a) = a

case h3.right_inv
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 1 ≤ a ∧ a ≤ 2 * n
⊢ p - (p - a) = a

case h3.h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ ↑a = -↑(p - a)
Tactic:
rotate_right
Proof state after:
case h3.h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ ↑a = -↑(p - a)

case h3.hi
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ 1 ≤ p - a ∧ p - a ≤ 2 * n

case h3.hj
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 1 ≤ a ∧ a ≤ 2 * n
⊢ 2 * n + 1 ≤ p - a ∧ p - a ≤ 4 * n

case h3.left_inv
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ p - (p - a) = a

case h3.right_inv
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 1 ≤ a ∧ a ≤ 2 * n
⊢ p - (p - a) = a
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case this
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ a + (p - a) = p

case h3.hi
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ 1 ≤ p - a ∧ p - a ≤ 2 * n

case h3.hj
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 1 ≤ a ∧ a ≤ 2 * n
⊢ 2 * n + 1 ≤ p - a ∧ p - a ≤ 4 * n

case h3.left_inv
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
⊢ p - (p - a) = a

case h3.right_inv
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 1 ≤ a ∧ a ≤ 2 * n
⊢ p - (p - a) = a
Tactic:
all_goals omega
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h3.h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
this : a + (p - a) = p
⊢ ↑a = -↑(p - a)
Tactic:
rw [eq_neg_iff_add_eq_zero]
Proof state after:
case h3.h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
this : a + (p - a) = p
⊢ ↑a + ↑(p - a) = 0
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h3.h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
this : a + (p - a) = p
⊢ ↑a + ↑(p - a) = 0
Tactic:
norm_cast
Proof state after:
case h3.h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
this : a + (p - a) = p
⊢ ↑(a + (p - a)) = 0
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h3.h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 2 * n + 1 ≤ a ∧ a ≤ 4 * n
this : a + (p - a) = p
⊢ ↑(a + (p - a)) = 0
Tactic:
simp [this]
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h3.right_inv
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
a : ℕ
ha : 1 ≤ a ∧ a ≤ 2 * n
⊢ p - (p - a) = a
Tactic:
omega
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ ∏ x in Finset.Icc 1 (2 * n) ∪ Finset.Icc (2 * n + 1) (4 * n), ↑x = -1
Tactic:
convert_to ∏ j in Finset.Icc 1 (4 * n), (j : ZMod p) = -1
Proof state after:
case h.e'_2
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ ∏ x in Finset.Icc 1 (2 * n) ∪ Finset.Icc (2 * n + 1) (4 * n), ↑x = ∏ j in Finset.Icc 1 (4 * n), ↑j

case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = -1
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h.e'_2
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ ∏ x in Finset.Icc 1 (2 * n) ∪ Finset.Icc (2 * n + 1) (4 * n), ↑x = ∏ j in Finset.Icc 1 (4 * n), ↑j
Tactic:
congr
Proof state after:
case h.e'_2.e_s
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ Finset.Icc 1 (2 * n) ∪ Finset.Icc (2 * n + 1) (4 * n) = Finset.Icc 1 (4 * n)
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h.e'_2.e_s
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ Finset.Icc 1 (2 * n) ∪ Finset.Icc (2 * n + 1) (4 * n) = Finset.Icc 1 (4 * n)
Tactic:
ext x
Proof state after:
case h.e'_2.e_s.a
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
⊢ x ∈ Finset.Icc 1 (2 * n) ∪ Finset.Icc (2 * n + 1) (4 * n) ↔ x ∈ Finset.Icc 1 (4 * n)
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h.e'_2.e_s.a
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
⊢ x ∈ Finset.Icc 1 (2 * n) ∪ Finset.Icc (2 * n + 1) (4 * n) ↔ x ∈ Finset.Icc 1 (4 * n)
Tactic:
rw [Finset.mem_union]
Proof state after:
case h.e'_2.e_s.a
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
⊢ x ∈ Finset.Icc 1 (2 * n) ∨ x ∈ Finset.Icc (2 * n + 1) (4 * n) ↔ x ∈ Finset.Icc 1 (4 * n)