awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
m n : ℕ
hd : m ∣ n
hs : IsSquare (α := ZMod n) (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (α := ZMod m) ((f : (a : ZMod n) → ZMod m) (-1))

Tactic:
exact hs.map f

Premises used: IsSquare.map
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (α := ZMod m) (-1)
hn : IsSquare (α := ZMod n) (-1)
rw : IsSquare (α := ZMod m × ZMod n) (-1, -1)
⊢ IsSquare (α := ZMod m × ZMod n) (-1)

Tactic:
rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]

Premises used: rfl
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (α := ZMod m) (-1)
hn : IsSquare (α := ZMod n) (-1)
obtain : ∀ (x : ZMod m) (hx : -1 = x * x), IsSquare (α := ZMod m × ZMod n) (-1, -1)
⊢ IsSquare (α := ZMod m × ZMod n) (-1, -1)

Tactic:
obtain ⟨x, hx⟩ := hm
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
m n : ℕ
hc : m.Coprime n
hn : IsSquare (α := ZMod n) (-1)
x : ZMod m
hx : -1 = x * x
obtain : ∀ (y : ZMod n) (hy : -1 = y * y), IsSquare (α := ZMod m × ZMod n) (-1, -1)
⊢ IsSquare (α := ZMod m × ZMod n) (-1, -1)

Tactic:
obtain ⟨y, hy⟩ := hn
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
m n : ℕ
hc : m.Coprime n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
rw : IsSquare (x * x, y * y)
⊢ IsSquare (α := ZMod m × ZMod n) (-1, -1)

Tactic:
rw [hx, hy]
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
m n : ℕ
hc : m.Coprime n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (x * x, y * y)

Tactic:
⟨(x, y), rfl⟩

Premises used: Prod.mk, IsSquare, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
m n : ℕ
hc : m.Coprime n
x : ZMod m
hx : -1 = x * x
y : ZMod n
hy : -1 = y * y
⊢ IsSquare (x * x, y * y)

Tactic:
exact ⟨(x, y), rfl⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (α := ZMod m) (-1)
hn : IsSquare (α := ZMod n) (-1)
⊢ IsSquare (α := ZMod m × ZMod n) (-1)

Tactic:
have : IsSquare (-1 : ZMod m × ZMod n) := by
    rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]
    obtain ⟨x, hx⟩ := hm
    obtain ⟨y, hy⟩ := hn
    rw [hx, hy]
    exact ⟨(x, y), rfl⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
m n : ℕ
hc : m.Coprime n
hm : IsSquare (α := ZMod m) (-1)
hn : IsSquare (α := ZMod n) (-1)
this : IsSquare (α := ZMod m × ZMod n) (-1)
⊢ IsSquare (α := ZMod (m * n)) (-1)

Tactic:
simpa only [RingEquiv.map_neg_one] using this.map (ZMod.chineseRemainder hc).symm

Premises used: RingEquiv.map_neg_one, IsSquare.map, ZMod.chineseRemainder, RingEquiv.symm
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (α := ZMod n) (-1)
obtain : ∀ (y : ZMod p) (h : -1 = y * y), p % 4 ≠ 3
⊢ p % 4 ≠ 3

Tactic:
obtain ⟨y, h⟩ := ZMod.isSquare_neg_one_of_dvd (Nat.dvd_of_mem_primeFactors hp) hs

Premises used: Nat.dvd_of_mem_primeFactors, ZMod.isSquare_neg_one_of_dvd
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (α := ZMod n) (-1)
y : ZMod p
h : HPow.hPow (β := ℕ) y 2 = -1
⊢ -1 = -HPow.hPow (α := ZMod p) (β := ℕ) 1 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (α := ZMod n) (-1)
y : ZMod p
h : -1 = y * y
⊢ HPow.hPow (β := ℕ) y 2 = -HPow.hPow (α := ZMod p) (β := ℕ) 1 2

Tactic:
rw [← sq, eq_comm, show (-1 : ZMod p) = -1 ^ 2 by ring] at h

Premises used: sq, eq_comm
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (α := ZMod n) (-1)
y : ZMod p
h : HPow.hPow (β := ℕ) y 2 = -HPow.hPow (α := ZMod p) (β := ℕ) 1 2
⊢ Fact (Prime p)

