awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
a b c d x y z w : ℕ
rw :
  Eq (α := ℤ)
    (↑(HPow.hPow (β := ℕ)
                (HMul.hMul (α := ℤ) (↑a : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑y : ℤ) -
                      HMul.hMul (α := ℤ) (↑c : ℤ) (↑z : ℤ) -
                    HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ)).natAbs
                2 +
              HPow.hPow (β := ℕ)
                (HMul.hMul (α := ℤ) (↑a : ℤ) (↑y : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑x : ℤ) +
                      HMul.hMul (α := ℤ) (↑c : ℤ) (↑w : ℤ) -
                    HMul.hMul (α := ℤ) (↑d : ℤ) (↑z : ℤ)).natAbs
                2 +
            HPow.hPow (β := ℕ)
              (HMul.hMul (α := ℤ) (↑a : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑w : ℤ) +
                    HMul.hMul (α := ℤ) (↑c : ℤ) (↑x : ℤ) +
                  HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ)).natAbs
              2 +
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := ℤ) (↑a : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑z : ℤ) -
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑y : ℤ) +
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑x : ℤ)).natAbs
            2) :
      ℤ)
    (↑((HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) *
          (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 + HPow.hPow (β := ℕ) w 2)) :
      ℤ)
⊢ HPow.hPow (β := ℕ)
            (HMul.hMul (α := ℤ) (↑a : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑y : ℤ) -
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑z : ℤ) -
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ)).natAbs
            2 +
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := ℤ) (↑a : ℤ) (↑y : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑x : ℤ) +
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑w : ℤ) -
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑z : ℤ)).natAbs
            2 +
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := ℤ) (↑a : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑w : ℤ) +
                HMul.hMul (α := ℤ) (↑c : ℤ) (↑x : ℤ) +
              HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ)).natAbs
          2 +
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := ℤ) (↑a : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑z : ℤ) -
              HMul.hMul (α := ℤ) (↑c : ℤ) (↑y : ℤ) +
            HMul.hMul (α := ℤ) (↑d : ℤ) (↑x : ℤ)).natAbs
        2 =
    (HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) *
      (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 + HPow.hPow (β := ℕ) w 2)

Tactic:
rw [← Int.natCast_inj]

Premises used: Int.natCast_inj
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
a b c d x y z w : ℕ
push_cast :
  HPow.hPow (β := ℕ)
            |HMul.hMul (α := ℤ) (↑a : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑y : ℤ) -
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑z : ℤ) -
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ)|
            2 +
          HPow.hPow (β := ℕ)
            |HMul.hMul (α := ℤ) (↑a : ℤ) (↑y : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑x : ℤ) +
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑w : ℤ) -
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑z : ℤ)|
            2 +
        HPow.hPow (β := ℕ)
          |HMul.hMul (α := ℤ) (↑a : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑w : ℤ) +
                HMul.hMul (α := ℤ) (↑c : ℤ) (↑x : ℤ) +
              HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ)|
          2 +
      HPow.hPow (β := ℕ)
        |HMul.hMul (α := ℤ) (↑a : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑z : ℤ) -
              HMul.hMul (α := ℤ) (↑c : ℤ) (↑y : ℤ) +
            HMul.hMul (α := ℤ) (↑d : ℤ) (↑x : ℤ)|
        2 =
    (HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
          HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
        HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2) *
      (HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2 +
          HPow.hPow (α := ℤ) (β := ℕ) (↑z : ℤ) 2 +
        HPow.hPow (α := ℤ) (β := ℕ) (↑w : ℤ) 2)
