awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this_2 : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : (↑m : ℤ) ∣ w
hx : (↑m : ℤ) ∣ x
hy : (↑m : ℤ) ∣ y
hz : (↑m : ℤ) ∣ z
h :
  HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
this :
  HPow.hPow (β := ℕ) (w / (↑m : ℤ)).natAbs 2 + HPow.hPow (β := ℕ) (x / (↑m : ℤ)).natAbs 2 +
        HPow.hPow (β := ℕ) (y / (↑m : ℤ)).natAbs 2 +
      HPow.hPow (β := ℕ) (z / (↑m : ℤ)).natAbs 2 =
    r * p
⊢ False

Tactic:
hmin r hrm ⟨hrm.trans hmp, hr₀, _, _, _, _, this⟩

Premises used: And.intro, Exists.intro, LT.lt.trans
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this_2 : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : (↑m : ℤ) ∣ w
hx : (↑m : ℤ) ∣ x
hy : (↑m : ℤ) ∣ y
hz : (↑m : ℤ) ∣ z
h :
  HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
this :
  HPow.hPow (β := ℕ) (w / (↑m : ℤ)).natAbs 2 + HPow.hPow (β := ℕ) (x / (↑m : ℤ)).natAbs 2 +
        HPow.hPow (β := ℕ) (y / (↑m : ℤ)).natAbs 2 +
      HPow.hPow (β := ℕ) (z / (↑m : ℤ)).natAbs 2 =
    r * p
⊢ False

Tactic:
exact hmin r hrm ⟨hrm.trans hmp, hr₀, _, _, _, _, this⟩

Premises used: And.intro, Exists.intro, LT.lt.trans
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
rw :
  HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f d).natAbs 2 +
      HPow.hPow (β := ℕ) (f c).natAbs 2 =
    HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2
⊢ HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)

Tactic:
rw [← natAbs_iff, natAbs_neg, ← hr]

Premises used: Int.natAbs_neg
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
⊢ HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f d).natAbs 2 +
      HPow.hPow (β := ℕ) (f c).natAbs 2 =
    HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2

Tactic:
ac_rfl
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr :
  HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
      HPow.hPow (β := ℕ) (f d).natAbs 2 =
    m * r
hr₀ : 0 < r
hrm : r < m
⊢ HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)

Tactic:
replace hr : (f b) ^ 2 + (f a) ^ 2 + (f d) ^ 2 + (-f c) ^ 2 = ↑(m * r) := by
      rw [← natAbs_iff, natAbs_neg, ← hr]
      ac_rfl
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr :
  HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)
⊢ Eq (α := ℤ)
    ((fun (x1 : ℤ) (x2 : ℕ) ↦ x1 * (↑x2 : ℤ))
      (HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 +
        HPow.hPow (β := ℕ) (-f c) 2)
      (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2))
    ((fun (x1 : ℤ) (x2 : ℕ) ↦ x1 * (↑x2 : ℤ)) (↑(m * r) : ℤ) (m * p))

Tactic:
have := congr_arg₂ (· * Nat.cast ·) hr habcd
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this_2 : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr :
  HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)
this :
  Eq (α := ℤ)
    ((fun (x1 : ℤ) (x2 : ℕ) ↦ x1 * (↑x2 : ℤ))
      (HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 +
        HPow.hPow (β := ℕ) (-f c) 2)
      (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2))
    ((fun (x1 : ℤ) (x2 : ℕ) ↦ x1 * (↑x2 : ℤ)) (↑(m * r) : ℤ) (m * p))
⊢ HPow.hPow (β := ℕ) (f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)) 2 +
          HPow.hPow (β := ℕ) (f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)) 2 +
        HPow.hPow (β := ℕ) (f b * (↑c : ℤ) - f a * (↑d : ℤ) + f d * (↑a : ℤ) + -f c * (↑b : ℤ)) 2 +
      HPow.hPow (β := ℕ) (f b * (↑d : ℤ) + f a * (↑c : ℤ) - f d * (↑b : ℤ) + -f c * (↑a : ℤ)) 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)

Tactic:
simp only [← _root_.euler_four_squares, Nat.cast_add, Nat.cast_pow] at this

Premises used: euler_four_squares, Nat.cast_add, Nat.cast_pow
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this_2 : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr :
  HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)
this :
  HPow.hPow (β := ℕ) (f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)) 2 +
          HPow.hPow (β := ℕ) (f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)) 2 +
        HPow.hPow (β := ℕ) (f b * (↑c : ℤ) - f a * (↑d : ℤ) + f d * (↑a : ℤ) + -f c * (↑b : ℤ)) 2 +
      HPow.hPow (β := ℕ) (f b * (↑d : ℤ) + f a * (↑c : ℤ) - f d * (↑b : ℤ) + -f c * (↑a : ℤ)) 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    (↑m : ℤ) ∣ w ∧
      (↑m : ℤ) ∣ x ∧
        (↑m : ℤ) ∣ y ∧
          (↑m : ℤ) ∣ z ∧
            HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
              HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)

Tactic:
⟨_, _, _, _, ?_, ?_, ?_, ?_, this⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this_2 : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr :
  HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)
this :
  HPow.hPow (β := ℕ) (f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)) 2 +
          HPow.hPow (β := ℕ) (f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)) 2 +
        HPow.hPow (β := ℕ) (f b * (↑c : ℤ) - f a * (↑d : ℤ) + f d * (↑a : ℤ) + -f c * (↑b : ℤ)) 2 +
      HPow.hPow (β := ℕ) (f b * (↑d : ℤ) + f a * (↑c : ℤ) - f d * (↑b : ℤ) + -f c * (↑a : ℤ)) 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
