[GOAL]
p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ∃ a b, a ^ 2 + b ^ 2 = p
[PROOFSTEP]
apply sq_add_sq_of_nat_prime_of_not_irreducible p
[GOAL]
p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ¬Irreducible ↑p
[PROOFSTEP]
rwa [PrincipalIdealRing.irreducible_iff_prime, prime_iff_mod_four_eq_three_of_nat_prime p]
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ a * b = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2
[PROOFSTEP]
rw [ha, hb]
[GOAL]
R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ (x ^ 2 + y ^ 2) * (u ^ 2 + v ^ 2) = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2
[PROOFSTEP]
ring
[GOAL]
a b x y u v : ℕ
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ ∃ r s, a * b = r ^ 2 + s ^ 2
[PROOFSTEP]
zify at ha hb ⊢
[GOAL]
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
⊢ ∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2
[PROOFSTEP]
obtain ⟨r, s, h⟩ := _root_.sq_add_sq_mul ha hb
[GOAL]
case intro.intro
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
r s : ℤ
h : ↑a * ↑b = r ^ 2 + s ^ 2
⊢ ∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2
[PROOFSTEP]
refine' ⟨r.natAbs, s.natAbs, _⟩
[GOAL]
case intro.intro
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
r s : ℤ
h : ↑a * ↑b = r ^ 2 + s ^ 2
⊢ ↑a * ↑b = ↑(Int.natAbs r) ^ 2 + ↑(Int.natAbs s) ^ 2
[PROOFSTEP]
simpa only [Int.coe_natAbs, sq_abs]
[GOAL]
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
⊢ IsSquare (-1)
[PROOFSTEP]
let f : ZMod n →+* ZMod m := ZMod.castHom hd _
[GOAL]
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (-1)
[PROOFSTEP]
rw [← RingHom.map_one f, ← RingHom.map_neg]
[GOAL]
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (↑f (-1))
[PROOFSTEP]
exact hs.map f
[GOAL]
m n : ℕ
hc : Nat.coprime m n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1)
[PROOFSTEP]
have : IsSquare (-1 : ZMod m × ZMod n) :=
  by
  rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]
  obtain ⟨x, hx⟩ := hm
  obtain ⟨y, hy⟩ := hn
  rw [hx, hy]
  exact ⟨(x, y), rfl⟩
[GOAL]
m n : ℕ
hc : Nat.coprime m n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1)
[PROOFSTEP]
rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]
[GOAL]
m n : ℕ
hc : Nat.coprime m n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1, -1)
[PROOFSTEP]
obtain ⟨x, hx⟩ := hm
[GOAL]
case intro
m n : ℕ
hc : Nat.coprime m n
hn : IsSquare (-1)
x : ZMod m
hx : -1 = x * x
⊢ IsSquare (-1, -1)
[PROOFSTEP]
obtain ⟨y, hy⟩ := hn
[GOAL]
case intro.intro
m n : ℕ
hc : Nat.coprime m n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (-1, -1)
[PROOFSTEP]
rw [hx, hy]
[GOAL]
case intro.intro
m n : ℕ
hc : Nat.coprime m n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (x * x, y * y)
[PROOFSTEP]
exact ⟨(x, y), rfl⟩
[GOAL]
m n : ℕ
hc : Nat.coprime m n
hm : IsSquare (-1)
hn : IsSquare (-1)
this : IsSquare (-1)
⊢ IsSquare (-1)
[PROOFSTEP]
simpa only [RingEquiv.map_neg_one] using this.map (ZMod.chineseRemainder hc).symm
[GOAL]
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
⊢ p % 4 ≠ 3
[PROOFSTEP]
obtain ⟨y, h⟩ := ZMod.isSquare_neg_one_of_dvd hp hs
[GOAL]
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : -1 = y * y
⊢ p % 4 ≠ 3
[PROOFSTEP]
rw [← sq, eq_comm, show (-1 : ZMod p) = -1 ^ 2 by ring] at h 
[GOAL]
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1
⊢ -1 = -1 ^ 2
[PROOFSTEP]
ring
[GOAL]
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
⊢ p % 4 ≠ 3
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hpp⟩
[GOAL]
case intro
p n : ℕ
hpp : Prime p
hp : p ∣ n
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
this : Fact (Prime p)
⊢ p % 4 ≠ 3
[PROOFSTEP]
exact ZMod.mod_four_ne_three_of_sq_eq_neg_sq' one_ne_zero h
[GOAL]
n : ℕ
hn : Squarefree n
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
refine' ⟨fun H q hqp hqd => hqp.mod_four_ne_three_of_dvd_isSquare_neg_one hqd H, fun H => _⟩
[GOAL]
n : ℕ
hn : Squarefree n
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ IsSquare (-1)
[PROOFSTEP]
induction' n using induction_on_primes with p n hpp ih
[GOAL]
case h₀
n : ℕ
hn✝ : Squarefree n
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
hn : Squarefree 0
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ 0 → q % 4 ≠ 3
⊢ IsSquare (-1)
[PROOFSTEP]
exact False.elim (hn.ne_zero rfl)
[GOAL]
case h₁
n : ℕ
hn✝ : Squarefree n
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
hn : Squarefree 1
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ 1 → q % 4 ≠ 3
⊢ IsSquare (-1)
[PROOFSTEP]
exact ⟨0, by simp only [Fin.zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]⟩
[GOAL]
n : ℕ
hn✝ : Squarefree n
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
hn : Squarefree 1
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ 1 → q % 4 ≠ 3
⊢ -1 = 0 * 0
[PROOFSTEP]
simp only [Fin.zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]
[GOAL]
case h
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
⊢ IsSquare (-1)
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hpp⟩
[GOAL]
case h
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
⊢ IsSquare (-1)
[PROOFSTEP]
have hcp : p.coprime n := by
  by_contra hc
  exact hpp.not_unit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
