awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
m a b c d : ℤ
h : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    HPow.hPow (β := ℕ) (f 0) 2 + HPow.hPow (β := ℕ) (f 1) 2 + HPow.hPow (β := ℕ) (f 2) 2 + HPow.hPow (β := ℕ) (f 3) 2 =
        0 →
      ∃ (i : Fin 4),
        HPow.hPow (β := ℕ) (f i) 2 + HPow.hPow (β := ℕ) (f ((swap i 0 : (a : Fin 4) → Fin 4) 1)) 2 = 0 ∧
          HPow.hPow (β := ℕ) (f ((swap i 0 : (a : Fin 4) → Fin 4) 2)) 2 +
              HPow.hPow (β := ℕ) (f ((swap i 0 : (a : Fin 4) → Fin 4) 3)) 2 =
            0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ :
  HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f i) : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((σ : (a : Fin 4) → Fin 4) 1)) : ZMod 2) 2 =
      0 ∧
    HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((σ : (a : Fin 4) → Fin 4) 2)) : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((σ : (a : Fin 4) → Fin 4) 3)) : ZMod 2) 2 =
      0
x : ℤ
hx :
  HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 0)) 2 + HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 1)) 2 =
    2 * x
y : ℤ
hy :
  HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 2)) 2 + HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 3)) 2 =
    2 * y
rw : 2 * x + 2 * y = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2
⊢ HPow.hPow (β := ℕ) ((f ((σ : (a : Fin 4) → Fin 4) 0) - f ((σ : (a : Fin 4) → Fin 4) 1)) / 2) 2 +
          HPow.hPow (β := ℕ) ((f ((σ : (a : Fin 4) → Fin 4) 0) + f ((σ : (a : Fin 4) → Fin 4) 1)) / 2) 2 +
        HPow.hPow (β := ℕ) ((f ((σ : (a : Fin 4) → Fin 4) 2) - f ((σ : (a : Fin 4) → Fin 4) 3)) / 2) 2 +
      HPow.hPow (β := ℕ) ((f ((σ : (a : Fin 4) → Fin 4) 2) + f ((σ : (a : Fin 4) → Fin 4) 3)) / 2) 2 =
    m

Tactic:
rw [← Int.sq_add_sq_of_two_mul_sq_add_sq hx.symm, add_assoc,
    ← Int.sq_add_sq_of_two_mul_sq_add_sq hy.symm, ← mul_right_inj' two_ne_zero, ← h, mul_add]

Premises used: add_assoc, Int.sq_add_sq_of_two_mul_sq_add_sq, two_ne_zero, mul_add, mul_right_inj', Eq.symm
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
m a b c d : ℤ
h : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    HPow.hPow (β := ℕ) (f 0) 2 + HPow.hPow (β := ℕ) (f 1) 2 + HPow.hPow (β := ℕ) (f 2) 2 + HPow.hPow (β := ℕ) (f 3) 2 =
        0 →
      ∃ (i : Fin 4),
        HPow.hPow (β := ℕ) (f i) 2 + HPow.hPow (β := ℕ) (f ((swap i 0 : (a : Fin 4) → Fin 4) 1)) 2 = 0 ∧
          HPow.hPow (β := ℕ) (f ((swap i 0 : (a : Fin 4) → Fin 4) 2)) 2 +
              HPow.hPow (β := ℕ) (f ((swap i 0 : (a : Fin 4) → Fin 4) 3)) 2 =
            0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ :
  HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f i) : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((σ : (a : Fin 4) → Fin 4) 1)) : ZMod 2) 2 =
      0 ∧
    HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((σ : (a : Fin 4) → Fin 4) 2)) : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((σ : (a : Fin 4) → Fin 4) 3)) : ZMod 2) 2 =
      0
x : ℤ
hx :
  HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 0)) 2 + HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 1)) 2 =
    2 * x
y : ℤ
hy :
  HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 2)) 2 + HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 3)) 2 =
    2 * y
⊢ Eq (α := ℤ) (∑ x : Fin 4, HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) x)) 2)
    (∑ x : Fin 4, HPow.hPow (β := ℕ) (f x) 2)

Tactic:
have : (∑ x, f (σ x) ^ 2) = ∑ x, f x ^ 2 := Equiv.sum_comp σ (f · ^ 2)
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
m a b c d : ℤ
h : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 2 * m
this_1 :
  ∀ (f : Fin 4 → ZMod 2),
    HPow.hPow (β := ℕ) (f 0) 2 + HPow.hPow (β := ℕ) (f 1) 2 + HPow.hPow (β := ℕ) (f 2) 2 + HPow.hPow (β := ℕ) (f 3) 2 =
        0 →
      ∃ (i : Fin 4),
        HPow.hPow (β := ℕ) (f i) 2 + HPow.hPow (β := ℕ) (f ((swap i 0 : (a : Fin 4) → Fin 4) 1)) 2 = 0 ∧
          HPow.hPow (β := ℕ) (f ((swap i 0 : (a : Fin 4) → Fin 4) 2)) 2 +
              HPow.hPow (β := ℕ) (f ((swap i 0 : (a : Fin 4) → Fin 4) 3)) 2 =
            0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ :
  HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f i) : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((σ : (a : Fin 4) → Fin 4) 1)) : ZMod 2) 2 =
      0 ∧
    HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((σ : (a : Fin 4) → Fin 4) 2)) : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((σ : (a : Fin 4) → Fin 4) 3)) : ZMod 2) 2 =
      0