refine_1 : (↑m : ℤ) ∣ f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)
refine_2 : (↑m : ℤ) ∣ f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)
refine_3 : (↑m : ℤ) ∣ f b * (↑c : ℤ) - f a * (↑d : ℤ) + f d * (↑a : ℤ) + -f c * (↑b : ℤ)
refine_4 : (↑m : ℤ) ∣ f b * (↑d : ℤ) + f a * (↑c : ℤ) - f d * (↑b : ℤ) + -f c * (↑a : ℤ)
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    (↑m : ℤ) ∣ w ∧
      (↑m : ℤ) ∣ x ∧
        (↑m : ℤ) ∣ y ∧
          (↑m : ℤ) ∣ z ∧
            HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 =
              HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)

Tactic:
refine ⟨_, _, _, _, ?_, ?_, ?_, ?_, this⟩
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this_2 : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr :
  HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)
this :
  HPow.hPow (β := ℕ) (f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)) 2 +
          HPow.hPow (β := ℕ) (f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)) 2 +
        HPow.hPow (β := ℕ) (f b * (↑c : ℤ) - f a * (↑d : ℤ) + f d * (↑a : ℤ) + -f c * (↑b : ℤ)) 2 +
      HPow.hPow (β := ℕ) (f b * (↑d : ℤ) + f a * (↑c : ℤ) - f d * (↑b : ℤ) + -f c * (↑a : ℤ)) 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
⊢ (↑m : ℤ) ∣ f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)

Tactic:
simp [← ZMod.intCast_zmod_eq_zero_iff_dvd, hf_mod, mul_comm]

Premises used: ZMod.intCast_zmod_eq_zero_iff_dvd, mul_comm
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this_2 : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr :
  HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)
this_3 :
  HPow.hPow (β := ℕ) (f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)) 2 +
          HPow.hPow (β := ℕ) (f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)) 2 +
        HPow.hPow (β := ℕ) (f b * (↑c : ℤ) - f a * (↑d : ℤ) + f d * (↑a : ℤ) + -f c * (↑b : ℤ)) 2 +
      HPow.hPow (β := ℕ) (f b * (↑d : ℤ) + f a * (↑c : ℤ) - f d * (↑b : ℤ) + -f c * (↑a : ℤ)) 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
this :
  HPow.hPow (α := ZMod m) (β := ℕ) (↑a : ZMod m) 2 + HPow.hPow (α := ZMod m) (β := ℕ) (↑b : ZMod m) 2 +
        HPow.hPow (α := ZMod m) (β := ℕ) (↑c : ZMod m) 2 +
      HPow.hPow (α := ZMod m) (β := ℕ) (↑d : ZMod m) 2 =
    0
⊢ (↑m : ℤ) ∣ f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)

Tactic:
simpa [← ZMod.intCast_zmod_eq_zero_iff_dvd, hf_mod, sq, add_comm, add_assoc,
          add_left_comm] using this

Premises used: add_left_comm, add_assoc, sq, add_comm, ZMod.intCast_zmod_eq_zero_iff_dvd
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this_1 : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    HPow.hPow (β := ℕ) a.natAbs 2 + HPow.hPow (β := ℕ) b.natAbs 2 + HPow.hPow (β := ℕ) c.natAbs 2 +
          HPow.hPow (β := ℕ) d.natAbs 2 =
        k ↔
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
hm_1 :
  ∃ m < p,
    0 < m ∧
      ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
        HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
m : ℕ
hmin :
  ∀ m_1 < m,
    ¬(m_1 < p ∧
        0 < m_1 ∧
          ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
            HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = m * p
hm₁ : 1 < m
this_2 : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr :
  HPow.hPow (β := ℕ) (f b) 2 + HPow.hPow (β := ℕ) (f a) 2 + HPow.hPow (β := ℕ) (f d) 2 + HPow.hPow (β := ℕ) (-f c) 2 =
    (↑(m * r) : ℤ)
this :
  HPow.hPow (β := ℕ) (f b * (↑a : ℤ) - f a * (↑b : ℤ) - f d * (↑c : ℤ) - -f c * (↑d : ℤ)) 2 +
          HPow.hPow (β := ℕ) (f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)) 2 +
        HPow.hPow (β := ℕ) (f b * (↑c : ℤ) - f a * (↑d : ℤ) + f d * (↑a : ℤ) + -f c * (↑b : ℤ)) 2 +
      HPow.hPow (β := ℕ) (f b * (↑d : ℤ) + f a * (↑c : ℤ) - f d * (↑b : ℤ) + -f c * (↑a : ℤ)) 2 =
    HMul.hMul (α := ℤ) (↑(m * r) : ℤ) (↑(m * p) : ℤ)
refine_2 :
  HPow.hPow (α := ZMod m) (β := ℕ) (↑a : ZMod m) 2 + HPow.hPow (α := ZMod m) (β := ℕ) (↑b : ZMod m) 2 +
        HPow.hPow (α := ZMod m) (β := ℕ) (↑c : ZMod m) 2 +
      HPow.hPow (α := ZMod m) (β := ℕ) (↑d : ZMod m) 2 =
    0
⊢ (↑m : ℤ) ∣ f b * (↑b : ℤ) + f a * (↑a : ℤ) + f d * (↑d : ℤ) - -f c * (↑c : ℤ)

Tactic:
suffices ((a : ZMod m) ^ 2 + (b : ZMod m) ^ 2 + (c : ZMod m) ^ 2 + (d : ZMod m) ^ 2) = 0 by
        simpa [← ZMod.intCast_zmod_eq_zero_iff_dvd, hf_mod, sq, add_comm, add_assoc,
          add_left_comm] using this