awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn : Squarefree n
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
zero : ∀ (hn : Squarefree (R := ℕ) 0) (H : ∀ q ∈ Nat.primeFactors 0, q % 4 ≠ 3), IsSquare (α := ZMod 0) (-1)
⊢ IsSquare (α := ZMod n) (-1)
have one : ∀ (hn : Squarefree (R := ℕ) 1) (H : ∀ q ∈ Nat.primeFactors 1, q % 4 ≠ 3), IsSquare (α := ZMod 1) (-1)
Tactic: induction n using induction_on_primes with
  | zero => exact False.elim (hn.ne_zero rfl)
  | one => exact ⟨0, by simp only [mul_zero, eq_iff_true_of_subsingleton]⟩
  | prime_mul p n hpp ih =>
    have : Fact p.Prime := ⟨hpp⟩
    have hcp : p.Coprime n := by
      by_contra hc
      exact hpp.not_isUnit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
    have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr <| H _ <|
      Nat.mem_primeFactors.mpr ⟨hpp, Nat.dvd_mul_right .., Squarefree.ne_zero hn⟩
    exact ZMod.isSquare_neg_one_mul hcp hp₁ <| ih hn.of_mul_right fun q hqp => H q <|
        Nat.mem_primeFactors.mpr ⟨Nat.prime_of_mem_primeFactors hqp,
          dvd_mul_of_dvd_right (Nat.dvd_of_mem_primeFactors hqp) _, Squarefree.ne_zero hn⟩
Cleared hypotheses: n, hn, H
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn : Squarefree n
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
zero : ∀ (hn : Squarefree (R := ℕ) 0) (H : ∀ q ∈ Nat.primeFactors 0, q % 4 ≠ 3), IsSquare (α := ZMod 0) (-1)
one : ∀ (hn : Squarefree (R := ℕ) 1) (H : ∀ q ∈ Nat.primeFactors 1, q % 4 ≠ 3), IsSquare (α := ZMod 1) (-1)
⊢ IsSquare (α := ZMod n) (-1)
have prime_mul : ∀ (p n : ℕ) (hpp : Nat.Prime p)
  (ih : ∀ (hn : Squarefree n) (H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3), IsSquare (α := ZMod n) (-1))
  (hn : Squarefree (p * n)) (H : ∀ q ∈ (p * n).primeFactors, q % 4 ≠ 3), IsSquare (α := ZMod (p * n)) (-1)
Tactic: induction n using induction_on_primes with
  | zero => exact False.elim (hn.ne_zero rfl)
  | one => exact ⟨0, by simp only [mul_zero, eq_iff_true_of_subsingleton]⟩
  | prime_mul p n hpp ih =>
    have : Fact p.Prime := ⟨hpp⟩
    have hcp : p.Coprime n := by
      by_contra hc
      exact hpp.not_isUnit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)
    have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr <| H _ <|
      Nat.mem_primeFactors.mpr ⟨hpp, Nat.dvd_mul_right .., Squarefree.ne_zero hn⟩
    exact ZMod.isSquare_neg_one_mul hcp hp₁ <| ih hn.of_mul_right fun q hqp => H q <|
        Nat.mem_primeFactors.mpr ⟨Nat.prime_of_mem_primeFactors hqp,
          dvd_mul_of_dvd_right (Nat.dvd_of_mem_primeFactors hqp) _, Squarefree.ne_zero hn⟩