⊢ Eq (α := ℤ)
    (↑(HPow.hPow (β := ℕ)
                (HMul.hMul (α := ℤ) (↑a : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑y : ℤ) -
                      HMul.hMul (α := ℤ) (↑c : ℤ) (↑z : ℤ) -
                    HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ)).natAbs
                2 +
              HPow.hPow (β := ℕ)
                (HMul.hMul (α := ℤ) (↑a : ℤ) (↑y : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑x : ℤ) +
                      HMul.hMul (α := ℤ) (↑c : ℤ) (↑w : ℤ) -
                    HMul.hMul (α := ℤ) (↑d : ℤ) (↑z : ℤ)).natAbs
                2 +
            HPow.hPow (β := ℕ)
              (HMul.hMul (α := ℤ) (↑a : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑w : ℤ) +
                    HMul.hMul (α := ℤ) (↑c : ℤ) (↑x : ℤ) +
                  HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ)).natAbs
              2 +
          HPow.hPow (β := ℕ)
            (HMul.hMul (α := ℤ) (↑a : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑z : ℤ) -
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑y : ℤ) +
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑x : ℤ)).natAbs
            2) :
      ℤ)
    (↑((HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) *
          (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 + HPow.hPow (β := ℕ) w 2)) :
      ℤ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
a b c d x y z w : ℕ
⊢ HPow.hPow (β := ℕ)
            |HMul.hMul (α := ℤ) (↑a : ℤ) (↑x : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑y : ℤ) -
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑z : ℤ) -
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑w : ℤ)|
            2 +
          HPow.hPow (β := ℕ)
            |HMul.hMul (α := ℤ) (↑a : ℤ) (↑y : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑x : ℤ) +
                  HMul.hMul (α := ℤ) (↑c : ℤ) (↑w : ℤ) -
                HMul.hMul (α := ℤ) (↑d : ℤ) (↑z : ℤ)|
            2 +
        HPow.hPow (β := ℕ)
          |HMul.hMul (α := ℤ) (↑a : ℤ) (↑z : ℤ) - HMul.hMul (α := ℤ) (↑b : ℤ) (↑w : ℤ) +
                HMul.hMul (α := ℤ) (↑c : ℤ) (↑x : ℤ) +
              HMul.hMul (α := ℤ) (↑d : ℤ) (↑y : ℤ)|
          2 +
      HPow.hPow (β := ℕ)
        |HMul.hMul (α := ℤ) (↑a : ℤ) (↑w : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑z : ℤ) -
              HMul.hMul (α := ℤ) (↑c : ℤ) (↑y : ℤ) +
            HMul.hMul (α := ℤ) (↑d : ℤ) (↑x : ℤ)|
        2 =
    (HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
          HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
        HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2) *
      (HPow.hPow (α := ℤ) (β := ℕ) (↑x : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑y : ℤ) 2 +
          HPow.hPow (α := ℤ) (β := ℕ) (↑z : ℤ) 2 +
        HPow.hPow (α := ℤ) (β := ℕ) (↑w : ℤ) 2)

Tactic:
simp only [sq_abs, _root_.euler_four_squares]

Premises used: euler_four_squares, sq_abs
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
⊢ Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)

Tactic:
simp [← h]
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
⊢ HMul.hMul (α := ℤ) 2 2 ≠ 0

Tactic:
decide
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
rw : 2 * (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) = HPow.hPow (β := ℕ) (x - y) 2 + HPow.hPow (β := ℕ) (x + y) 2
⊢ HMul.hMul (α := ℤ) 2 2 * m = HPow.hPow (β := ℕ) (x - y) 2 + HPow.hPow (β := ℕ) (x + y) 2

Tactic:
rw [mul_assoc, h]

Premises used: mul_assoc
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
⊢ 2 * (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2) = HPow.hPow (β := ℕ) (x - y) 2 + HPow.hPow (β := ℕ) (x + y) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
rw : 2 ∣ x + y
rw₁ : 2 ∣ x - y
⊢ HPow.hPow (β := ℕ) (x - y) 2 + HPow.hPow (β := ℕ) (x + y) 2 =
    HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2

Tactic:
rw [Int.mul_ediv_cancel' _, Int.mul_ediv_cancel' _]

