Theorem: ℤθ.norm_hMul
Proof state before:
a b c r s : ℤθ
⊢ |(r.f ^ 3 - 2 * r.g ^ 3 + 4 * r.h ^ 3 - 3 * r.f ^ 2 * r.g - 3 * r.f ^ 2 * r.h + 6 * r.f * r.g ^ 2 +
                6 * r.g ^ 2 * r.h +
              24 * r.f * r.h ^ 2 -
            12 * r.g * r.h ^ 2 -
          12 * r.f * r.g * r.h) *
        (s.f ^ 3 - 2 * s.g ^ 3 + 4 * s.h ^ 3 - 3 * s.f ^ 2 * s.g - 3 * s.f ^ 2 * s.h + 6 * s.f * s.g ^ 2 +
                6 * s.g ^ 2 * s.h +
              24 * s.f * s.h ^ 2 -
            12 * s.g * s.h ^ 2 -
          12 * s.f * s.g * s.h)| =
    |{ f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                              g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                              h :=
                                r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.f ^
                          3 -
                        2 *
                          { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                                g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                                h :=
                                  r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h -
                                    3 * r.h * s.g }.g ^
                            3 +
                      4 *
                        { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                              g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                              h :=
                                r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.h ^
                          3 -
                    3 *
                        { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                              g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                              h :=
                                r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.f ^
                          2 *
                      { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                          g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                          h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.g -
                  3 *
                      { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                            g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                            h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.f ^
                        2 *
                    { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                        g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                        h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.h +
                6 *
                    { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                        g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                        h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.f *
                  { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                        g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                        h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.g ^
                    2 +
              6 *
                  { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                        g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                        h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.g ^
                    2 *
                { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                    g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                    h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.h +
            24 *
                { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                    g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                    h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.f *
              { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                    g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                    h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.h ^
                2 -
          12 *
              { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                  g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                  h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.g *
            { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                  g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                  h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.h ^
              2 -
        12 *
              { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                  g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                  h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.f *
            { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
                g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
                h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.g *
          { f := r.f * s.f + 6 * r.h * s.h - 2 * r.g * s.h - 2 * r.h * s.g,
              g := r.f * s.g + r.g * s.f + 16 * r.h * s.h - 6 * r.g * s.h - 6 * r.h * s.g,
              h := r.f * s.h + r.h * s.f + r.g * s.g + 3 * r.h * s.h - 3 * r.g * s.h - 3 * r.h * s.g }.h|
Tactic:
ring_nf
Proof state after:
no goals