Tactic:
have : Fact p.Prime := ⟨Nat.prime_of_mem_primeFactors hp⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (α := ZMod n) (-1)
y : ZMod p
h : HPow.hPow (β := ℕ) y 2 = -HPow.hPow (α := ZMod p) (β := ℕ) 1 2
this : Fact (Prime p)
⊢ p % 4 ≠ 3

Tactic:
ZMod.mod_four_ne_three_of_sq_eq_neg_sq' one_ne_zero h

Premises used: one_ne_zero, ZMod.mod_four_ne_three_of_sq_eq_neg_sq'
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (α := ZMod n) (-1)
y : ZMod p
h : HPow.hPow (β := ℕ) y 2 = -HPow.hPow (α := ZMod p) (β := ℕ) 1 2
this : Fact (Prime p)
⊢ p % 4 ≠ 3

Tactic:
exact ZMod.mod_four_ne_three_of_sq_eq_neg_sq' one_ne_zero h

Premises used: one_ne_zero, ZMod.mod_four_ne_three_of_sq_eq_neg_sq'
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn : Squarefree n
⊢ IsSquare (α := ZMod n) (-1) ↔ ∀ q ∈ n.primeFactors, q % 4 ≠ 3

Tactic:
⟨fun H q hq ↦ Nat.mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one hq H,
    fun H ↦ ?_⟩

Premises used: Iff.intro, Nat.mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn : Squarefree n
refine : ∀ (H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3), IsSquare (α := ZMod n) (-1)
⊢ IsSquare (α := ZMod n) (-1) ↔ ∀ q ∈ n.primeFactors, q % 4 ≠ 3

Tactic:
refine ⟨fun H q hq ↦ Nat.mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one hq H,
    fun H ↦ ?_⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
hn : Squarefree (R := ℕ) 0
H : ∀ q ∈ Nat.primeFactors 0, q % 4 ≠ 3
⊢ IsSquare (α := ZMod 0) (-1)

Tactic:
False.elim (hn.ne_zero rfl)

Premises used: False.elim, Squarefree.ne_zero, rfl
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
hn : Squarefree (R := ℕ) 0
H : ∀ q ∈ Nat.primeFactors 0, q % 4 ≠ 3
⊢ IsSquare (α := ZMod 0) (-1)

Tactic:
exact False.elim (hn.ne_zero rfl)

Premises used: False.elim, Squarefree.ne_zero, rfl
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
hn : Squarefree (R := ℕ) 1
H : ∀ q ∈ Nat.primeFactors 1, q % 4 ≠ 3
⊢ -1 = HMul.hMul (α := ZMod 1) 0 0

Tactic:
simp only [mul_zero, eq_iff_true_of_subsingleton]

Premises used: MulZeroClass.mul_zero, eq_iff_true_of_subsingleton
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
hn : Squarefree (R := ℕ) 1
H : ∀ q ∈ Nat.primeFactors 1, q % 4 ≠ 3
⊢ IsSquare (α := ZMod 1) (-1)

Tactic:
exact ⟨0, by simp only [mul_zero, eq_iff_true_of_subsingleton]⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
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
⊢ Fact (Nat.Prime p)

Tactic:
have : Fact p.Prime := ⟨hpp⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
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
this : Fact (Nat.Prime p)
by_contra : ∀ (hc : ¬p.Coprime n), False
⊢ p.Coprime n

Tactic:
by_contra hc
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
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
this : Fact (Nat.Prime p)
hc : ¬p.Coprime n
⊢ False

Tactic:
hpp.not_isUnit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)

Premises used: Iff.mpr, Irreducible.not_isUnit, mul_dvd_mul_left, Nat.Prime.dvd_iff_not_coprime
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
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
this : Fact (Nat.Prime p)
hc : ¬p.Coprime n
⊢ False

Tactic:
exact hpp.not_isUnit (hn p <| mul_dvd_mul_left p <| hpp.dvd_iff_not_coprime.mpr hc)

Premises used: Iff.mpr, Irreducible.not_isUnit, mul_dvd_mul_left, Nat.Prime.dvd_iff_not_coprime
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
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
this : Fact (Nat.Prime p)
⊢ p.Coprime n

Tactic:
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)
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
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
this : Fact (Nat.Prime p)
hcp : p.Coprime n
⊢ IsSquare (α := ZMod p) (-1)