[GOAL]
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
⊢ Nat.coprime p n
[PROOFSTEP]
by_contra hc
[GOAL]
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hc : ¬Nat.coprime p n
⊢ False
[PROOFSTEP]
exact hpp.not_unit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
[GOAL]
case h
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hcp : Nat.coprime p n
⊢ IsSquare (-1)
[PROOFSTEP]
have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr (H hpp (dvd_mul_right p n))
[GOAL]
case h
n✝ : ℕ
hn✝ : Squarefree n✝
H✝ : ∀ {q : ℕ}, Nat.Prime q → q ∣ n✝ → q % 4 ≠ 3
p n : ℕ
hpp : Nat.Prime p
ih : Squarefree n → (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → IsSquare (-1)
hn : Squarefree (p * n)
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ p * n → q % 4 ≠ 3
this : Fact (Nat.Prime p)
hcp : Nat.coprime p n
hp₁ : IsSquare (-1)
⊢ IsSquare (-1)
[PROOFSTEP]
exact ZMod.isSquare_neg_one_mul hcp hp₁ (ih hn.of_mul_right fun hqp hqd => H hqp <| dvd_mul_of_dvd_right hqd _)
[GOAL]
n : ℕ
hn : Squarefree n
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
have help : ∀ a b : ZMod 4, a ≠ 3 → b ≠ 3 → a * b ≠ 3 := by decide
[GOAL]
n : ℕ
hn : Squarefree n
⊢ ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
[PROOFSTEP]
decide
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
rw [ZMod.isSquare_neg_one_iff hn]
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
refine' ⟨_, fun H q _ => H⟩
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ (∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3) → ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
intro H
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
[PROOFSTEP]
refine' @induction_on_primes _ _ _ (fun p q hp hq hpq => _)
[GOAL]
case refine'_1
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ 0 ∣ n → 0 % 4 ≠ 3
[PROOFSTEP]
exact fun _ => by norm_num
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
x✝ : 0 ∣ n
⊢ 0 % 4 ≠ 3
[PROOFSTEP]
norm_num
[GOAL]
case refine'_2
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
⊢ 1 ∣ n → 1 % 4 ≠ 3
[PROOFSTEP]
exact fun _ => by norm_num
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
x✝ : 1 ∣ n
⊢ 1 % 4 ≠ 3
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hp : Nat.Prime p
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
⊢ p * q % 4 ≠ 3
[PROOFSTEP]
replace hp := H hp (dvd_of_mul_right_dvd hpq)
[GOAL]
case refine'_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
hp : p % 4 ≠ 3
⊢ p * q % 4 ≠ 3
[PROOFSTEP]
replace hq := hq (dvd_of_mul_left_dvd hpq)
[GOAL]
case refine'_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3
hq : q % 4 ≠ 3
⊢ p * q % 4 ≠ 3
[PROOFSTEP]
rw [show 3 = 3 % 4 by norm_num, Ne.def, ← ZMod.nat_cast_eq_nat_cast_iff'] at hp hq ⊢
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3
hq : q % 4 ≠ 3
⊢ 3 = 3 % 4
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3 % 4
hq : q % 4 ≠ 3
⊢ 3 = 3 % 4
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3 % 4
hq : q % 4 ≠ 3 % 4
⊢ 3 = 3 % 4
[PROOFSTEP]
norm_num
[GOAL]
case refine'_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬↑p = ↑3
hq : ¬↑q = ↑3
⊢ ¬↑(p * q) = ↑3
[PROOFSTEP]
rw [Nat.cast_mul]
[GOAL]
case refine'_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ {q : ℕ}, Nat.Prime q → q ∣ n → q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬↑p = ↑3
hq : ¬↑q = ↑3
⊢ ¬↑p * ↑q = ↑3
[PROOFSTEP]
exact help p q hp hq
[GOAL]
n : ℕ
h : IsSquare (-1)
⊢ ∃ x y, n = x ^ 2 + y ^ 2
[PROOFSTEP]
induction' n using induction_on_primes with p n hpp ih
[GOAL]
case h₀
n : ℕ
h✝ : IsSquare (-1)
h : IsSquare (-1)
⊢ ∃ x y, 0 = x ^ 2 + y ^ 2
[PROOFSTEP]
exact ⟨0, 0, rfl⟩
[GOAL]
case h₁
n : ℕ
h✝ : IsSquare (-1)
h : IsSquare (-1)
⊢ ∃ x y, 1 = x ^ 2 + y ^ 2
[PROOFSTEP]
exact ⟨0, 1, rfl⟩
[GOAL]
case h
n✝ : ℕ
h✝ : IsSquare (-1)
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hpp⟩
[GOAL]
case h
n✝ : ℕ
h✝ : IsSquare (-1)
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
[PROOFSTEP]
have hp : IsSquare (-1 : ZMod p) := ZMod.isSquare_neg_one_of_dvd ⟨n, rfl⟩ h
[GOAL]
case h
n✝ : ℕ
h✝ : IsSquare (-1)
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
[PROOFSTEP]
obtain ⟨u, v, huv⟩ := Nat.Prime.sq_add_sq (ZMod.exists_sq_eq_neg_one_iff.mp hp)
[GOAL]
case h.intro.intro
n✝ : ℕ
h✝ : IsSquare (-1)
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
u v : ℕ
huv : u ^ 2 + v ^ 2 = p
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
[PROOFSTEP]
obtain ⟨x, y, hxy⟩ := ih (ZMod.isSquare_neg_one_of_dvd ⟨p, mul_comm _ _⟩ h)
[GOAL]
case h.intro.intro.intro.intro
n✝ : ℕ
h✝ : IsSquare (-1)
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
u v : ℕ
huv : u ^ 2 + v ^ 2 = p
x y : ℕ
hxy : n = x ^ 2 + y ^ 2
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
[PROOFSTEP]
exact Nat.sq_add_sq_mul huv.symm hxy
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
⊢ IsSquare (-1)
[PROOFSTEP]
obtain ⟨u, v, huv⟩ : IsCoprime x n :=
  by
  have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow
  rw [show y ^ 2 = n + -1 * x ^ 2 by rw [h]; ring] at hc2 
  exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
⊢ IsCoprime x n
[PROOFSTEP]
have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (y ^ 2)
⊢ IsCoprime x n
[PROOFSTEP]
rw [show y ^ 2 = n + -1 * x ^ 2 by rw [h]; ring] at hc2 
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (y ^ 2)
⊢ y ^ 2 = n + -1 * x ^ 2
[PROOFSTEP]
rw [h]
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (y ^ 2)
⊢ y ^ 2 = x ^ 2 + y ^ 2 + -1 * x ^ 2
[PROOFSTEP]
ring
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (n + -1 * x ^ 2)
⊢ IsCoprime x n
[PROOFSTEP]
exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right
[GOAL]
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
⊢ IsSquare (-1)
[PROOFSTEP]
have H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v) := by
  linear_combination -u ^ 2 * h + (n * v - u * x - 1) * huv
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
⊢ u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
[PROOFSTEP]
linear_combination -u ^ 2 * h + (n * v - u * x - 1) * huv
[GOAL]
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ IsSquare (-1)
[PROOFSTEP]
refine' ⟨u * y, _⟩
[GOAL]
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑u * ↑y * (↑u * ↑y)
[PROOFSTEP]
conv_rhs => tactic => norm_cast
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
| ↑u * ↑y * (↑u * ↑y)
[PROOFSTEP]
tactic => norm_cast
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
| ↑u * ↑y * (↑u * ↑y)
[PROOFSTEP]
tactic => norm_cast
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
| ↑u * ↑y * (↑u * ↑y)
[PROOFSTEP]
tactic => norm_cast
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ ↑u * ↑y * (↑u * ↑y) = ?m.37150
[PROOFSTEP]
norm_cast
[GOAL]
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑(u * y * (u * y))
[PROOFSTEP]
rw [(by norm_cast : (-1 : ZMod n.natAbs) = (-1 : ℤ))]
[GOAL]
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑(-1)
[PROOFSTEP]
norm_cast
[GOAL]
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ ↑(-1) = ↑(u * y * (u * y))
[PROOFSTEP]
exact (ZMod.int_cast_eq_int_cast_iff_dvd_sub _ _ _).mpr (Int.natAbs_dvd.mpr ⟨_, H⟩)
[GOAL]
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hc : Nat.coprime x y
⊢ IsSquare (-1)
[PROOFSTEP]
zify at h 
[GOAL]
n x y : ℕ
hc : Nat.coprime x y
h : ↑n = ↑x ^ 2 + ↑y ^ 2
⊢ IsSquare (-1)
[PROOFSTEP]
exact ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime h hc.isCoprime
[GOAL]
n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) → ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
rintro ⟨x, y, h⟩
[GOAL]
case mp.intro.intro
n x y : ℕ
h : n = x ^ 2 + y ^ 2
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
by_cases hxy : x = 0 ∧ y = 0
[GOAL]
case pos
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
exact
  ⟨0, 1, by rw [h, hxy.1, hxy.2, zero_pow zero_lt_two, add_zero, zero_mul],
    ⟨0, by rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]⟩⟩