Cleared hypotheses: n, hn, H
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n : ℕ
hn : Squarefree n
⊢ IsSquare (α := ZMod n) (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
have help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
Tactic: have help : ∀ a b : ZMod 4, a ≠ 3 → b ≠ 3 → a * b ≠ 3 := by decide
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ IsSquare (α := ZMod n) (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
have rw : (∀ q ∈ n.primeFactors, q % 4 ≠ 3) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
Tactic: rw [ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three hn]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ (∀ q ∈ n.primeFactors, q % 4 ≠ 3) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
have refine : (∀ q ∈ n.primeFactors, q % 4 ≠ 3) → ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
Tactic: refine ⟨?_, fun H q hq => H <| Nat.dvd_of_mem_primeFactors hq⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
⊢ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
have refine_1 : 0 ∣ n → HMod.hMod (α := ℕ) 0 4 ≠ 3
Tactic: refine @induction_on_primes _ ?_ ?_ (fun p q hp hq hpq => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
refine_1 : 0 ∣ n → HMod.hMod (α := ℕ) 0 4 ≠ 3
⊢ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
have refine_2 : 1 ∣ n → HMod.hMod (α := ℕ) 1 4 ≠ 3
Tactic: refine @induction_on_primes _ ?_ ?_ (fun p q hp hq hpq => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
refine_1 : 0 ∣ n → HMod.hMod (α := ℕ) 0 4 ≠ 3
refine_2 : 1 ∣ n → HMod.hMod (α := ℕ) 1 4 ≠ 3
⊢ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
have refine_3 : ∀ (p q : ℕ) (hp : Nat.Prime p) (hq : q ∣ n → q % 4 ≠ 3) (hpq : p * q ∣ n), p * q % 4 ≠ 3
Tactic: refine @induction_on_primes _ ?_ ?_ (fun p q hp hq hpq => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hp : Nat.Prime p
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
⊢ p * q % 4 ≠ 3
have hp₁ : p % 4 ≠ 3
Tactic: replace hp := H _ <|
      Nat.mem_primeFactors.mpr ⟨hp, dvd_of_mul_right_dvd hpq, Squarefree.ne_zero hn⟩
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
hp : p % 4 ≠ 3
⊢ p * q % 4 ≠ 3
have hq₁ : q % 4 ≠ 3
Tactic: replace hq := hq (dvd_of_mul_left_dvd hpq)
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : p % 4 ≠ 3
hq : q % 4 ≠ 3
⊢ p * q % 4 ≠ 3
have refine_3 : ∀ (hp : ¬Eq (α := ZMod 4) (↑p : ZMod 4) (↑3 : ZMod 4)) (hq : ¬Eq (α := ZMod 4) (↑q : ZMod 4) (↑3 : ZMod 4)),
  ¬Eq (α := ZMod 4) (↑(p * q) : ZMod 4) (↑3 : ZMod 4)
Tactic: rw [show 3 = 3 % 4 by simp, Ne, ← ZMod.natCast_eq_natCast_iff'] at hp hq ⊢
Cleared hypotheses: hp, hq
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬Eq (α := ZMod 4) (↑p : ZMod 4) (↑3 : ZMod 4)
hq : ¬Eq (α := ZMod 4) (↑q : ZMod 4) (↑3 : ZMod 4)
⊢ ¬Eq (α := ZMod 4) (↑(p * q) : ZMod 4) (↑3 : ZMod 4)
have refine_3 : ¬HMul.hMul (α := ZMod 4) (↑p : ZMod 4) (↑q : ZMod 4) = (↑3 : ZMod 4)
Tactic: rw [Nat.cast_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
p n : ℕ
hpp : Prime p
ih : ∀ (h : IsSquare (α := ZMod n) (-1)), ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
h : IsSquare (α := ZMod (p * n)) (-1)
⊢ ∃ (x : ℕ) (y : ℕ), p * n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have this : Fact (Prime p)
Tactic: have : Fact p.Prime := ⟨hpp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
p n : ℕ
hpp : Prime p
ih : ∀ (h : IsSquare (α := ZMod n) (-1)), ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
h : IsSquare (α := ZMod (p * n)) (-1)
this : Fact (Prime p)
⊢ ∃ (x : ℕ) (y : ℕ), p * n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have hp : IsSquare (α := ZMod p) (-1)
Tactic: have hp : IsSquare (-1 : ZMod p) := ZMod.isSquare_neg_one_of_dvd ⟨n, rfl⟩ h
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
p n : ℕ
hpp : Prime p
ih : ∀ (h : IsSquare (α := ZMod n) (-1)), ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
h : IsSquare (α := ZMod (p * n)) (-1)
this : Fact (Prime p)
hp : IsSquare (α := ZMod p) (-1)
⊢ ∃ (x : ℕ) (y : ℕ), p * n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have prime_mul : ∀ (u v : ℕ) (huv : HPow.hPow (β := ℕ) u 2 + HPow.hPow (β := ℕ) v 2 = p),
  ∃ (x : ℕ) (y : ℕ), p * n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: obtain ⟨u, v, huv⟩ := Nat.Prime.sq_add_sq (ZMod.exists_sq_eq_neg_one_iff.mp hp)
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
p n : ℕ
hpp : Prime p
ih : ∀ (h : IsSquare (α := ZMod n) (-1)), ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
h : IsSquare (α := ZMod (p * n)) (-1)
this : Fact (Prime p)
hp : IsSquare (α := ZMod p) (-1)
u v : ℕ
huv : HPow.hPow (β := ℕ) u 2 + HPow.hPow (β := ℕ) v 2 = p
⊢ ∃ (x : ℕ) (y : ℕ), p * n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have prime_mul : ∀ (x y : ℕ) (hxy : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2),
  ∃ (x : ℕ) (y : ℕ), p * n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: obtain ⟨x, y, hxy⟩ := ih (ZMod.isSquare_neg_one_of_dvd ⟨p, mul_comm _ _⟩ h)
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
h : IsSquare (α := ZMod n) (-1)
⊢ ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have zero : ∀ (h : IsSquare (α := ZMod 0) (-1)), ∃ (x : ℕ) (y : ℕ), 0 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: induction n using induction_on_primes with
  | zero => exact ⟨0, 0, rfl⟩
  | one => exact ⟨0, 1, rfl⟩
  | prime_mul p n hpp ih =>
    have : Fact p.Prime := ⟨hpp⟩
    have hp : IsSquare (-1 : ZMod p) := ZMod.isSquare_neg_one_of_dvd ⟨n, rfl⟩ h
    obtain ⟨u, v, huv⟩ := Nat.Prime.sq_add_sq (ZMod.exists_sq_eq_neg_one_iff.mp hp)
    obtain ⟨x, y, hxy⟩ := ih (ZMod.isSquare_neg_one_of_dvd ⟨p, mul_comm _ _⟩ h)
    exact Nat.sq_add_sq_mul huv.symm hxy
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
h : IsSquare (α := ZMod n) (-1)
zero : ∀ (h : IsSquare (α := ZMod 0) (-1)), ∃ (x : ℕ) (y : ℕ), 0 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have one : ∀ (h : IsSquare (α := ZMod 1) (-1)), ∃ (x : ℕ) (y : ℕ), 1 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: induction n using induction_on_primes with
  | zero => exact ⟨0, 0, rfl⟩
  | one => exact ⟨0, 1, rfl⟩
  | prime_mul p n hpp ih =>
    have : Fact p.Prime := ⟨hpp⟩
    have hp : IsSquare (-1 : ZMod p) := ZMod.isSquare_neg_one_of_dvd ⟨n, rfl⟩ h
    obtain ⟨u, v, huv⟩ := Nat.Prime.sq_add_sq (ZMod.exists_sq_eq_neg_one_iff.mp hp)
    obtain ⟨x, y, hxy⟩ := ih (ZMod.isSquare_neg_one_of_dvd ⟨p, mul_comm _ _⟩ h)
    exact Nat.sq_add_sq_mul huv.symm hxy
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
h : IsSquare (α := ZMod n) (-1)
zero : ∀ (h : IsSquare (α := ZMod 0) (-1)), ∃ (x : ℕ) (y : ℕ), 0 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
one : ∀ (h : IsSquare (α := ZMod 1) (-1)), ∃ (x : ℕ) (y : ℕ), 1 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
have prime_mul : ∀ (p n : ℕ) (hpp : Prime p)
  (ih : ∀ (h : IsSquare (α := ZMod n) (-1)), ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
  (h : IsSquare (α := ZMod (p * n)) (-1)), ∃ (x : ℕ) (y : ℕ), p * n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: induction n using induction_on_primes with
  | zero => exact ⟨0, 0, rfl⟩
  | one => exact ⟨0, 1, rfl⟩
  | prime_mul p n hpp ih =>
    have : Fact p.Prime := ⟨hpp⟩
    have hp : IsSquare (-1 : ZMod p) := ZMod.isSquare_neg_one_of_dvd ⟨n, rfl⟩ h
    obtain ⟨u, v, huv⟩ := Nat.Prime.sq_add_sq (ZMod.exists_sq_eq_neg_one_iff.mp hp)
    obtain ⟨x, y, hxy⟩ := ih (ZMod.isSquare_neg_one_of_dvd ⟨p, mul_comm _ _⟩ h)
    exact Nat.sq_add_sq_mul huv.symm hxy
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
⊢ IsCoprime x n
have hc2 : IsCoprime (HPow.hPow (β := ℕ) x 2) (HPow.hPow (β := ℕ) y 2)
Tactic: have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
hc2 : IsCoprime (HPow.hPow (β := ℕ) x 2) (HPow.hPow (β := ℕ) y 2)
⊢ IsCoprime x n
have hc2₁ : IsCoprime (HPow.hPow (β := ℕ) x 2) (n + -1 * HPow.hPow (β := ℕ) x 2)
Tactic: rw [show y ^ 2 = n + -1 * x ^ 2 by lia] at hc2
Cleared hypotheses: hc2
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
⊢ IsSquare (α := ZMod n.natAbs) (-1)
have obtain : ∀ (u v : ℤ) (huv : u * x + v * n = 1), IsSquare (α := ZMod n.natAbs) (-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 lia] at hc2
    exact (IsCoprime.pow_left_iff zero_lt_two).mp hc2.of_add_mul_right_right
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
⊢ IsSquare (α := ZMod n.natAbs) (-1)
have H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
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
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
⊢ IsSquare (α := ZMod n.natAbs) (-1)
have refine : -1 =
  HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs) *
    HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs)
Tactic: refine ⟨u * y, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
⊢ HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs) *
      HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs) =
    (↑(u * y * (u * y)) : ZMod n.natAbs)
have norm_cast : Eq (α := ZMod n.natAbs) (↑(u * y * (u * y)) : ZMod n.natAbs) (↑(u * y * (u * y)) : ZMod n.natAbs)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
⊢ -1 =
    HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs) *
      HMul.hMul (α := ZMod n.natAbs) (↑u : ZMod n.natAbs) (↑y : ZMod n.natAbs)
have conv_rhs : Eq (α := ZMod n.natAbs) (-1) (↑(u * y * (u * y)) : ZMod n.natAbs)
Tactic: conv_rhs => tactic => norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
⊢ Eq (α := ZMod n.natAbs) (-1) (↑(-1) : ZMod n.natAbs)
have norm_cast : Eq (α := ZMod n.natAbs) (↑(Int.negSucc 0) : ZMod n.natAbs) (↑(Int.negSucc 0) : ZMod n.natAbs)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-HPow.hPow (β := ℕ) v 2 * n + HPow.hPow (β := ℕ) u 2 + 2 * v)
⊢ Eq (α := ZMod n.natAbs) (-1) (↑(u * y * (u * y)) : ZMod n.natAbs)
have rw : Eq (α := ZMod n.natAbs) (↑(-1) : ZMod n.natAbs) (↑(u * y * (u * y)) : ZMod n.natAbs)
Tactic: rw [(by norm_cast : (-1 : ZMod n.natAbs) = (-1 : ℤ))]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : x.Coprime y
⊢ IsSquare (α := ZMod n) (-1)
have h₁ : (↑n : ℤ) = HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2
Tactic: zify at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
⊢ (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
have mp : (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) →
  ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n : ℕ
mp :
  (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) →
    ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
⊢ (∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) ↔
    ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
have mpr : (∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)) →
  ∃ (x : ℕ) (y : ℕ), n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
have pos : ∀ (hxy : x = 0 ∧ y = 0), ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
Tactic: by_cases hxy : x = 0 ∧ y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
pos : ∀ (hxy : x = 0 ∧ y = 0), ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
have neg : ∀ (hxy : ¬(x = 0 ∧ y = 0)), ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
Tactic: by_cases hxy : x = 0 ∧ y = 0
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
⊢ n = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
have rw : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
Tactic: rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
rw : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
⊢ n = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
have rw₁ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
Tactic: rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
rw : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₁ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
⊢ n = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
have rw₂ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
Tactic: rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
rw : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₁ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₂ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
⊢ n = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
have rw₃ : HAdd.hAdd (α := ℕ) 0 0 = HMul.hMul (α := ℕ) 0 1
Tactic: rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
rw : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₁ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₂ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₃ : HAdd.hAdd (α := ℕ) 0 0 = HMul.hMul (α := ℕ) 0 1
⊢ n = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
have rw₄ : 0 = HMul.hMul (α := ℕ) 0 1
Tactic: rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
rw : HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₁ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 + HPow.hPow (β := ℕ) y 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₂ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
rw₃ : HAdd.hAdd (α := ℕ) 0 0 = HMul.hMul (α := ℕ) 0 1
rw₄ : 0 = HMul.hMul (α := ℕ) 0 1
⊢ n = HPow.hPow (α := ℕ) (β := ℕ) 0 2 * 1
have rw₅ : Eq (α := ℕ) 0 0
Tactic: rw [h, hxy.1, hxy.2, zero_pow two_ne_zero, add_zero, zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
⊢ -1 = HMul.hMul (α := ZMod 1) 0 0
have rw : Eq (α := ZMod 1) (-1) 0
Tactic: rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
rw : Eq (α := ZMod 1) (-1) 0
⊢ -1 = HMul.hMul (α := ZMod 1) 0 0
have rw₁ : Eq (α := ZMod 1) 1 0
Tactic: rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : x = 0 ∧ y = 0
rw : Eq (α := ZMod 1) (-1) 0
rw₁ : Eq (α := ZMod 1) 1 0
⊢ -1 = HMul.hMul (α := ZMod 1) 0 0
have rw₂ : 0 + 1 = 1
Tactic: rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (hypothesis)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : ¬(x = 0 ∧ y = 0)
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
have hg : 0 < x.gcd y
Tactic: have hg := Nat.pos_of_ne_zero (mt Nat.gcd_eq_zero_iff.mp hxy)
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hxy : ¬(x = 0 ∧ y = 0)
hg : 0 < x.gcd y
⊢ ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
have neg : ∀ (g x₁ y₁ : ℕ),
  0 < g →
    ∀ (h₂ : x₁.Coprime y₁) (h₃ : x = x₁ * g) (h₄ : y = y₁ * g),
      ∃ (a : ℕ) (b : ℕ), n = HPow.hPow (β := ℕ) a 2 * b ∧ IsSquare (α := ZMod b) (-1)
Tactic: obtain ⟨g, x₁, y₁, _, h₂, h₃, h₄⟩ := Nat.exists_coprime' hg
-- Lean 4 proof step from Mathlib.NumberTheory.SumTwoSquares (goal)
Goal:
n x y : ℕ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) 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 = HPow.hPow (β := ℕ) g 2 * (HPow.hPow (β := ℕ) x₁ 2 + HPow.hPow (β := ℕ) y₁ 2)
have rw : HPow.hPow (β := ℕ) (x₁ * g) 2 + HPow.hPow (β := ℕ) (y₁ * g) 2 =
  HPow.hPow (β := ℕ) g 2 * (HPow.hPow (β := ℕ) x₁ 2 + HPow.hPow (β := ℕ) y₁ 2)
Tactic: rw [h, h₃, h₄]