Premises used: Int.mul_ediv_cancel'
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
⊢ 2 ∣ x + y

Tactic:
simpa [sq, parity_simps, ← even_iff_two_dvd]

Premises used: sq, even_iff_two_dvd
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
⊢ 2 ∣ x - y

Tactic:
simpa [sq, parity_simps, ← even_iff_two_dvd]

Premises used: sq, even_iff_two_dvd
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
m x y : ℤ
h : 2 * m = HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2
this : Even (HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2)
nlinarith :
  HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2 <
      HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2) →
    -1 +
        (HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2 + 1 -
          HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2)) =
      0
nlinarith₁ :
  HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2) <
      HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2 →
    -1 +
        (HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2) + 1 -
          (HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2)) =
      0
⊢ HPow.hPow (β := ℕ) (2 * ((x - y) / 2)) 2 + HPow.hPow (β := ℕ) (2 * ((x + y) / 2)) 2 =
    HMul.hMul (α := ℤ) 2 2 * (HPow.hPow (β := ℕ) ((x - y) / 2) 2 + HPow.hPow (β := ℕ) ((x + y) / 2) 2)

Tactic:
nlinarith
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
a b c d k m : ℕ
h : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = k * m
ha : 2 * a < m
hb : 2 * b < m
hc : 2 * c < m
hd : 2 * d < m
nlinarith :
  m ≤ k →
    HMul.hMul (α := ℤ) 4 (-1) + 10 * HSub.hSub (α := ℤ) 0 (↑a : ℤ) + 2 * HSub.hSub (α := ℤ) 0 (↑b : ℤ) +
                                2 * HSub.hSub (α := ℤ) 0 (↑c : ℤ) +
                              2 * HSub.hSub (α := ℤ) 0 (↑d : ℤ) +
                            4 *
                              -(HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 +
                                      HPow.hPow (α := ℤ) (β := ℕ) (↑c : ℤ) 2 +
                                    HPow.hPow (α := ℤ) (β := ℕ) (↑d : ℤ) 2 -
                                  HMul.hMul (α := ℤ) (↑k : ℤ) (↑m : ℤ)) +
                          4 * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ)) +
                        (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ))) +
                      (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑b : ℤ) + 1 - (↑m : ℤ))) +
                    (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑c : ℤ) + 1 - (↑m : ℤ))) +
                  (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * (HMul.hMul (α := ℤ) 2 (↑d : ℤ) + 1 - (↑m : ℤ))) +
                4 * (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * HSub.hSub (α := ℤ) (↑m : ℤ) (↑k : ℤ)) +
              2 * (0 - HSub.hSub (α := ℤ) 0 (↑a : ℤ) * (HMul.hMul (α := ℤ) 2 (↑a : ℤ) + 1 - (↑m : ℤ))) +
            2 * (0 - HSub.hSub (α := ℤ) 0 (↑b : ℤ) * (HMul.hMul (α := ℤ) 2 (↑b : ℤ) + 1 - (↑m : ℤ))) +
          2 * (0 - HSub.hSub (α := ℤ) 0 (↑c : ℤ) * (HMul.hMul (α := ℤ) 2 (↑c : ℤ) + 1 - (↑m : ℤ))) +
        2 * (0 - HSub.hSub (α := ℤ) 0 (↑d : ℤ) * (HMul.hMul (α := ℤ) 2 (↑d : ℤ) + 1 - (↑m : ℤ))) =
      0
nlinarith₁ : m ≤ k → GT.gt (α := ℤ) 4 0
nlinarith₂ : m ≤ k → GT.gt (α := ℤ) 10 0
nlinarith₃ nlinarith₄ nlinarith₅ : m ≤ k → GT.gt (α := ℤ) 2 0
nlinarith₆ nlinarith₇ nlinarith₈ : m ≤ k → GT.gt (α := ℤ) 4 0
nlinarith₉ nlinarith₁₀ nlinarith₁₁ nlinarith₁₂ : m ≤ k → GT.gt (α := ℤ) 2 0
⊢ k < m