[GOAL]
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ n = 0 ^ 2 * 1
[PROOFSTEP]
rw [h, hxy.1, hxy.2, zero_pow zero_lt_two, add_zero, zero_mul]
[GOAL]
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ -1 = 0 * 0
[PROOFSTEP]
rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]
[GOAL]
case neg
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
have hg := Nat.pos_of_ne_zero (mt Nat.gcd_eq_zero_iff.mp hxy)
[GOAL]
case neg
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < gcd x y
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
obtain ⟨g, x₁, y₁, _, h₂, h₃, h₄⟩ := Nat.exists_coprime' hg
[GOAL]
case neg.intro.intro.intro.intro.intro.intro
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < gcd x y
g : ℕ
x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : coprime x₁ y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
exact ⟨g, x₁ ^ 2 + y₁ ^ 2, by rw [h, h₃, h₄]; ring, ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime rfl h₂⟩
[GOAL]
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < gcd x y
g : ℕ
x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : coprime x₁ y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ n = g ^ 2 * (x₁ ^ 2 + y₁ ^ 2)
[PROOFSTEP]
rw [h, h₃, h₄]
[GOAL]
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < gcd x y
g : ℕ
x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : coprime x₁ y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ (x₁ * g) ^ 2 + (y₁ * g) ^ 2 = g ^ 2 * (x₁ ^ 2 + y₁ ^ 2)
[PROOFSTEP]
ring
[GOAL]
case mpr
n : ℕ
⊢ (∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) → ∃ x y, n = x ^ 2 + y ^ 2
[PROOFSTEP]
rintro ⟨a, b, h₁, h₂⟩
[GOAL]
case mpr.intro.intro.intro
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
⊢ ∃ x y, n = x ^ 2 + y ^ 2
[PROOFSTEP]
obtain ⟨x', y', h⟩ := Nat.eq_sq_add_sq_of_isSquare_mod_neg_one h₂
[GOAL]
case mpr.intro.intro.intro.intro.intro
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ ∃ x y, n = x ^ 2 + y ^ 2
[PROOFSTEP]
exact ⟨a * x', a * y', by rw [h₁, h]; ring⟩
[GOAL]
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ n = (a * x') ^ 2 + (a * y') ^ 2
[PROOFSTEP]
rw [h₁, h]
[GOAL]
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ a ^ 2 * (x' ^ 2 + y' ^ 2) = (a * x') ^ 2 + (a * y') ^ 2
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn₀)
[GOAL]
case inl
⊢ (∃ x y, 0 = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q 0)
[PROOFSTEP]
exact
  ⟨fun _ q _ _ => (@padicValNat.zero q).symm ▸ even_zero, fun _ => ⟨0, 0, rfl⟩⟩
    -- now `0 < n`
