-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime {n x y : ℤ} (h : n = x ^ 2 + y ^ 2)
    (hc : IsCoprime x y) : IsSquare (-1 : ZMod n.natAbs)

Proof state:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
⊢ IsCoprime x n

Tactic:
have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow

Result:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (y ^ 2)
⊢ IsCoprime x n

Proof state:
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑(u * y * (u * y))

Tactic:
rw [(by norm_cast : (-1 : ZMod n.natAbs) = (-1 : ℤ))]

Result:
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ ↑(-1) = ↑(u * y * (u * y))

Proof state:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (n + -1 * x ^ 2)
⊢ IsCoprime x n

Tactic:
exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right

Result:
no goals

Proof state:
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ ↑(-1) = ↑(u * y * (u * y))

Tactic:
exact (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ _).mpr (Int.natAbs_dvd.mpr ⟨_, H⟩)

Result:
no goals

Proof state:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
⊢ IsSquare (-1)

Tactic:
obtain ⟨u, v, huv⟩ : IsCoprime x n := by
  have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow
  rw [show y ^ 2 = n + -1 * x ^ 2 by omega] at hc2
  exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right

Result:
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
⊢ IsSquare (-1)

Proof state:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑(-1)

Tactic:
norm_cast

Result:
no goals

Proof state:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (y ^ 2)
⊢ y ^ 2 = n + -1 * x ^ 2

Tactic:
omega

Result:
no goals

Proof state:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ ↑u * ↑y * (↑u * ↑y) = ?m.37853

Tactic:
norm_cast

Result:
no goals

Proof state:
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑u * ↑y * (↑u * ↑y)

Tactic:
conv_rhs => tactic => norm_cast

Result:
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑(u * y * (u * y))

Proof state:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (y ^ 2)
⊢ IsCoprime x n

Tactic:
rw [show y ^ 2 = n + -1 * x ^ 2 by omega] at hc2

Result:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
hc2 : IsCoprime (x ^ 2) (n + -1 * x ^ 2)
⊢ IsCoprime x n

Proof state:
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
⊢ IsSquare (-1)

Tactic:
have H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v) := by
  linear_combination -u ^ 2 * h + (n * v - u * x - 1) * huv

Result:
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ IsSquare (-1)

Proof state:
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ IsSquare (-1)

Tactic:
refine ⟨u * y, ?_⟩

Result:
case intro.intro
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ -1 = ↑u * ↑y * (↑u * ↑y)

Proof state:
n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
⊢ u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)

Tactic:
linear_combination -u ^ 2 * h + (n * v - u * x - 1) * huv

Result:
no goals