awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (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'
-- 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
⊢ HMul.hMul (α := ℕ) 2 1 < p

Tactic:
lt_of_le_of_ne hp.1.two_le (hodd.ne_two_of_dvd_nat (dvd_refl _)).symm

Premises used: Odd.ne_two_of_dvd_nat, Ne.symm, Nat.Prime.two_le, dvd_refl, Fact.out, lt_of_le_of_ne
-- 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
⊢ HMul.hMul (α := ℕ) 2 1 < p

Tactic:
exact lt_of_le_of_ne hp.1.two_le (hodd.ne_two_of_dvd_nat (dvd_refl _)).symm

Premises used: Odd.ne_two_of_dvd_nat, Ne.symm, Nat.Prime.two_le, dvd_refl, Fact.out, lt_of_le_of_ne
-- 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
⊢ HMul.hMul (α := ℕ) 2 0 < p

Tactic:
hp.1.pos

Premises used: Nat.Prime.pos, Fact.out
-- 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
⊢ HMul.hMul (α := ℕ) 2 0 < p

Tactic:
exact hp.1.pos

Premises used: Nat.Prime.pos, Fact.out
-- 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
⊢ ∀ (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

Tactic:
decide
-- 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
⊢ ∀ (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

Tactic:
have : ∀ f : Fin 4 → ZMod 2, f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 → ∃ i : Fin 4,
      f i ^ 2 + f (swap i 0 1) ^ 2 = 0 ∧ f (swap i 0 2) ^ 2 + f (swap i 0 3) ^ 2 = 0 := by
    decide
-- 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]
rw :
  HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 0) 2 +
          HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 1) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 2) 2 +
      HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 3) 2 =
    (↑(HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) : ZMod 2)
⊢ HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 0) 2 +
          HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 1) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 2) 2 +
      HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 3) 2 =
    0

Tactic:
rw [← @zero_mul (ZMod 2) _ m, ← show ((2 : ℤ) : ZMod 2) = 0 from rfl, ← Int.cast_mul, ← h]

Premises used: Int.cast, MulZeroClass.zero_mul, Int.cast_mul, rfl
-- 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]
simp :
  HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f 0) : ZMod 2) 2 + HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f 1) : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f 2) : ZMod 2) 2 +
      HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f 3) : ZMod 2) 2 =
    HPow.hPow (α := ZMod 2) (β := ℕ) (↑a : ZMod 2) 2 + HPow.hPow (α := ZMod 2) (β := ℕ) (↑b : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑c : ZMod 2) 2 +
      HPow.hPow (α := ZMod 2) (β := ℕ) (↑d : ZMod 2) 2
⊢ HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 0) 2 +
          HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 1) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 2) 2 +
      HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (x : Fin 4) ↦ ((↑(f x) : ZMod 2) : ZMod 2)) 3) 2 =
    (↑(HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2) : ZMod 2)

Tactic:
simp only [Int.cast_add, Int.cast_pow]

Premises used: Int.cast_pow, Int.cast_add
-- 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]
⊢ HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f 0) : ZMod 2) 2 + HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f 1) : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f 2) : ZMod 2) 2 +
      HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f 3) : ZMod 2) 2 =
    HPow.hPow (α := ZMod 2) (β := ℕ) (↑a : ZMod 2) 2 + HPow.hPow (α := ZMod 2) (β := ℕ) (↑b : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑c : ZMod 2) 2 +
      HPow.hPow (α := ZMod 2) (β := ℕ) (↑d : ZMod 2) 2

Tactic:
rfl
-- 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]
obtain :
  ∀ (i : Fin 4)
    (hσ :
      HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f i) : ZMod 2) 2 +
            HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((swap i 0 : (a : Fin 4) → Fin 4) 1)) : ZMod 2) 2 =
          0 ∧
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((swap i 0 : (a : Fin 4) → Fin 4) 2)) : ZMod 2) 2 +
            HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((swap i 0 : (a : Fin 4) → Fin 4) 3)) : ZMod 2) 2 =
          0),
    ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
      HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m