Tactic:
nlinarith
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
inl :
  ∀ [hp : Fact (Nat.Prime 2)],
    ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < 2 ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * 2
inr :
  ∀ (hodd : Odd p),
    ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p

Tactic:
rcases hp.1.eq_two_or_odd' with (rfl | hodd)

Premises used: Nat.Prime.eq_two_or_odd', rfl, Fact.out
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
hp : Fact (Nat.Prime 2)
h :
  LT.lt (α := ℕ) 0 1 ∧
    LT.lt (α := ℕ) 1 2 ∧ HPow.hPow (α := ℕ) (β := ℕ) 1 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 + 1 = HMul.hMul (α := ℕ) 1 2
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < 2 ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * 2

Tactic:
use 1, 0, 1
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
hp : Fact (Nat.Prime 2)
⊢ LT.lt (α := ℕ) 0 1 ∧
    LT.lt (α := ℕ) 1 2 ∧ HPow.hPow (α := ℕ) (β := ℕ) 1 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 + 1 = HMul.hMul (α := ℕ) 1 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
inr :
  ∀ (a b : ℕ) (ha : a ≤ p / 2) (hb : b ≤ p / 2)
    (hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]),
    ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p

Tactic:
rcases Nat.sq_add_sq_zmodEq p (-1) with ⟨a, b, ha, hb, hab⟩

Premises used: OfNat.ofNat, Nat.sq_add_sq_zmodEq, Neg.neg
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
inr :
  ∀ (k : ℤ) (hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 - -1 = (↑p : ℤ) * k),
    ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p

Tactic:
rcases Int.modEq_iff_dvd.1 hab.symm with ⟨k, hk⟩

Premises used: Int.ModEq.symm, Int.modEq_iff_dvd, Iff.mp
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℤ
hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 - -1 = (↑p : ℤ) * k
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 = k * (↑p : ℤ)

Tactic:
rw [sub_neg_eq_add, mul_comm] at hk

Premises used: mul_comm, sub_neg_eq_add
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℤ
hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 = k * (↑p : ℤ)
⊢ 0 < k

Tactic:
pos_of_mul_pos_left ?_ (Nat.cast_nonneg p)

Premises used: pos_of_mul_pos_left, Nat.cast_nonneg
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℤ
hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 = k * (↑p : ℤ)
refine : 0 < k * (↑p : ℤ)
⊢ 0 < k

Tactic:
refine pos_of_mul_pos_left ?_ (Nat.cast_nonneg p)

Premises used: pos_of_mul_pos_left, Nat.cast_nonneg
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℤ
hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 = k * (↑p : ℤ)
rw : 0 < HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1
⊢ 0 < k * (↑p : ℤ)

Tactic:
rw [← hk]
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℤ
hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 = k * (↑p : ℤ)
⊢ 0 < HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℤ
hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 = k * (↑p : ℤ)
⊢ 0 < k

Tactic:
have hk₀ : 0 < k := by
    refine pos_of_mul_pos_left ?_ (Nat.cast_nonneg p)
    rw [← hk]
    positivity
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℤ
hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 = k * (↑p : ℤ)
hk₀ : 0 < k
⊢ 0 ≤ k

Tactic:
hk₀.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℤ
hk : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 = k * (↑p : ℤ)
hk₀ : 0 < k
inr :
  ∀ (k : ℕ)
    (hk :
      HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 =
        HMul.hMul (α := ℤ) (↑k : ℤ) (↑p : ℤ))
    (hk₀ : LT.lt (α := ℤ) 0 (↑k : ℤ)),
    ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p

Tactic:
lift k to ℕ using hk₀.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℕ
hk :
  HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 =
    HMul.hMul (α := ℤ) (↑k : ℤ) (↑p : ℤ)
hk₀ : LT.lt (α := ℤ) 0 (↑k : ℤ)
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p

