a b c d x y z w : ℕ
⊢ ↑(Int.natAbs (↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w) ^ 2 + Int.natAbs (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z) ^ 2 +
          Int.natAbs (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y) ^ 2 +
        Int.natAbs (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x) ^ 2) =
    ↑((a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2))
a b c d x y z w : ℕ
⊢ Int.natAbs (↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w) ^ 2 + Int.natAbs (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z) ^ 2 +
        Int.natAbs (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y) ^ 2 +
      Int.natAbs (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x) ^ 2 =
    (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)
rw [← Int.coe_nat_inj']
a b c d x y z w : ℕ
⊢ abs (↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w) ^ 2 + abs (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z) ^ 2 +
        abs (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y) ^ 2 +
      abs (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x) ^ 2 =
    (↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2) * (↑x ^ 2 + ↑y ^ 2 + ↑z ^ 2 + ↑w ^ 2)
a b c d x y z w : ℕ
⊢ ↑(Int.natAbs (↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w) ^ 2 + Int.natAbs (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z) ^ 2 +
          Int.natAbs (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y) ^ 2 +
        Int.natAbs (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x) ^ 2) =
    ↑((a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2))
push_cast
no goals
a b c d x y z w : ℕ
⊢ abs (↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w) ^ 2 + abs (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z) ^ 2 +
        abs (↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y) ^ 2 +
      abs (↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x) ^ 2 =
    (↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2) * (↑x ^ 2 + ↑y ^ 2 + ↑z ^ 2 + ↑w ^ 2)
simp only [sq_abs, _root_.euler_four_squares]