case inl
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp2 : p = 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

case inr
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
cases' hp.1.eq_two_or_odd with hp2 hp_odd
case inr
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
case inr
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
let f : (ZMod p)[X] := X ^ 2
case inr
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
case inr
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
let g : (ZMod p)[X] := X ^ 2 - C x
case inr.intro.intro
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
case inr
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
obtain ⟨a, b, hab⟩ : ∃ a b, f.eval a + g.eval b = 0 :=
  @exists_root_sum_quadratic _ _ _ _ f g (degree_X_pow 2) (degree_X_pow_sub_C (by decide) _)
    (by rw [ZMod.card, hp_odd])
case inr.intro.intro
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ a ^ 2 + b ^ 2 = x
case inr.intro.intro
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
refine' ⟨a, b, _⟩
case inr.intro.intro
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ a ^ 2 + b ^ 2 - x = 0
case inr.intro.intro
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ a ^ 2 + b ^ 2 = x
rw [← sub_eq_zero]
no goals
case inr.intro.intro
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
a b : ZMod p
hab : eval a f + eval b g = 0
⊢ a ^ 2 + b ^ 2 - x = 0
simpa only [eval_C, eval_X, eval_pow, eval_sub, ← add_sub_assoc] using hab
case inl
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
x : ZMod 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
case inl
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp2 : p = 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
subst p
case inl
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
x : Fin 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
case inl
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
x : ZMod 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
change Fin 2 at x
case inl.head
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = { val := 0, isLt := (_ : 0 < 2) }

case inl.tail.head
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = { val := 1, isLt := (_ : (fun a => a < 2) 1) }
case inl
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
x : Fin 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x
fin_cases x
case inl.head
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
⊢ ∃ b, 0 ^ 2 + b ^ 2 = { val := 0, isLt := (_ : 0 < 2) }
case inl.head
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = { val := 0, isLt := (_ : 0 < 2) }
use 0
no goals
case inl.head
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
⊢ ∃ b, 0 ^ 2 + b ^ 2 = { val := 0, isLt := (_ : 0 < 2) }
simp
case inl.tail.head
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
⊢ 0 ^ 2 + 1 ^ 2 = { val := 1, isLt := (_ : (fun a => a < 2) 1) }
case inl.tail.head
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = { val := 1, isLt := (_ : (fun a => a < 2) 1) }
use 0, 1
no goals
case inl.tail.head
K : Type ?u.822912
R : Type ?u.822915
hp : Fact (Nat.Prime 2)
⊢ 0 ^ 2 + 1 ^ 2 = { val := 1, isLt := (_ : (fun a => a < 2) 1) }
simp
no goals
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
⊢ 0 < 2
decide
no goals
K : Type ?u.822912
R : Type ?u.822915
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
f : (ZMod p)[X] := X ^ 2
g : (ZMod p)[X] := X ^ 2 - ↑C x
⊢ Fintype.card (ZMod p) % 2 = 1
rw [ZMod.card, hp_odd]