awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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 * (↑p : ℤ)
have rw : 0 < HPow.hPow (α := ℤ) (β := ℕ) (↑a : ℤ) 2 + HPow.hPow (α := ℤ) (β := ℕ) (↑b : ℤ) 2 + 1
Tactic: rw [← hk]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
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 : ℤ)
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
have hk₀ : 0 < k
Tactic: have hk₀ : 0 < k := by
    refine pos_of_mul_pos_left ?_ (Nat.cast_nonneg p)
    rw [← hk]
    positivity
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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
⊢ ∃ (a : ℕ) (b : ℕ) (k : ℕ), 0 < k ∧ k < p ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + 1 = k * p
have 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
Tactic: lift k to ℕ using hk₀.le
Cleared hypotheses: k, hk, hk₀
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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
have inr : k < p
Tactic: refine ⟨a, b, k, Nat.cast_pos.1 hk₀, ?_, mod_cast hk⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
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 : ℤ)
⊢ k < p
have hk₁ : 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
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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
have inr : 2 * a < p
Tactic: refine lt_of_sum_four_squares_eq_mul hk ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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
⊢ k < p
have inr₁ : 2 * b < p
Tactic: refine lt_of_sum_four_squares_eq_mul hk ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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
⊢ k < p
have inr₂ : HMul.hMul (α := ℕ) 2 1 < p
Tactic: refine lt_of_sum_four_squares_eq_mul hk ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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
⊢ k < p
have inr₃ : HMul.hMul (α := ℕ) 2 0 < p
Tactic: refine lt_of_sum_four_squares_eq_mul hk ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
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
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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) (β := ℕ) ((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
have 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)
Tactic: rw [← @zero_mul (ZMod 2) _ m, ← show ((2 : ℤ) : ZMod 2) = 0 from rfl, ← Int.cast_mul, ← h]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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) (β := ℕ) ((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)
have 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
Tactic: simp only [Int.cast_add, Int.cast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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]
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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
⊢ ∃ (w : ℤ) (x : ℤ) (y : ℤ) (z : ℤ),
    HPow.hPow (β := ℕ) w 2 + HPow.hPow (β := ℕ) x 2 + HPow.hPow (β := ℕ) y 2 + HPow.hPow (β := ℕ) z 2 = m
have 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
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
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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
have 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
Tactic: refine ⟨(f (σ 0) - f (σ 1)) / 2, (f (σ 0) + f (σ 1)) / 2, (f (σ 2) - f (σ 3)) / 2,
    (f (σ 2) + f (σ 3)) / 2, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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
⊢ 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
have rw : 2 * x + 2 * y = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2
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]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
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
⊢ 2 * x + 2 * y = HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2
have this₁ : 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)
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
Goal:
p : ℕ
hp : Prime p
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p
have this : Fact (Prime p)
Tactic: have := Fact.mk hp
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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 : ℤ)
have 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 : ℤ)
Tactic: rw [← @Nat.cast_inj ℤ]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
Goal:
p : ℕ
hp : Prime p
this : Fact (Prime p)
a b c d : ℤ
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 : ℤ)
have 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 : ℤ)
Tactic: push_cast [sq_abs]
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (hypothesis)
Goal:
p : ℕ
hp : Prime p
this : Fact (Prime p)
⊢ ∃ (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ),
    HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 + HPow.hPow (β := ℕ) c 2 + HPow.hPow (β := ℕ) d 2 = p
have 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 : ℤ)
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
-- Lean 4 proof step from Mathlib.NumberTheory.SumFourSquares (goal)
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
have 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
Tactic: obtain ⟨a, b, k, hk₀, hkp, hk⟩ := exists_sq_add_sq_add_one_eq_mul p