Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four (FormalisingMathematics2024/Solutions/Section15numberTheory/Sheet8.lean)

State before:
p : ℕ
hp : Nat.Prime p
hp2 : ∃ n, p = 4 * n + 1
⊢ ∃ i, i ^ 2 = -1
Tactic:
cases' hp2 with n hn
State after:
case intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
⊢ ∃ i, i ^ 2 = -1

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
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

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
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

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
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

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
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

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
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

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]
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

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]
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

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]
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

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]
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))

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]
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

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]
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

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]
State after:
no goals

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]
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

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]
State after:
no goals

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]
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

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 *
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)

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
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

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
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

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
State after:
no goals

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]
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

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
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

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]
State after:
no goals

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
State after:
no goals

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
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

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
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)

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
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)

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]
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)

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) ∨ x ∈ Finset.Icc (2 * n + 1) (4 * n) ↔ x ∈ Finset.Icc 1 (4 * n)
Tactic:
simp only [Finset.mem_Icc]
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 : ℕ
⊢ 1 ≤ x ∧ x ≤ 2 * n ∨ 2 * n + 1 ≤ x ∧ x ≤ 4 * n ↔ 1 ≤ x ∧ x ≤ 4 * n

State before:
case h.e'_2.e_s.a.mpr
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 : ℕ
⊢ 1 ≤ x ∧ x ≤ 4 * n → 1 ≤ x ∧ x ≤ 2 * n ∨ 2 * n + 1 ≤ x ∧ x ≤ 4 * n
Tactic:
intros
State after:
case h.e'_2.e_s.a.mpr
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 : ℕ
a✝ : 1 ≤ x ∧ x ≤ 4 * n
⊢ 1 ≤ x ∧ x ≤ 2 * n ∨ 2 * n + 1 ≤ x ∧ x ≤ 4 * n

State before:
case h.e'_2.e_s.a.mpr
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 : ℕ
a✝ : 1 ≤ x ∧ x ≤ 4 * n
⊢ 1 ≤ x ∧ x ≤ 2 * n ∨ 2 * n + 1 ≤ x ∧ x ≤ 4 * n
Tactic:
omega
State after:
no goals

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 (4 * n), ↑j = -1
Tactic:
apply wilson_theorem hp hn
State after:
no goals

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
⊢ Disjoint (Finset.Icc 1 (2 * n)) (Finset.Icc (2 * n + 1) (4 * n))
Tactic:
rw [disjoint_iff_inf_le]
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
⊢ Finset.Icc 1 (2 * n) ⊓ Finset.Icc (2 * n + 1) (4 * n) ≤ ⊥

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
⊢ Finset.Icc 1 (2 * n) ⊓ Finset.Icc (2 * n + 1) (4 * n) ≤ ⊥
Tactic:
rintro x (hx : x ∈ _ ∩ _)
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 : ℕ
hx : x ∈ Finset.Icc 1 (2 * n) ∩ Finset.Icc (2 * n + 1) (4 * n)
⊢ x ∈ ⊥

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 : ℕ
hx : x ∈ Finset.Icc 1 (2 * n) ∩ Finset.Icc (2 * n + 1) (4 * n)
⊢ x ∈ ⊥
Tactic:
rw [Finset.mem_inter, Finset.mem_Icc, Finset.mem_Icc] at hx
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 : ℕ
hx : (1 ≤ x ∧ x ≤ 2 * n) ∧ 2 * n + 1 ≤ x ∧ x ≤ 4 * n
⊢ x ∈ ⊥

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 : ℕ
hx : (1 ≤ x ∧ x ≤ 2 * n) ∧ 2 * n + 1 ≤ x ∧ x ≤ 4 * n
⊢ x ∈ ⊥
Tactic:
rcases hx with ⟨⟨_, _⟩, _, _⟩
State after:
case h.intro.intro.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
x : ℕ
left✝¹ : 1 ≤ x
right✝¹ : x ≤ 2 * n
left✝ : 2 * n + 1 ≤ x
right✝ : x ≤ 4 * n
⊢ x ∈ ⊥

State before:
case h.intro.intro.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
x : ℕ
left✝¹ : 1 ≤ x
right✝¹ : x ≤ 2 * n
left✝ : 2 * n + 1 ≤ x
right✝ : x ≤ 4 * n
⊢ x ∈ ⊥
Tactic:
linarith
State after:
no goals