x : ℤ
hx :
  HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 0)) 2 + HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 1)) 2 =
    2 * x
y : ℤ
hy :
  HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 2)) 2 + HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 3)) 2 =
    2 * y
this :
  Eq (α := ℤ) (∑ x : Fin 4, HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) x)) 2)
    (∑ x : Fin 4, HPow.hPow (β := ℕ) (f x) 2)
⊢ 2 * x + 2 * y = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2

Tactic:
simpa only [← hx, ← hy, Fin.sum_univ_four, add_assoc] using this

Premises used: add_assoc, Fin.sum_univ_four
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
⊢ Fact (Prime p)

Tactic:
have := Fact.mk hp
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : Fact (Prime p)
a b c d : ℤ
k : ℕ
rw :
  Eq (α := ℤ)
      (↑(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 : ℤ)
⊢ 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 : ℤ)

Tactic:
rw [← @Nat.cast_inj ℤ]

Premises used: Nat.cast_inj
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : Fact (Prime p)
a b c d : ℤ
k : ℕ
push_cast :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ) ↔
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)
⊢ Eq (α := ℤ)
      (↑(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 : ℤ)

Tactic:
push_cast [sq_abs]

Premises used: sq_abs
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : Fact (Prime p)
a b c d : ℤ
k : ℕ
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ) ↔
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = (↑k : ℤ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : Fact (Prime p)
⊢ ∀ {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 : ℤ)

Tactic:
have natAbs_iff {a b c d : ℤ} {k : ℕ} :
      a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔
        a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = k := by
    rw [← @Nat.cast_inj ℤ]; push_cast [sq_abs]; rfl
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : 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 : ℤ)
obtain :
  ∀ (a b k : ℕ) (hk₀ : 0 < k) (hkp : k < p) (hk : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p),
    ∃ 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 < 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

Tactic:
obtain ⟨a, b, k, hk₀, hkp, hk⟩ := exists_sq_add_sq_add_one_eq_mul p

Premises used: Int.exists_sq_add_sq_add_one_eq_mul
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : 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 : ℤ)
a b k : ℕ
hk₀ : 0 < k
hkp : k < p
hk : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
⊢ ∃ 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

Tactic:
⟨k, hkp, hk₀, a, b, 1, 0, ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : 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 : ℤ)
a b k : ℕ
hk₀ : 0 < k
hkp : k < p
hk : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
refine :
  HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (α := ℕ) (β := ℕ) 1 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 =
    k * p
⊢ ∃ 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

Tactic:
refine ⟨k, hkp, hk₀, a, b, 1, 0, ?_⟩
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : 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 : ℤ)
a b k : ℕ
hk₀ : 0 < k
hkp : k < p
hk : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (α := ℕ) (β := ℕ) 1 2 + HPow.hPow (α := ℕ) (β := ℕ) 0 2 =
    k * p

Tactic:
simpa
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : 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 : ℤ)
⊢ ∃ 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

Tactic:
have hm : ∃ m < p, 0 < m ∧ ∃ a b c d : ℕ, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p := by
    obtain ⟨a, b, k, hk₀, hkp, hk⟩ := exists_sq_add_sq_add_one_eq_mul p
    refine ⟨k, hkp, hk₀, a, b, 1, 0, ?_⟩
    simpa
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : 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
rcases :
  ∀ (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),
    ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p

Tactic:
rcases Nat.findX hm with ⟨m, ⟨hmp, hm₀, a, b, c, d, habcd⟩, hmin⟩

Premises used: Nat.findX
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : 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
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
inl :
  ∀
    (hmin :
      ∀ m < 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))
    (hmp : 1 < p) (hm₀ : LT.lt (α := ℕ) 0 1)
    (habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 1 * p),
    ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p
inr :
  ∀ (hm₁ : 1 < m),
    ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
      HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p

Tactic:
rcases (Nat.one_le_iff_ne_zero.2 hm₀.ne').eq_or_lt with rfl | hm₁

Premises used: Iff.mpr, LE.le.eq_or_lt, LT.lt.ne', Nat.one_le_iff_ne_zero, rfl
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : 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 : ℕ
hmin :
  ∀ m < 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)
hmp : 1 < p
hm₀ : LT.lt (α := ℕ) 0 1
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 1 * p
h : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p

Tactic:
use a, b, c, d
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : 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 : ℕ
hmin :
  ∀ m < 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)
hmp : 1 < p
hm₀ : LT.lt (α := ℕ) 0 1
habcd : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = 1 * p
⊢ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p

Tactic:
simpa using habcd
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : 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
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
inr : False
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.SumFourSquares
Goal:
p : ℕ
hp : Prime p
this : 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
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
⊢ NeZero m

Tactic:
have : NeZero m := ⟨hm₀.ne'⟩
-- 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
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
pos : ∀ (hm : 2 ∣ m), False
neg : ∀ (hm : ¬2 ∣ m), False
⊢ False

Tactic:
by_cases hm : 2 ∣ m
-- 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
pos :
  ∀ (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)), False
⊢ False

Tactic:
rcases hm with ⟨m, rfl⟩

Premises used: 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 :
  ∃ 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)
⊢ 0 < m

Tactic:
rw [mul_pos_iff_of_pos_left two_pos] at hm₀

Premises used: mul_pos_iff_of_pos_left