m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
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
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
set f : Fin 4 → ℤ := ![a, b, c, d]
case intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
hσ : ↑(f i) ^ 2 + ↑(f (↑(swap i 0) 1)) ^ 2 = 0 ∧ ↑(f (↑(swap i 0) 2)) ^ 2 + ↑(f (↑(swap i 0) 3)) ^ 2 = 0
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
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
case intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
case intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
hσ : ↑(f i) ^ 2 + ↑(f (↑(swap i 0) 1)) ^ 2 = 0 ∧ ↑(f (↑(swap i 0) 2)) ^ 2 + ↑(f (↑(swap i 0) 3)) ^ 2 = 0
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
set σ := swap i 0
case intro.intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
x : ℤ
hx : f (↑σ 0) ^ 2 + f (↑σ 1) ^ 2 = 2 * x
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
case intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
obtain ⟨x, hx⟩ : (2 : ℤ) ∣ f (σ 0) ^ 2 + f (σ 1) ^ 2 :=
  (CharP.int_cast_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
case intro.intro.intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
x : ℤ
hx : f (↑σ 0) ^ 2 + f (↑σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (↑σ 2) ^ 2 + f (↑σ 3) ^ 2 = 2 * y
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
case intro.intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
x : ℤ
hx : f (↑σ 0) ^ 2 + f (↑σ 1) ^ 2 = 2 * x
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
obtain ⟨y, hy⟩ : (2 : ℤ) ∣ f (σ 2) ^ 2 + f (σ 3) ^ 2 :=
  (CharP.int_cast_eq_zero_iff (ZMod 2) 2 _).1 <| by
    simpa only [Int.cast_pow, Int.cast_add, ZMod.pow_card] using hσ.2
case intro.intro.intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
x : ℤ
hx : f (↑σ 0) ^ 2 + f (↑σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (↑σ 2) ^ 2 + f (↑σ 3) ^ 2 = 2 * y
⊢ ((f (↑σ 0) - f (↑σ 1)) / 2) ^ 2 + ((f (↑σ 0) + f (↑σ 1)) / 2) ^ 2 + ((f (↑σ 2) - f (↑σ 3)) / 2) ^ 2 +
      ((f (↑σ 2) + f (↑σ 3)) / 2) ^ 2 =
    m
case intro.intro.intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
x : ℤ
hx : f (↑σ 0) ^ 2 + f (↑σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (↑σ 2) ^ 2 + f (↑σ 3) ^ 2 = 2 * y
⊢ ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
refine ⟨(f (σ 0) - f (σ 1)) / 2, (f (σ 0) + f (σ 1)) / 2, (f (σ 2) - f (σ 3)) / 2,
  (f (σ 2) + f (σ 3)) / 2, ?_⟩
case intro.intro.intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
x : ℤ
hx : f (↑σ 0) ^ 2 + f (↑σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (↑σ 2) ^ 2 + f (↑σ 3) ^ 2 = 2 * y
⊢ 2 * x + 2 * y = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2
case intro.intro.intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
x : ℤ
hx : f (↑σ 0) ^ 2 + f (↑σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (↑σ 2) ^ 2 + f (↑σ 3) ^ 2 = 2 * y
⊢ ((f (↑σ 0) - f (↑σ 1)) / 2) ^ 2 + ((f (↑σ 0) + f (↑σ 1)) / 2) ^ 2 + ((f (↑σ 2) - f (↑σ 3)) / 2) ^ 2 +
      ((f (↑σ 2) + f (↑σ 3)) / 2) ^ 2 =
    m
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]
no goals
case intro.intro.intro
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this✝ :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
x : ℤ
hx : f (↑σ 0) ^ 2 + f (↑σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (↑σ 2) ^ 2 + f (↑σ 3) ^ 2 = 2 * y
this : ∑ x : Fin 4, f (↑σ x) ^ 2 = ∑ x : Fin 4, f x ^ 2
⊢ 2 * x + 2 * y = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2
simpa only [← hx, ← hy, Fin.sum_univ_four, add_assoc] using this
no goals
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
⊢ ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
decide
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
⊢ (fun x => ↑(f x)) 0 ^ 2 + (fun x => ↑(f x)) 1 ^ 2 + (fun x => ↑(f x)) 2 ^ 2 + (fun x => ↑(f x)) 3 ^ 2 =
    ↑(a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2)
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
⊢ (fun x => ↑(f x)) 0 ^ 2 + (fun x => ↑(f x)) 1 ^ 2 + (fun x => ↑(f x)) 2 ^ 2 + (fun x => ↑(f x)) 3 ^ 2 = 0
rw [← @zero_mul (ZMod 2) _ m, ← show ((2 : ℤ) : ZMod 2) = 0 from rfl, ← Int.cast_mul, ← h]
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
⊢ ↑(Matrix.vecCons a ![b, c, d] 0) ^ 2 + ↑(Matrix.vecCons a ![b, c, d] 1) ^ 2 + ↑(Matrix.vecCons a ![b, c, d] 2) ^ 2 +
      ↑(Matrix.vecCons a ![b, c, d] 3) ^ 2 =
    ↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
⊢ (fun x => ↑(f x)) 0 ^ 2 + (fun x => ↑(f x)) 1 ^ 2 + (fun x => ↑(f x)) 2 ^ 2 + (fun x => ↑(f x)) 3 ^ 2 =
    ↑(a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2)
simp only [Int.cast_add, Int.cast_pow]
no goals
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
⊢ ↑(Matrix.vecCons a ![b, c, d] 0) ^ 2 + ↑(Matrix.vecCons a ![b, c, d] 1) ^ 2 + ↑(Matrix.vecCons a ![b, c, d] 2) ^ 2 +
      ↑(Matrix.vecCons a ![b, c, d] 3) ^ 2 =
    ↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2
rfl
no goals
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
⊢ ↑(f (↑σ 0) ^ 2 + f (↑σ 1) ^ 2) = 0
simpa only [Int.cast_pow, Int.cast_add, Equiv.swap_apply_right, ZMod.pow_card] using hσ.1
no goals
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f (↑(swap i 0) 1) ^ 2 = 0 ∧ f (↑(swap i 0) 2) ^ 2 + f (↑(swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (↑σ 1)) ^ 2 = 0 ∧ ↑(f (↑σ 2)) ^ 2 + ↑(f (↑σ 3)) ^ 2 = 0
x : ℤ
hx : f (↑σ 0) ^ 2 + f (↑σ 1) ^ 2 = 2 * x
⊢ ↑(f (↑σ 2) ^ 2 + f (↑σ 3) ^ 2) = 0
simpa only [Int.cast_pow, Int.cast_add, ZMod.pow_card] using hσ.2