dsimp
a b c : ℤθ
elem : 6 = 3 + 3
⊢ {
      f :=
        { f := -23, g := -63, h := -15 }.f * { f := -23, g := -63, h := -15 }.f +
              6 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.h -
            2 * { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.h -
          2 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.g,
      g :=
        { f := -23, g := -63, h := -15 }.f * { f := -23, g := -63, h := -15 }.g +
                { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.f +
              16 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.h -
            6 * { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.h -
          6 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.g,
      h :=
        { f := -23, g := -63, h := -15 }.f * { f := -23, g := -63, h := -15 }.h +
                  { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.f +
                { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.g +
              3 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.h -
            3 * { f := -23, g := -63, h := -15 }.g * { f := -23, g := -63, h := -15 }.h -
          3 * { f := -23, g := -63, h := -15 }.h * { f := -23, g := -63, h := -15 }.g } =
    { f := -1901, g := -4842, h := -336 }
a b c : ℤθ
elem : 6 = 3 + 3
⊢ { f := -23 * -23 + 6 * -15 * -15 - 2 * -63 * -15 - 2 * -15 * -63,
      g := -23 * -63 + -63 * -23 + 16 * -15 * -15 - 6 * -63 * -15 - 6 * -15 * -63,
      h := -23 * -15 + -15 * -23 + -63 * -63 + 3 * -15 * -15 - 3 * -63 * -15 - 3 * -15 * -63 } =
    { f := -1901, g := -4842, h := -336 }