-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem Nat.eq_sq_add_sq_iff {n : ℕ} :
    (∃ x y : ℕ, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, q.Prime → q % 4 = 3 → Even (padicValNat q n)

Proof state:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
⊢ Odd (padicValNat q n)

Tactic:
haveI hqi : Fact q.Prime := ⟨hqp⟩

Result:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
hqi : Fact (Prime q)
⊢ Odd (padicValNat q n)

Proof state:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
hqi : Fact (Prime q)
⊢ Even (padicValNat q n)

Tactic:
simp_rw [h₁, padicValNat.mul ha₂ hb, padicValNat.pow 2 ha, hqb, add_zero]

Result:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
hqi : Fact (Prime q)
⊢ Even (2 * padicValNat q a)

Proof state:
case inr
n : ℕ
hn₀ : n > 0
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)

Tactic:
rw [Nat.eq_sq_add_sq_iff_eq_sq_mul]

Result:
case inr
n : ℕ
hn₀ : n > 0
⊢ (∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)

Proof state:
case inr.refine_2
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Tactic:
obtain ⟨b, a, hb₀, ha₀, hab, hb⟩ := Nat.sq_mul_squarefree_of_pos hn₀

Result:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Proof state:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
⊢ False

Tactic:
refine Nat.not_even_iff_odd.2 ?_ (H hqp hq4)

Result:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
⊢ Odd (padicValNat q n)

Proof state:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
⊢ Even (padicValNat q n)

Tactic:
have hab : a ^ 2 * b ≠ 0 := h₁ ▸ hn₀.ne'

Result:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
⊢ Even (padicValNat q n)

Proof state:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
⊢ Odd (padicValNat q n)

Tactic:
have hqb' : padicValNat q b = 1 :=
  b.factorization_def hqp ▸ le_antisymm (hb.natFactorization_le_one _)
    ((hqp.dvd_iff_one_le_factorization hb₀.ne').mp hqb)

Result:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
hqb' : padicValNat q b = 1
⊢ Odd (padicValNat q n)

Proof state:
case inl

⊢ (∃ x y, 0 = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q 0)

Tactic:
exact ⟨fun _ q _ _ => (@padicValNat.zero q).symm ▸ Even.zero, fun _ => ⟨0, 0, rfl⟩⟩

Result:
no goals

Proof state:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
⊢ Even (padicValNat q n)

Tactic:
haveI hqi : Fact q.Prime := ⟨hq⟩

Result:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
hqi : Fact (Prime q)
⊢ Even (padicValNat q n)

Proof state:
case inr.refine_1
n : ℕ
hn₀ : n > 0
H : ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
q : ℕ
hq : Prime q
h : q % 4 = 3
⊢ Even (padicValNat q n)

Tactic:
obtain ⟨a, b, h₁, h₂⟩ := H

Result:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
⊢ Even (padicValNat q n)

Proof state:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Tactic:
refine ⟨a, b, hab.symm, (ZMod.isSquare_neg_one_iff hb).mpr fun {q} hqp hqb hq4 => ?_⟩

Result:
case inr.refine_2.intro.intro.intro.intro.intro
n : ℕ
hn₀ : n > 0
H : ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)
b a : ℕ
hb₀ : 0 < b
ha₀ : 0 < a
hab : a ^ 2 * b = n
hb : Squarefree b
q : ℕ
hqp : Prime q
hqb : q ∣ b
hq4 : q % 4 = 3
⊢ False

Proof state:
n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn₀)

Result:
case inl

⊢ (∃ x y, 0 = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q 0)

case inr
n : ℕ
hn₀ : n > 0
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, Prime q → q % 4 = 3 → Even (padicValNat q n)

Proof state:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
⊢ Even (padicValNat q n)

Tactic:
have hb := right_ne_zero_of_mul hab

Result:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
hb : b ≠ 0
⊢ Even (padicValNat q n)

Proof state:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
⊢ Even (padicValNat q n)

Tactic:
have ha := mt sq_eq_zero_iff.mpr ha₂

Result:
case inr.refine_1.intro.intro.intro
n : ℕ
hn₀ : n > 0
q : ℕ
hq : Prime q
h : q % 4 = 3
a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
hqb : padicValNat q b = 0
hab : a ^ 2 * b ≠ 0
ha₂ : a ^ 2 ≠ 0
ha : ¬a = 0
⊢ Even (padicValNat q n)