case intro.intro
K : Type ?u.853209
R : Type ?u.853212
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]
K : Type ?u.853209
R : Type ?u.853212
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]
rcases ZMod.sq_add_sq p x with ⟨a, b, hx⟩
case intro.intro
K : Type ?u.853209
R : Type ?u.853212
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ↑(Int.natAbs (ZMod.valMinAbs a)) ^ 2 + ↑(Int.natAbs (ZMod.valMinAbs b)) ^ 2 ≡ x [ZMOD ↑p]
case intro.intro
K : Type ?u.853209
R : Type ?u.853212
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ ↑a ^ 2 + ↑b ^ 2 ≡ x [ZMOD ↑p]
refine ⟨a.valMinAbs.natAbs, b.valMinAbs.natAbs, ZMod.natAbs_valMinAbs_le _,
  ZMod.natAbs_valMinAbs_le _, ?_⟩
case intro.intro
K : Type ?u.853209
R : Type ?u.853212
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑(ZMod.valMinAbs a) ^ 2 + ↑(ZMod.valMinAbs b) ^ 2 = ↑x
⊢ ↑(Int.natAbs (ZMod.valMinAbs a)) ^ 2 + ↑(Int.natAbs (ZMod.valMinAbs b)) ^ 2 ≡ x [ZMOD ↑p]
case intro.intro
K : Type ?u.853209
R : Type ?u.853212
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : a ^ 2 + b ^ 2 = ↑x
⊢ ↑(Int.natAbs (ZMod.valMinAbs a)) ^ 2 + ↑(Int.natAbs (ZMod.valMinAbs b)) ^ 2 ≡ x [ZMOD ↑p]
rw [← a.coe_valMinAbs, ← b.coe_valMinAbs] at hx
case intro.intro
K : Type ?u.853209
R : Type ?u.853212
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑(ZMod.valMinAbs a) ^ 2 + ↑(ZMod.valMinAbs b) ^ 2 = ↑x
⊢ abs (ZMod.valMinAbs a) ^ 2 + abs (ZMod.valMinAbs b) ^ 2 ≡ x [ZMOD ↑p]
case intro.intro
K : Type ?u.853209
R : Type ?u.853212
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑(ZMod.valMinAbs a) ^ 2 + ↑(ZMod.valMinAbs b) ^ 2 = ↑x
⊢ ↑(Int.natAbs (ZMod.valMinAbs a)) ^ 2 + ↑(Int.natAbs (ZMod.valMinAbs b)) ^ 2 ≡ x [ZMOD ↑p]
push_cast
case intro.intro
K : Type ?u.853209
R : Type ?u.853212
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑(ZMod.valMinAbs a) ^ 2 + ↑(ZMod.valMinAbs b) ^ 2 = ↑x
⊢ ↑(ZMod.valMinAbs a ^ 2 + ZMod.valMinAbs b ^ 2) = ↑x
case intro.intro
K : Type ?u.853209
R : Type ?u.853212
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑(ZMod.valMinAbs a) ^ 2 + ↑(ZMod.valMinAbs b) ^ 2 = ↑x
⊢ abs (ZMod.valMinAbs a) ^ 2 + abs (ZMod.valMinAbs b) ^ 2 ≡ x [ZMOD ↑p]
rw [sq_abs, sq_abs, ← ZMod.int_cast_eq_int_cast_iff]
no goals
case intro.intro
K : Type ?u.853209
R : Type ?u.853212
p : ℕ
inst✝ : Fact (Prime p)
x : ℤ
a b : ZMod p
hx : ↑(ZMod.valMinAbs a) ^ 2 + ↑(ZMod.valMinAbs b) ^ 2 = ↑x
⊢ ↑(ZMod.valMinAbs a ^ 2 + ZMod.valMinAbs b ^ 2) = ↑x
exact_mod_cast hx