[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp2 : p = 2
x✝ : Irreducible ↑p
not_unit✝ : ¬IsUnit ↑p
h : ∀ (a b : ℤ[i]), ↑p = a * b → IsUnit a ∨ IsUnit b
⊢ False
[PROOFSTEP]
have := h ⟨1, 1⟩ ⟨1, -1⟩ (hp2.symm ▸ rfl)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp2 : p = 2
x✝ : Irreducible ↑p
not_unit✝ : ¬IsUnit ↑p
h : ∀ (a b : ℤ[i]), ↑p = a * b → IsUnit a ∨ IsUnit b
this : IsUnit { re := 1, im := 1 } ∨ IsUnit { re := 1, im := -1 }
⊢ False
[PROOFSTEP]
rw [← norm_eq_one_iff, ← norm_eq_one_iff] at this 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp2 : p = 2
x✝ : Irreducible ↑p
not_unit✝ : ¬IsUnit ↑p
h : ∀ (a b : ℤ[i]), ↑p = a * b → IsUnit a ∨ IsUnit b
this : Int.natAbs (Zsqrtd.norm { re := 1, im := 1 }) = 1 ∨ Int.natAbs (Zsqrtd.norm { re := 1, im := -1 }) = 1
⊢ False
[PROOFSTEP]
exact absurd this (by decide)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp2 : p = 2
x✝ : Irreducible ↑p
not_unit✝ : ¬IsUnit ↑p
h : ∀ (a b : ℤ[i]), ↑p = a * b → IsUnit a ∨ IsUnit b
this : Int.natAbs (Zsqrtd.norm { re := 1, im := 1 }) = 1 ∨ Int.natAbs (Zsqrtd.norm { re := 1, im := -1 }) = 1
⊢ ¬(Int.natAbs (Zsqrtd.norm { re := 1, im := 1 }) = 1 ∨ Int.natAbs (Zsqrtd.norm { re := 1, im := -1 }) = 1)
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
⊢ False
[PROOFSTEP]
have hp41 : p % 4 = 1 := by
  rw [← Nat.mod_mul_left_mod p 2 2, show 2 * 2 = 4 from rfl] at hp1 
  have := Nat.mod_lt p (show 0 < 4 by decide)
  revert this hp3 hp1
  generalize p % 4 = m
  intros;
  interval_cases m <;>
    simp_all
      -- Porting note: was `decide!`
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
⊢ p % 4 = 1
[PROOFSTEP]
rw [← Nat.mod_mul_left_mod p 2 2, show 2 * 2 = 4 from rfl] at hp1 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 4 % 2 = 1
hp3 : p % 4 ≠ 3
⊢ p % 4 = 1
[PROOFSTEP]
have := Nat.mod_lt p (show 0 < 4 by decide)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 4 % 2 = 1
hp3 : p % 4 ≠ 3
⊢ 0 < 4
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 4 % 2 = 1
hp3 : p % 4 ≠ 3
this : p % 4 < 4
⊢ p % 4 = 1
[PROOFSTEP]
revert this hp3 hp1
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
⊢ p % 4 % 2 = 1 → p % 4 ≠ 3 → p % 4 < 4 → p % 4 = 1
[PROOFSTEP]
generalize p % 4 = m
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
⊢ m % 2 = 1 → m ≠ 3 → m < 4 → m = 1
[PROOFSTEP]
intros
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
hp1✝ : m % 2 = 1
hp3✝ : m ≠ 3
this✝ : m < 4
⊢ m = 1
[PROOFSTEP]
interval_cases m
[GOAL]
case «0»
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
hp1✝ : 0 % 2 = 1
hp3✝ : 0 ≠ 3
this✝ : 0 < 4
⊢ 0 = 1
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «1»
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
hp1✝ : 1 % 2 = 1
hp3✝ : 1 ≠ 3
this✝ : 1 < 4
⊢ 1 = 1
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «2»
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
hp1✝ : 2 % 2 = 1
hp3✝ : 2 ≠ 3
this✝ : 2 < 4
⊢ 2 = 1
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «3»
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
hp1✝ : 3 % 2 = 1
hp3✝ : 3 ≠ 3
this✝ : 3 < 4
⊢ 3 = 1
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
⊢ False
[PROOFSTEP]
let ⟨k, hk⟩ := (ZMod.exists_sq_eq_neg_one_iff (p := p)).2 <| by rw [hp41]; exact by decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
⊢ p % 4 ≠ 3
[PROOFSTEP]
rw [hp41]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
⊢ 1 ≠ 3
[PROOFSTEP]
exact by decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
⊢ 1 ≠ 3
[PROOFSTEP]
decide
[GOAL]
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
⊢ False
[PROOFSTEP]
obtain ⟨k, k_lt_p, rfl⟩ : ∃ (k' : ℕ) (_ : k' < p), (k' : ZMod p) = k := by
  refine' ⟨k.val, k.val_lt, ZMod.nat_cast_zmod_val k⟩
[GOAL]
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' x, ↑k' = k
[PROOFSTEP]
refine' ⟨k.val, k.val_lt, ZMod.nat_cast_zmod_val k⟩
[GOAL]
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
⊢ False
[PROOFSTEP]
have hpk : p ∣ k ^ 2 + 1 := by
  rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one, ← hk, add_left_neg]
[GOAL]
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
[PROOFSTEP]
rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one, ← hk, add_left_neg]
[GOAL]
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
[PROOFSTEP]
have hkmul : (k ^ 2 + 1 : ℤ[i]) = ⟨k, 1⟩ * ⟨k, -1⟩ := by simp [sq, Zsqrtd.ext]
[GOAL]
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
⊢ ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
[PROOFSTEP]
simp [sq, Zsqrtd.ext]
[GOAL]
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
[PROOFSTEP]
have hkltp : 1 + k * k < p * p :=
  calc
    1 + k * k ≤ k + k * k := by
      apply add_le_add_right
      exact (Nat.pos_of_ne_zero fun (hk0 : k = 0) => by clear_aux_decl; simp_all [pow_succ'])
    _ = k * (k + 1) := by simp [add_comm, mul_add]
    _ < p * p := mul_lt_mul k_lt_p k_lt_p (Nat.succ_pos _) (Nat.zero_le _)
[GOAL]
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 * k ≤ k + k * k
[PROOFSTEP]
apply add_le_add_right
[GOAL]
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
[PROOFSTEP]
exact (Nat.pos_of_ne_zero fun (hk0 : k = 0) => by clear_aux_decl; simp_all [pow_succ'])
[GOAL]
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 }
hk0 : k = 0
⊢ False
[PROOFSTEP]
clear_aux_decl
[GOAL]
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 }
hk0 : k = 0
⊢ False
[PROOFSTEP]
simp_all [pow_succ']
[GOAL]
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)
[PROOFSTEP]
simp [add_comm, mul_add]
[GOAL]
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
⊢ False
[PROOFSTEP]
have hpk₁ : ¬(p : ℤ[i]) ∣ ⟨k, -1⟩ := fun ⟨x, hx⟩ =>
  lt_irrefl (p * x : ℤ[i]).norm.natAbs <|
    calc
      (norm (p * x : ℤ[i])).natAbs = (Zsqrtd.norm ⟨k, -1⟩).natAbs := by rw [hx]
      _ < (norm (p : ℤ[i])).natAbs := by simpa [add_comm, Zsqrtd.norm] using hkltp
      _ ≤ (norm (p * x : ℤ[i])).natAbs :=
        norm_le_norm_mul_left _ fun hx0 => show (-1 : ℤ) ≠ 0 by decide <| by simpa [hx0] using congr_arg Zsqrtd.im hx
[GOAL]
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
⊢ Int.natAbs (Zsqrtd.norm (↑p * x)) = Int.natAbs (Zsqrtd.norm { re := ↑k, im := -1 })
[PROOFSTEP]
rw [hx]
[GOAL]
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
⊢ Int.natAbs (Zsqrtd.norm { re := ↑k, im := -1 }) < Int.natAbs (Zsqrtd.norm ↑p)
[PROOFSTEP]
simpa [add_comm, Zsqrtd.norm] using hkltp
[GOAL]
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
[PROOFSTEP]
decide
[GOAL]
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
[PROOFSTEP]
simpa [hx0] using congr_arg Zsqrtd.im hx
[GOAL]
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 }
⊢ False
[PROOFSTEP]
have hpk₂ : ¬(p : ℤ[i]) ∣ ⟨k, 1⟩ := fun ⟨x, hx⟩ =>
  lt_irrefl (p * x : ℤ[i]).norm.natAbs <|
    calc
      (norm (p * x : ℤ[i])).natAbs = (Zsqrtd.norm ⟨k, 1⟩).natAbs := by rw [hx]
      _ < (norm (p : ℤ[i])).natAbs := by simpa [add_comm, Zsqrtd.norm] using hkltp
      _ ≤ (norm (p * x : ℤ[i])).natAbs :=
        norm_le_norm_mul_left _ fun hx0 => show (1 : ℤ) ≠ 0 by decide <| by simpa [hx0] using congr_arg Zsqrtd.im hx
[GOAL]
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
⊢ Int.natAbs (Zsqrtd.norm (↑p * x)) = Int.natAbs (Zsqrtd.norm { re := ↑k, im := 1 })
[PROOFSTEP]
rw [hx]
[GOAL]
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
⊢ Int.natAbs (Zsqrtd.norm { re := ↑k, im := 1 }) < Int.natAbs (Zsqrtd.norm ↑p)
[PROOFSTEP]
simpa [add_comm, Zsqrtd.norm] using hkltp
[GOAL]
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
[PROOFSTEP]
decide
[GOAL]
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
[PROOFSTEP]
simpa [hx0] using congr_arg Zsqrtd.im hx
[GOAL]
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
[PROOFSTEP]
obtain ⟨y, hy⟩ := hpk
[GOAL]
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
[PROOFSTEP]
have := hpi.2.2 ⟨k, 1⟩ ⟨k, -1⟩ ⟨y, by rw [← hkmul, ← Nat.cast_mul p, ← hy]; simp⟩
[GOAL]
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
[PROOFSTEP]
rw [← hkmul, ← Nat.cast_mul p, ← hy]
[GOAL]
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)
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
clear_aux_decl
[GOAL]
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
[PROOFSTEP]
tauto
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑p
[PROOFSTEP]
erw [← ZMod.nat_cast_mod p 4, hp3]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑3
[PROOFSTEP]
exact by decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑3
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
this : ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑p
⊢ ↑a ^ 2 + ↑b ^ 2 = ↑(a ^ 2 + b ^ 2)
[PROOFSTEP]
simp