Tactic:
⟨a, b, k, Nat.cast_pos.1 hk₀, ?_, mod_cast hk⟩

Premises used: Nat.cast_mul._simp_1, Nat.cast_pos, HMul.hMul, congrArg, Nat.cast_add._simp_1, cast, Nat.cast, HPow.hPow, HAdd.hAdd, And.intro, congr, Exists.intro, Iff.mp, Nat.cast_inj._simp_1, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℕ
hk :
  HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 =
    HMul.hMul (α := ℤ) (↑k : ℤ) (↑p : ℤ)
hk₀ : LT.lt (α := ℤ) 0 (↑k : ℤ)
inr : k < p
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p

Tactic:
refine ⟨a, b, k, Nat.cast_pos.1 hk₀, ?_, mod_cast hk⟩
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℕ
hk :
  HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1 =
    HMul.hMul (α := ℤ) (↑k : ℤ) (↑p : ℤ)
hk₀ : LT.lt (α := ℤ) 0 (↑k : ℤ)
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (α := ℕ) (β := ℕ) 1 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 =
    k * p

Tactic:
replace hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p := mod_cast hk
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℕ
hk₀ : LT.lt (α := ℤ) 0 (↑k : ℤ)
hk :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (α := ℕ) (β := ℕ) 1 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 =
    k * p
⊢ k < p

Tactic:
lt_of_sum_four_squares_eq_mul hk ?_ ?_ ?_ ?_

Premises used: Int.lt_of_sum_four_squares_eq_mul
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℕ
hk₀ : LT.lt (α := ℤ) 0 (↑k : ℤ)
hk :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (α := ℕ) (β := ℕ) 1 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 =
    k * p
inr : 2 * a < p
inr₁ : 2 * b < p
inr₂ : HMul.hMul (α := ℕ) 2 1 < p
inr₃ : HMul.hMul (α := ℕ) 2 0 < p
⊢ k < p

Tactic:
refine lt_of_sum_four_squares_eq_mul hk ?_ ?_ ?_ ?_

Premises used: Int.lt_of_sum_four_squares_eq_mul
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℕ
hk₀ : LT.lt (α := ℤ) 0 (↑k : ℤ)
hk :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (α := ℕ) (β := ℕ) 1 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 =
    k * p
⊢ 2 * a < p

Tactic:
(mul_le_mul' le_rfl ha).trans_lt (Nat.mul_div_lt_iff_not_dvd.2 hodd.not_two_dvd_nat)

Premises used: Iff.mpr, le_rfl, Nat.mul_div_lt_iff_not_dvd, Odd.not_two_dvd_nat, LE.le.trans_lt, mul_le_mul'
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℕ
hk₀ : LT.lt (α := ℤ) 0 (↑k : ℤ)
hk :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (α := ℕ) (β := ℕ) 1 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 =
    k * p
⊢ 2 * a < p

Tactic:
exact (mul_le_mul' le_rfl ha).trans_lt (Nat.mul_div_lt_iff_not_dvd.2 hodd.not_two_dvd_nat)

Premises used: Iff.mpr, le_rfl, Nat.mul_div_lt_iff_not_dvd, Odd.not_two_dvd_nat, LE.le.trans_lt, mul_le_mul'
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 ≡ -1 [ZMOD (↑p : ℤ)]
k : ℕ
hk₀ : LT.lt (α := ℤ) 0 (↑k : ℤ)
hk :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (α := ℕ) (β := ℕ) 1 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 =
    k * p
⊢ 2 * b < p

Tactic:
(mul_le_mul' le_rfl hb).trans_lt (Nat.mul_div_lt_iff_not_dvd.2 hodd.not_two_dvd_nat)

Premises used: Iff.mpr, le_rfl, Nat.mul_div_lt_iff_not_dvd, Odd.not_two_dvd_nat, LE.le.trans_lt, mul_le_mul'