Tactic:
have hp₁ := ZMod.exists_sq_eq_neg_one_iff.mpr <| H _ <|
      Nat.mem_primeFactors.mpr ⟨hpp, Nat.dvd_mul_right .., Squarefree.ne_zero hn⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
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
this : Fact (Nat.Prime p)
hcp : p.Coprime n
hp₁ : IsSquare (α := ZMod p) (-1)
⊢ IsSquare (α := ZMod (p * n)) (-1)

Tactic:
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⟩

Premises used: Nat.dvd_of_mem_primeFactors, Iff.mpr, dvd_mul_of_dvd_right, Nat.prime_of_mem_primeFactors, Squarefree.ne_zero, And.intro, ZMod.isSquare_neg_one_mul, Squarefree.of_mul_right, Nat.mem_primeFactors
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
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
this : Fact (Nat.Prime p)
hcp : p.Coprime n
hp₁ : IsSquare (α := ZMod p) (-1)
⊢ IsSquare (α := ZMod (p * n)) (-1)

Tactic:
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⟩

Premises used: Nat.dvd_of_mem_primeFactors, Iff.mpr, dvd_mul_of_dvd_right, Nat.prime_of_mem_primeFactors, Squarefree.ne_zero, And.intro, ZMod.isSquare_neg_one_mul, Squarefree.of_mul_right, Nat.mem_primeFactors
-- Module: Mathlib.NumberTheory.SumTwoSquares
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)
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)
⊢ IsSquare (α := ZMod 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⟩

Premises used: False.elim, induction_on_primes, Squarefree.ne_zero
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn : Squarefree n
⊢ ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn : Squarefree n
⊢ ∀ (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
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
rw : (∀ q ∈ n.primeFactors, q % 4 ≠ 3) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
⊢ IsSquare (α := ZMod n) (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
rw [ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three hn]

Premises used: ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three
-- Module: Mathlib.NumberTheory.SumTwoSquares
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

Tactic:
⟨?_, fun H q hq => H <| Nat.dvd_of_mem_primeFactors hq⟩

Premises used: Nat.dvd_of_mem_primeFactors, Iff.intro
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
refine : (∀ q ∈ n.primeFactors, q % 4 ≠ 3) → ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
⊢ (∀ 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⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
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

Tactic:
@induction_on_primes _ ?_ ?_ (fun p q hp hq hpq => ?_)

Premises used: induction_on_primes
-- Module: Mathlib.NumberTheory.SumTwoSquares
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
refine_3 : ∀ (p q : ℕ) (hp : Nat.Prime p) (hq : q ∣ n → q % 4 ≠ 3) (hpq : p * q ∣ n), p * q % 4 ≠ 3
⊢ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
refine @induction_on_primes _ ?_ ?_ (fun p q hp hq hpq => ?_)

Premises used: induction_on_primes
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
h : 0 ∣ n
⊢ HMod.hMod (α := ℕ) 0 4 ≠ 3

Tactic:
simp
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
⊢ 0 ∣ n → HMod.hMod (α := ℕ) 0 4 ≠ 3

Tactic:
exact fun _ => by simp
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
h : 1 ∣ n
⊢ HMod.hMod (α := ℕ) 1 4 ≠ 3

Tactic:
simp
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
⊢ 1 ∣ n → HMod.hMod (α := ℕ) 1 4 ≠ 3

Tactic:
exact fun _ => by simp
-- Module: Mathlib.NumberTheory.SumTwoSquares
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 % 4 ≠ 3

Tactic:
replace hp := H _ <|
      Nat.mem_primeFactors.mpr ⟨hp, dvd_of_mul_right_dvd hpq, Squarefree.ne_zero hn⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
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
⊢ q % 4 ≠ 3

Tactic:
replace hq := hq (dvd_of_mul_left_dvd hpq)
-- Module: Mathlib.NumberTheory.SumTwoSquares
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
⊢ 3 = HMod.hMod (α := ℕ) 3 4

Tactic:
simp
-- Module: Mathlib.NumberTheory.SumTwoSquares
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 ≠ HMod.hMod (α := ℕ) 3 4
hq : q % 4 ≠ 3
⊢ 3 = HMod.hMod (α := ℕ) 3 4

Tactic:
simp
-- Module: Mathlib.NumberTheory.SumTwoSquares
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 ≠ HMod.hMod (α := ℕ) 3 4
hq : q % 4 ≠ HMod.hMod (α := ℕ) 3 4
⊢ 3 = HMod.hMod (α := ℕ) 3 4

Tactic:
simp
-- Module: Mathlib.NumberTheory.SumTwoSquares
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
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)
⊢ p * q % 4 ≠ 3

Tactic:
rw [show 3 = 3 % 4 by simp, Ne, ← ZMod.natCast_eq_natCast_iff'] at hp hq ⊢

Premises used: Ne, ZMod.natCast_eq_natCast_iff'
-- Module: Mathlib.NumberTheory.SumTwoSquares
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)
refine_3 : ¬HMul.hMul (α := ZMod 4) (↑p : ZMod 4) (↑q : ZMod 4) = (↑3 : ZMod 4)
⊢ ¬Eq (α := ZMod 4) (↑(p * q) : ZMod 4) (↑3 : ZMod 4)

Tactic:
rw [Nat.cast_mul]

Premises used: Nat.cast_mul
-- Module: Mathlib.NumberTheory.SumTwoSquares
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)
⊢ ¬HMul.hMul (α := ZMod 4) (↑p : ZMod 4) (↑q : ZMod 4) = (↑3 : ZMod 4)

Tactic:
help p q hp hq

Premises used: Nat.cast
-- Module: Mathlib.NumberTheory.SumTwoSquares
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)
⊢ ¬HMul.hMul (α := ZMod 4) (↑p : ZMod 4) (↑q : ZMod 4) = (↑3 : ZMod 4)

Tactic:
exact help p q hp hq

Premises used: Nat.cast
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
h : IsSquare (α := ZMod 0) (-1)
⊢ ∃ (x : ℕ) (y : ℕ), 0 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
⟨0, 0, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
h : IsSquare (α := ZMod 0) (-1)
⊢ ∃ (x : ℕ) (y : ℕ), 0 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
exact ⟨0, 0, rfl⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
h : IsSquare (α := ZMod 1) (-1)
⊢ ∃ (x : ℕ) (y : ℕ), 1 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
⟨0, 1, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
h : IsSquare (α := ZMod 1) (-1)
⊢ ∃ (x : ℕ) (y : ℕ), 1 = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
exact ⟨0, 1, rfl⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
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)
⊢ Fact (Prime p)

