-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem Nat.eq_sq_add_sq_iff_eq_sq_mul {n : ℕ} :
    (∃ x y : ℕ, n = x ^ 2 + y ^ 2) ↔ ∃ a b : ℕ, n = a ^ 2 * b ∧ IsSquare (-1 : ZMod b)

Proof state:
case pos
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Tactic:
exact ⟨0, 1, by rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul],
  ⟨0, by rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]⟩⟩

Result:
no goals

Proof state:
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ (x₁ * g) ^ 2 + (y₁ * g) ^ 2 = g ^ 2 * (x₁ ^ 2 + y₁ ^ 2)

Tactic:
ring

Result:
no goals

Proof state:
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ n = (a * x') ^ 2 + (a * y') ^ 2

Tactic:
rw [h₁, h]

Result:
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ a ^ 2 * (x' ^ 2 + y' ^ 2) = (a * x') ^ 2 + (a * y') ^ 2

Proof state:
case mpr
n : ℕ
⊢ (∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) → ∃ x y, n = x ^ 2 + y ^ 2

Tactic:
rintro ⟨a, b, h₁, h₂⟩

Result:
case mpr.intro.intro.intro
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
⊢ ∃ x y, n = x ^ 2 + y ^ 2

Proof state:
case neg
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Tactic:
have hg := Nat.pos_of_ne_zero (mt Nat.gcd_eq_zero_iff.mp hxy)

Result:
case neg
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Proof state:
case mp
n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) → ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Tactic:
rintro ⟨x, y, h⟩

Result:
case mp.intro.intro
n x y : ℕ
h : n = x ^ 2 + y ^ 2
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Proof state:
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ a ^ 2 * (x' ^ 2 + y' ^ 2) = (a * x') ^ 2 + (a * y') ^ 2

Tactic:
ring

Result:
no goals

Proof state:
case neg
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Tactic:
obtain ⟨g, x₁, y₁, _, h₂, h₃, h₄⟩ := Nat.exists_coprime' hg

Result:
case neg.intro.intro.intro.intro.intro.intro
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Proof state:
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ n = g ^ 2 * (x₁ ^ 2 + y₁ ^ 2)

Tactic:
rw [h, h₃, h₄]

Result:
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ (x₁ * g) ^ 2 + (y₁ * g) ^ 2 = g ^ 2 * (x₁ ^ 2 + y₁ ^ 2)

Proof state:
case mp.intro.intro
n x y : ℕ
h : n = x ^ 2 + y ^ 2
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Tactic:
by_cases hxy : x = 0 ∧ y = 0

Result:
case pos
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

case neg
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Proof state:
n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Tactic:
constructor

Result:
case mp
n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) → ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

case mpr
n : ℕ
⊢ (∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)) → ∃ x y, n = x ^ 2 + y ^ 2

Proof state:
case mpr.intro.intro.intro.intro.intro
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ ∃ x y, n = x ^ 2 + y ^ 2

Tactic:
exact ⟨a * x', a * y', by rw [h₁, h]; ring⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
⊢ ∃ x y, n = x ^ 2 + y ^ 2

Tactic:
obtain ⟨x', y', h⟩ := Nat.eq_sq_add_sq_of_isSquare_mod_neg_one h₂

Result:
case mpr.intro.intro.intro.intro.intro
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ ∃ x y, n = x ^ 2 + y ^ 2

Proof state:
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ n = 0 ^ 2 * 1

Tactic:
rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul]

Result:
no goals

Proof state:
case neg.intro.intro.intro.intro.intro.intro
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
g x₁ y₁ : ℕ
left✝ : 0 < g
h₂ : x₁.Coprime y₁
h₃ : x = x₁ * g
h₄ : y = y₁ * g
⊢ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)

Tactic:
exact ⟨g, x₁ ^ 2 + y₁ ^ 2, by rw [h, h₃, h₄]; ring,
  ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime rfl h₂⟩

Result:
no goals

Proof state:
n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ -1 = 0 * 0

Tactic:
rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]

Result:
no goals