Tactic:
obtain ⟨i, hσ⟩ := this (fun x => ↑(f x)) <| by
    rw [← @zero_mul (ZMod 2) _ m, ← show ((2 : ℤ) : ZMod 2) = 0 from rfl, ← Int.cast_mul, ← h]
    simp only [Int.cast_add, Int.cast_pow]
    rfl

Premises used: Int.cast
-- 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
hσ :
  HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f i) : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((swap i 0 : (a : Fin 4) → Fin 4) 1)) : ZMod 2) 2 =
      0 ∧
    HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((swap i 0 : (a : Fin 4) → Fin 4) 2)) : ZMod 2) 2 +
        HPow.hPow (α := ZMod 2) (β := ℕ) (↑(f ((swap i 0 : (a : Fin 4) → Fin 4) 3)) : ZMod 2) 2 =
      0
⊢ let σ := swap i 0;
  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

Tactic:
set σ := swap i 0

Premises used: Equiv.swap, OfNat.ofNat
-- 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
⊢ Eq (α := ZMod 2)
    (↑(HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 0)) 2 +
          HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 1)) 2) :
      ZMod 2)
    0

Tactic:
simpa only [σ, Int.cast_pow, Int.cast_add, Equiv.swap_apply_right, ZMod.pow_card] using hσ.1

Premises used: Int.cast_pow, ZMod.pow_card, Int.cast_add, And.left, Equiv.swap_apply_right
-- 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
obtain :
  ∀ (x : ℤ)
    (hx :
      HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 0)) 2 + HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 1)) 2 =
        2 * x),
    ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
      HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m

Tactic:
obtain ⟨x, hx⟩ : (2 : ℤ) ∣ f (σ 0) ^ 2 + f (σ 1) ^ 2 :=
    (CharP.intCast_eq_zero_iff (ZMod 2) 2 _).1 <| by
      simpa only [σ, Int.cast_pow, Int.cast_add, Equiv.swap_apply_right, ZMod.pow_card] using hσ.1

Premises used: ZMod, Iff.mp, OfNat.ofNat, DFunLike.coe, CharP.intCast_eq_zero_iff
-- 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
⊢ Eq (α := ZMod 2)
    (↑(HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 2)) 2 +
          HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 3)) 2) :
      ZMod 2)
    0

Tactic:
simpa only [Int.cast_pow, Int.cast_add, ZMod.pow_card] using hσ.2

Premises used: Int.cast_pow, ZMod.pow_card, Int.cast_add, And.right
-- 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
obtain :
  ∀ (y : ℤ)
    (hy :
      HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 2)) 2 + HPow.hPow (β := ℕ) (f ((σ : (a : Fin 4) → Fin 4) 3)) 2 =
        2 * y),
    ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
      HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m

Tactic:
obtain ⟨y, hy⟩ : (2 : ℤ) ∣ f (σ 2) ^ 2 + f (σ 3) ^ 2 :=
    (CharP.intCast_eq_zero_iff (ZMod 2) 2 _).1 <| by
      simpa only [Int.cast_pow, Int.cast_add, ZMod.pow_card] using hσ.2

Premises used: ZMod, Iff.mp, OfNat.ofNat, DFunLike.coe, CharP.intCast_eq_zero_iff
-- 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
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m

Tactic:
⟨(f (σ 0) - f (σ 1)) / 2, (f (σ 0) + f (σ 1)) / 2, (f (σ 2) - f (σ 3)) / 2,
    (f (σ 2) + f (σ 3)) / 2, ?_⟩

Premises used: HSub.hSub, HDiv.hDiv, HAdd.hAdd, Exists.intro, OfNat.ofNat, DFunLike.coe
-- 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
refine :
  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
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m

Tactic:
refine ⟨(f (σ 0) - f (σ 1)) / 2, (f (σ 0) + f (σ 1)) / 2, (f (σ 2) - f (σ 3)) / 2,
    (f (σ 2) + f (σ 3)) / 2, ?_⟩