-- Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean
theorem mod_four_eq_three_of_nat_prime_of_prime (p : ℕ) [hp : Fact p.Prime]
    (hpi : Prime (p : ℤ[i])) : p % 4 = 3 :=
  hp.1.eq_two_or_odd.elim
    (fun hp2 => by
      have := hpi.irreducible.isUnit_or_isUnit (a := ⟨1, 1⟩) (b := ⟨1, -1⟩)
      simp [hp2, Zsqrtd.ext_iff, ← norm_eq_one_iff, norm_def] at this)
    fun hp1 =>
    by_contradiction fun hp3 : p % 4 ≠ 3 => by
      have hp41 : p % 4 = 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
x✝ : ↑p ∣ { re := ↑k, im := -1 }
x : ℤ[i]
hx : { re := ↑k, im := -1 } = ↑p * x
hx0 : x = 0
⊢ -1 = 0

Tactic:
simpa [hx0] using congr_arg Zsqrtd.im hx

Result:
no goals

Proof state:
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
⊢ False

Tactic:
obtain ⟨y, hy⟩ := hpk

Result:
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ False

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ { re := ↑k, im := 1 } * { re := ↑k, im := -1 } = ↑p * ↑y

Tactic:
rw [← hkmul, ← Nat.cast_mul p, ← hy]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ ↑k ^ 2 + 1 = ↑(k ^ 2 + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
⊢ k + k * k = k * (k + 1)

Tactic:
simp [add_comm, mul_add]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
x✝ : ↑p ∣ { re := ↑k, im := -1 }
x : ℤ[i]
hx : { re := ↑k, im := -1 } = ↑p * x
⊢ (Zsqrtd.norm (↑p * x)).natAbs = { re := ↑k, im := -1 }.norm.natAbs

Tactic:
rw [hx]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
x✝ : ↑p ∣ { re := ↑k, im := 1 }
x : ℤ[i]
hx : { re := ↑k, im := 1 } = ↑p * x
hx0 : x = 0
⊢ 1 = 0

Tactic:
simpa [hx0] using congr_arg Zsqrtd.im hx

Result:
no goals

Proof state:
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
⊢ False

Tactic:
have hkmul : (k ^ 2 + 1 : ℤ[i]) = ⟨k, 1⟩ * ⟨k, -1⟩ := by ext <;> simp [sq]

Result:
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
⊢ False

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
x✝ : ↑p ∣ { re := ↑k, im := 1 }
x : ℤ[i]
hx : { re := ↑k, im := 1 } = ↑p * x
⊢ (Zsqrtd.norm (↑p * x)).natAbs = { re := ↑k, im := 1 }.norm.natAbs

Tactic:
rw [hx]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
x✝ : ↑p ∣ { re := ↑k, im := 1 }
x : ℤ[i]
hx : { re := ↑k, im := 1 } = ↑p * x
hx0 : x = 0
⊢ 1 ≠ 0

Tactic:
decide

Result:
no goals

Proof state:
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ False

Tactic:
have := hpi.2.2 ⟨k, 1⟩ ⟨k, -1⟩ ⟨y, by rw [← hkmul, ← Nat.cast_mul p, ← hy]; simp⟩

Result:
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
this : ↑p ∣ { re := ↑k, im := 1 } ∨ ↑p ∣ { re := ↑k, im := -1 }
⊢ False

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
⊢ 1 ≠ 3

Tactic:
decide

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
⊢ p ∣ k ^ 2 + 1

Tactic:
rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one,
  ← hk, neg_add_cancel]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ZMod p
hk : -1 = k * k
⊢ ∃ k', ∃ (_ : k' < p), ↑k' = k

Tactic:
exact ⟨k.val, k.val_lt, ZMod.natCast_zmod_val k⟩

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
⊢ p % 4 = 1

Tactic:
omega

Result:
no goals

Proof state:
case bc
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
⊢ 1 ≤ k

Tactic:
exact (Nat.pos_of_ne_zero fun (hk0 : k = 0) => by clear_aux_decl; simp_all [pow_succ'])

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
x✝ : ↑p ∣ { re := ↑k, im := 1 }
x : ℤ[i]
hx : { re := ↑k, im := 1 } = ↑p * x
⊢ { re := ↑k, im := 1 }.norm.natAbs < (Zsqrtd.norm ↑p).natAbs

Tactic:
simpa [add_comm, Zsqrtd.norm] using hkltp

Result:
no goals