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
⊢ ↑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
Tactic:
suffices : a + (p - a) = p
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)

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