Tactic:
have : Fact p.Prime := ⟨hpp⟩
-- Module: Mathlib.NumberTheory.SumTwoSquares
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)
⊢ IsSquare (α := ZMod p) (-1)

Tactic:
have hp : IsSquare (-1 : ZMod p) := ZMod.isSquare_neg_one_of_dvd ⟨n, rfl⟩ h
-- Module: Mathlib.NumberTheory.SumTwoSquares
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)
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
⊢ ∃ (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)

Premises used: ZMod.exists_sq_eq_neg_one_iff, Nat.Prime.sq_add_sq, Iff.mp
-- Module: Mathlib.NumberTheory.SumTwoSquares
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
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
⊢ ∃ (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)

Premises used: ZMod.isSquare_neg_one_of_dvd, Exists.intro, mul_comm
-- Module: Mathlib.NumberTheory.SumTwoSquares
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 : ℕ
hxy : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ ∃ (x : ℕ) (y : ℕ), p * n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
Nat.sq_add_sq_mul huv.symm hxy

Premises used: Eq.symm, Nat.sq_add_sq_mul
-- Module: Mathlib.NumberTheory.SumTwoSquares
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 : ℕ
hxy : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ ∃ (x : ℕ) (y : ℕ), p * n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2

Tactic:
exact Nat.sq_add_sq_mul huv.symm hxy

Premises used: Eq.symm, Nat.sq_add_sq_mul
-- Module: Mathlib.NumberTheory.SumTwoSquares
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
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
⊢ ∃ (x : ℕ) (y : ℕ), 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

Premises used: induction_on_primes, Nat.zero
-- Module: Mathlib.NumberTheory.SumTwoSquares
Goal:
n x y : ℤ
h : n = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
hc : IsCoprime x y
⊢ IsCoprime (HPow.hPow (β := ℕ) x 2) (HPow.hPow (β := ℕ) y 2)

Tactic:
have hc2 : IsCoprime (x ^ 2) (y ^ 2) := hc.pow
-- Module: Mathlib.NumberTheory.SumTwoSquares
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)
⊢ HPow.hPow (β := ℕ) y 2 = n + -1 * HPow.hPow (β := ℕ) x 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.SumTwoSquares
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 (HPow.hPow (β := ℕ) x 2) (n + -1 * HPow.hPow (β := ℕ) x 2)

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