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 :
  ∃ 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
a b c d m : ℕ
hmin :
  ∀ m_1 < 2 * 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 : 2 * m < p
hm₀ : 0 < 2 * m
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m * p
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
hm₂ : 0 < m
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m * p

Tactic:
rw [mul_pos_iff_of_pos_left two_pos] at hm₀

Premises used: mul_pos_iff_of_pos_left
-- 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 :
  ∃ 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
a b c d m : ℕ
hmin :
  ∀ m_1 < 2 * 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 : 2 * m < p
hm₀ : 0 < 2 * m
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m * p
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
hm₂ : 0 < m
habcd₁ : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m * p
⊢ 1 < 2 * m

Tactic:
rw [mul_pos_iff_of_pos_left two_pos] at hm₀

Premises used: mul_pos_iff_of_pos_left
-- 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 :
  ∃ 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
a b c d m : ℕ
hmin :
  ∀ m_1 < 2 * 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 : 2 * m < p
hm₀ : 0 < 2 * m
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m * p
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
hm₂ : 0 < m
habcd₁ : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m * p
hm₃ : 1 < 2 * m
⊢ NeZero (2 * m)

Tactic:
rw [mul_pos_iff_of_pos_left two_pos] at hm₀

Premises used: mul_pos_iff_of_pos_left
-- 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 :
  ∃ 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
a b c d m : ℕ
hmin :
  ∀ m_1 < 2 * 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 : 2 * m < p
hm₀ : 0 < m
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m * p
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
⊢ m < 2 * m

Tactic:
simpa [two_mul]

Premises used: two_mul
-- 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 :
  ∃ 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
a b c d m : ℕ
hmin :
  ∀ m_1 < 2 * 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 : 2 * m < p
hm₀ : 0 < m
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m * p
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
⊢ m < 2 * m

Tactic:
have hm₂ : m < 2 * m := by simpa [two_mul]
-- 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 :
  ∃ 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
a b c d m : ℕ
hmin :
  ∀ m_1 < 2 * 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 : 2 * m < p
hm₀ : 0 < m
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m * p
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
hm₂ : m < 2 * m
⊢ Eq (α := ℤ) (↑(HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) : ℤ)
    (↑(2 * m * p) : ℤ)

Tactic:
apply_fun (Nat.cast : ℕ → ℤ) at habcd

Premises used: Nat.cast
-- 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 :
  ∃ 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
a b c d m : ℕ
hmin :
  ∀ m_1 < 2 * 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 : 2 * m < p
hm₀ : 0 < m
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
hm₂ : m < 2 * m
habcd :
  Eq (α := ℤ) (↑(HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) : ℤ)
    (↑(2 * m * p) : ℤ)
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
        HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
      HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2 =
    2 * HMul.hMul (α := ℤ) (↑m : ℤ) (↑p : ℤ)

Tactic:
push_cast [mul_assoc] at habcd

Premises used: mul_assoc
-- 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 :
  ∃ 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
a b c d m : ℕ
hmin :
  ∀ m_1 < 2 * 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 : 2 * m < p
hm₀ : 0 < m
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
hm₂ : m < 2 * m
habcd :
  HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
        HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
      HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2 =
    2 * HMul.hMul (α := ℤ) (↑m : ℤ) (↑p : ℤ)
pos :
  ∀ (w w_1 w_2 w_3 : ℤ)
    (h :
      HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) w_1 2 + HPow.hPow (β := ℕ) w_2 2 + HPow.hPow (β := ℕ) w_3 2 =
        HMul.hMul (α := ℤ) (↑m : ℤ) (↑p : ℤ)),
    False
⊢ False

Tactic:
obtain ⟨_, _, _, _, h⟩ := sum_four_squares_of_two_mul_sum_four_squares habcd

Premises used: _private.0.Nat.sum_four_squares_of_two_mul_sum_four_squares
-- 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 :
  ∃ 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
a b c d m : ℕ
hmin :
  ∀ m_1 < 2 * 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 : 2 * m < p
hm₀ : 0 < m
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
hm₂ : m < 2 * m
habcd :
  HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
        HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
      HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2 =
    2 * HMul.hMul (α := ℤ) (↑m : ℤ) (↑p : ℤ)
w w_1 w_2 w_3 : ℤ
h :
  HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) w_1 2 + HPow.hPow (β := ℕ) w_2 2 + HPow.hPow (β := ℕ) w_3 2 =
    HMul.hMul (α := ℤ) (↑m : ℤ) (↑p : ℤ)
⊢ False

Tactic:
hmin m hm₂ ⟨hm₂.trans hmp, hm₀, _, _, _, _, natAbs_iff.2 h⟩

Premises used: Iff.mpr, 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 :
  ∃ 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
