rw [unit_l, pow_three, hMul_mule_3]
a b c : ℤθ
⊢ ↑unit ^ 3 = { f := -23, g := -63, h := -15 }
a b c : ℤθ
⊢ {
      f :=
        { f := -1, g := -3, h := -1 }.f * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).f +
              6 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
            2 * { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
          2 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g,
      g :=
        { f := -1, g := -3, h := -1 }.f * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g +
                { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).f +
              16 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
            6 * { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
          6 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g,
      h :=
        { f := -1, g := -3, h := -1 }.f * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h +
                  { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).f +
                { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g +
              3 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
            3 * { f := -1, g := -3, h := -1 }.g * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).h -
          3 * { f := -1, g := -3, h := -1 }.h * ({ f := -1, g := -3, h := -1 } * { f := -1, g := -3, h := -1 }).g } =
    { f := -23, g := -63, h := -15 }