[GOAL]
case inr
n : ℕ
hn₀ : n > 0
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
[PROOFSTEP]
rw [Nat.eq_sq_add_sq_iff_eq_sq_mul]
[GOAL]
case inr
n : ℕ
hn₀ : n > 0
⊢ (∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
[PROOFSTEP]
refine' ⟨fun H q hq h => _, fun H => _⟩
[GOAL]
case inr.refine'_1
n : ℕ
hn₀ : n > 0
H : ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
q : ℕ
hq : Prime q
h : q % 4 = 3
⊢ Even (padicValNat q n)
[PROOFSTEP]
obtain ⟨a, b, h₁, h₂⟩ := H
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
⊢ Even (padicValNat q n)
[PROOFSTEP]
have hqb := padicValNat.eq_zero_of_not_dvd fun hf => (hq.mod_four_ne_three_of_dvd_isSquare_neg_one hf h₂) h
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
⊢ Even (padicValNat q n)
[PROOFSTEP]
have hab : a ^ 2 * b ≠ 0 := h₁ ▸ hn₀.ne'
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
⊢ Even (padicValNat q n)
[PROOFSTEP]
have ha₂ := left_ne_zero_of_mul hab
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
⊢ Even (padicValNat q n)
[PROOFSTEP]
have ha := mt sq_eq_zero_iff.mpr ha₂
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
⊢ Even (padicValNat q n)
[PROOFSTEP]
have hb := right_ne_zero_of_mul hab
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
⊢ Even (padicValNat q n)
[PROOFSTEP]
haveI hqi : Fact q.Prime := ⟨hq⟩
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
hqi : Fact (Prime q)
⊢ Even (padicValNat q n)
[PROOFSTEP]
simp_rw [h₁, padicValNat.mul ha₂ hb, padicValNat.pow 2 ha, hqb, add_zero]
[GOAL]
case inr.refine'_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
hqi : Fact (Prime q)
⊢ Even (2 * padicValNat q a)
[PROOFSTEP]
exact even_two_mul _
[GOAL]
case inr.refine'_2
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
obtain ⟨b, a, hb₀, ha₀, hab, hb⟩ := Nat.sq_mul_squarefree_of_pos hn₀
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
[PROOFSTEP]
refine' ⟨a, b, hab.symm, (ZMod.isSquare_neg_one_iff hb).mpr fun {q} hqp hqb hq4 => _⟩
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
⊢ False
[PROOFSTEP]
refine' Nat.odd_iff_not_even.mp _ (H hqp hq4)
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
⊢ Odd (padicValNat q n)
[PROOFSTEP]
have hqb' : padicValNat q b = 1 :=
  b.factorization_def hqp ▸
    le_antisymm (Nat.Squarefree.factorization_le_one _ hb) ((hqp.dvd_iff_one_le_factorization hb₀.ne').mp hqb)
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
⊢ Odd (padicValNat q n)
[PROOFSTEP]
haveI hqi : Fact q.Prime := ⟨hqp⟩
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
hqi : Fact (Prime q)
⊢ Odd (padicValNat q n)
[PROOFSTEP]
simp_rw [← hab, padicValNat.mul (pow_ne_zero 2 ha₀.ne') hb₀.ne', hqb', padicValNat.pow 2 ha₀.ne']
[GOAL]
case inr.refine'_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
hqi : Fact (Prime q)
⊢ Odd (2 * padicValNat q a + 1)
[PROOFSTEP]
exact odd_two_mul_add_one _
