-- Mathlib/FieldTheory/Finite/Basic.lean
theorem sq_add_sq (p : ℕ) [hp : Fact p.Prime] (x : ZMod p) : ∃ a b : ZMod p, a ^ 2 + b ^ 2 = x

Proof state:
case inr
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

Tactic:
let g : (ZMod p)[X] := X ^ 2 - C x

Result:
case inr
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

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp2 : p = 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Tactic:
subst p

Result:
case inl
hp : Fact (Nat.Prime 2)
x : ZMod 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Proof state:
case inl.«0»
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = (fun i => i) ⟨0, ⋯⟩

Tactic:
use 0

Result:
case h
hp : Fact (Nat.Prime 2)
⊢ ∃ b, 0 ^ 2 + b ^ 2 = (fun i => i) ⟨0, ⋯⟩

Proof state:
case h
hp : Fact (Nat.Prime 2)
⊢ ∃ b, 0 ^ 2 + b ^ 2 = (fun i => i) ⟨0, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
case inr
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

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

Result:
case inr.intro.intro
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

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Tactic:
let f : (ZMod p)[X] := X ^ 2

Result:
case inr
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

Proof state:
case inl
hp : Fact (Nat.Prime 2)
x : Fin 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Tactic:
fin_cases x

Result:
case inl.«0»
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = (fun i => i) ⟨0, ⋯⟩

case inl.«1»
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = (fun i => i) ⟨1, ⋯⟩

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Tactic:
rcases hp.1.eq_two_or_odd with hp2 | hp_odd

Result:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp2 : p = 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

case inr
p : ℕ
hp : Fact (Nat.Prime p)
x : ZMod p
hp_odd : p % 2 = 1
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Proof state:
case inl.«1»
hp : Fact (Nat.Prime 2)
⊢ ∃ a b, a ^ 2 + b ^ 2 = (fun i => i) ⟨1, ⋯⟩

Tactic:
use 0, 1

Result:
case h
hp : Fact (Nat.Prime 2)
⊢ 0 ^ 2 + 1 ^ 2 = (fun i => i) ⟨1, ⋯⟩

Proof state:
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

Tactic:
decide

Result:
no goals

Proof state:
case h
hp : Fact (Nat.Prime 2)
⊢ 0 ^ 2 + 1 ^ 2 = (fun i => i) ⟨1, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
case inl
hp : Fact (Nat.Prime 2)
x : ZMod 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Tactic:
change Fin 2 at x

Result:
case inl
hp : Fact (Nat.Prime 2)
x : Fin 2
⊢ ∃ a b, a ^ 2 + b ^ 2 = x

Proof state:
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

Tactic:
rw [ZMod.card, hp_odd]

Result:
no goals

Proof state:
case inr.intro.intro
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

Tactic:
refine ⟨a, b, ?_⟩

Result:
case inr.intro.intro
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

Proof state:
case inr.intro.intro
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

Tactic:
rw [← sub_eq_zero]

Result:
case inr.intro.intro
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

Proof state:
case inr.intro.intro
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

Tactic:
simpa only [f, g, eval_C, eval_X, eval_pow, eval_sub, ← add_sub_assoc] using hab

Result:
no goals