a b c d m : ℕ
hmin :
  ∀ m_1 < 2 * 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 : 2 * m < p
hm₀ : 0 < m
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
hm₂ : m < 2 * m
habcd :
  HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
        HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
      HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2 =
    2 * HMul.hMul (α := ℤ) (↑m : ℤ) (↑p : ℤ)
w w_1 w_2 w_3 : ℤ
h :
  HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) w_1 2 + HPow.hPow (β := ℕ) w_2 2 + HPow.hPow (β := ℕ) w_3 2 =
    HMul.hMul (α := ℤ) (↑m : ℤ) (↑p : ℤ)
⊢ False

Tactic:
exact hmin m hm₂ ⟨hm₂.trans hmp, hm₀, _, _, _, _, natAbs_iff.2 h⟩

Premises used: Iff.mpr, 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 : ℕ → ℤ), (∀ (x : ℕ), 2 * (f x).natAbs < m) ∧ ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)

Tactic:
⟨fun x ↦ (x : ZMod m).valMinAbs, fun x ↦ ?_, fun x ↦ (x : ZMod m).coe_valMinAbs⟩

Premises used: ZMod.valMinAbs, ZMod.coe_valMinAbs, Nat.cast, 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 : NeZero m
hm : ¬2 ∣ m
refine : ∀ (x : ℕ), 2 * natAbs ((fun (x : ℕ) ↦ ZMod.valMinAbs (n := m) (↑x : ZMod m)) x) < m
⊢ ∃ (f : ℕ → ℤ), (∀ (x : ℕ), 2 * (f x).natAbs < m) ∧ ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)

Tactic:
refine ⟨fun x ↦ (x : ZMod m).valMinAbs, fun x ↦ ?_, fun x ↦ (x : ZMod m).coe_valMinAbs⟩
-- 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
x : ℕ
⊢ 2 * natAbs ((fun (x : ℕ) ↦ ZMod.valMinAbs (n := m) (↑x : ZMod m)) x) < m

Tactic:
(mul_le_mul' le_rfl (x : ZMod m).natAbs_valMinAbs_le).trans_lt
        (Nat.mul_div_lt_iff_not_dvd.2 hm)

Premises used: Iff.mpr, le_rfl, Nat.cast, Nat.mul_div_lt_iff_not_dvd, ZMod.natAbs_valMinAbs_le, LE.le.trans_lt, mul_le_mul'
-- 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
x : ℕ
⊢ 2 * natAbs ((fun (x : ℕ) ↦ ZMod.valMinAbs (n := m) (↑x : ZMod m)) x) < m

Tactic:
exact (mul_le_mul' le_rfl (x : ZMod m).natAbs_valMinAbs_le).trans_lt
        (Nat.mul_div_lt_iff_not_dvd.2 hm)

Premises used: Iff.mpr, le_rfl, Nat.cast, Nat.mul_div_lt_iff_not_dvd, ZMod.natAbs_valMinAbs_le, LE.le.trans_lt, mul_le_mul'
-- 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
neg :
  ∀ (f : ℕ → ℤ) (hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m)
    (hf_mod : ∀ (x : ℕ), Eq (α := ZMod m) (↑(f x) : ZMod m) (↑x : ZMod m)), False
⊢ False

Tactic:
obtain ⟨f, hf_lt, hf_mod⟩ :
        ∃ f : ℕ → ℤ, (∀ x, 2 * (f x).natAbs < m) ∧ ∀ x, (f x : ZMod m) = x := by
      refine ⟨fun x ↦ (x : ZMod m).valMinAbs, fun x ↦ ?_, fun x ↦ (x : ZMod m).coe_valMinAbs⟩
      exact (mul_le_mul' le_rfl (x : ZMod m).natAbs_valMinAbs_le).trans_lt
        (Nat.mul_div_lt_iff_not_dvd.2 hm)
-- 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)
simp :
  Eq (α := ZMod m)
    (↑(↑(HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
              HPow.hPow (β := ℕ) (f d).natAbs 2) :
          ℤ) :
      ZMod m)
    0
⊢ m ∣
    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:
simp only [← Int.natCast_dvd_natCast, ← ZMod.intCast_zmod_eq_zero_iff_dvd]

Premises used: ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natCast_dvd_natCast
-- 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)
push_cast :
  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
⊢ Eq (α := ZMod m)
    (↑(↑(HPow.hPow (β := ℕ) (f a).natAbs 2 + HPow.hPow (β := ℕ) (f b).natAbs 2 + HPow.hPow (β := ℕ) (f c).natAbs 2 +
              HPow.hPow (β := ℕ) (f d).natAbs 2) :
          ℤ) :
      ZMod m)
    0

Tactic:
push_cast [hf_mod, sq_abs]

Premises used: sq_abs