K : Type ?u.857034
R✝ : Type ?u.857037
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
K : Type ?u.857034
R✝ : Type ?u.857037
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
haveI := char_is_prime_of_pos R p
case intro.intro
K : Type ?u.857034
R✝ : Type ?u.857037
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : a ^ 2 + b ^ 2 = ↑x
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
K : Type ?u.857034
R✝ : Type ?u.857037
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
obtain ⟨a, b, hab⟩ := ZMod.sq_add_sq p x
case intro.intro
K : Type ?u.857034
R✝ : Type ?u.857037
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : a ^ 2 + b ^ 2 = ↑x
⊢ ↑(ZMod.val a) ^ 2 + ↑(ZMod.val b) ^ 2 = ↑x
case intro.intro
K : Type ?u.857034
R✝ : Type ?u.857037
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : a ^ 2 + b ^ 2 = ↑x
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
refine' ⟨a.val, b.val, _⟩
no goals
case intro.intro
K : Type ?u.857034
R✝ : Type ?u.857037
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : a ^ 2 + b ^ 2 = ↑x
⊢ ↑(ZMod.val a) ^ 2 + ↑(ZMod.val b) ^ 2 = ↑x
simpa using congr_arg (ZMod.castHom dvd_rfl R) hab