-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap.0.WeierstrassCurve.addSubMapCoeff.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R),
  W.addSubMapCoeff =
    Function.uncurry
      ![![MvPolynomial.C (-W.b₂ ^ 2 * W.b₈ + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) *
                    MvPolynomial.X 0 ^ 2 +
                  MvPolynomial.C (2 * W.b₂ * W.b₄ * W.b₈ - 2 * W.b₄ ^ 2 * W.b₆ - 10 * W.b₆ * W.b₈) * MvPolynomial.X 0 *
                    MvPolynomial.X 1 +
                MvPolynomial.C (-W.b₂ * W.b₆ * W.b₈ + W.b₄ * W.b₆ ^ 2) * MvPolynomial.X 0 * MvPolynomial.X 2 +
              MvPolynomial.C (3 * W.b₄ ^ 2 * W.b₈ - 3 * W.b₄ * W.b₆ ^ 2) * MvPolynomial.X 1 ^ 2 +
            MvPolynomial.C (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * MvPolynomial.X 1 * MvPolynomial.X 2,
          MvPolynomial.C (-W.b₂ * W.b₄ * W.b₈ + W.b₄ ^ 2 * W.b₆ + 5 * W.b₆ * W.b₈) * MvPolynomial.X 0 ^ 2 +
                  MvPolynomial.C (2 * W.b₂ * W.b₆ * W.b₈ - 2 * W.b₄ * W.b₆ ^ 2 - 10 * W.b₈ ^ 2) * MvPolynomial.X 0 *
                    MvPolynomial.X 1 +
                MvPolynomial.C (-W.b₂ * W.b₈ ^ 2 + W.b₄ * W.b₆ * W.b₈) * MvPolynomial.X 0 * MvPolynomial.X 2 +
              MvPolynomial.C (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * MvPolynomial.X 1 ^ 2 +
            MvPolynomial.C (3 * W.b₄ * W.b₈ ^ 2 - 3 * W.b₆ ^ 2 * W.b₈) * MvPolynomial.X 1 * MvPolynomial.X 2,
          MvPolynomial.C (W.b₂ * W.b₆ * W.b₈ - 8 * W.b₄ ^ 2 * W.b₈ + 7 * W.b₄ * W.b₆ ^ 2) * MvPolynomial.X 0 ^ 2 +
              MvPolynomial.C (-6 * W.b₄ * W.b₆ * W.b₈ + 6 * W.b₆ ^ 3) * MvPolynomial.X 0 * MvPolynomial.X 1 +
            MvPolynomial.C (-8 * W.b₄ * W.b₈ ^ 2 + 8 * W.b₆ ^ 2 * W.b₈) * MvPolynomial.X 0 * MvPolynomial.X 2],
        ![MvPolynomial.C (96 * W.b₆) * MvPolynomial.X 0 * MvPolynomial.X 1 +
              MvPolynomial.C (12 * W.b₂ * W.b₆ - 64 * W.b₈) * MvPolynomial.X 1 ^ 2 +
            MvPolynomial.C (16 * W.b₄ * W.b₆) * MvPolynomial.X 1 * MvPolynomial.X 2,
          MvPolynomial.C (-48 * W.b₆) * MvPolynomial.X 0 ^ 2 +
                MvPolynomial.C (32 * W.b₈) * MvPolynomial.X 0 * MvPolynomial.X 1 +
              MvPolynomial.C (-4 * W.b₂ * W.b₈ + 16 * W.b₄ * W.b₆) * MvPolynomial.X 1 ^ 2 +
            MvPolynomial.C (16 * W.b₄ * W.b₈) * MvPolynomial.X 1 * MvPolynomial.X 2,
          MvPolynomial.C (-12 * W.b₂ * W.b₆) * MvPolynomial.X 0 ^ 2 +
                  MvPolynomial.C (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * MvPolynomial.X 0 * MvPolynomial.X 1 +
                MvPolynomial.C (-12 * W.b₆ ^ 2) * MvPolynomial.X 0 * MvPolynomial.X 2 +
              MvPolynomial.C (-W.b₂ ^ 2 * W.b₈ + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) *
                MvPolynomial.X 1 ^ 2 +
            MvPolynomial.C (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * MvPolynomial.X 1 * MvPolynomial.X 2],
        ![MvPolynomial.C (-12) * MvPolynomial.X 1 ^ 2 +
              MvPolynomial.C (-4 * W.b₂) * MvPolynomial.X 1 * MvPolynomial.X 2 +
            MvPolynomial.C (W.b₂ ^ 2 - 32 * W.b₄) * MvPolynomial.X 2 ^ 2,
          MvPolynomial.C 6 * MvPolynomial.X 0 * MvPolynomial.X 1 +
                MvPolynomial.C (-W.b₂) * MvPolynomial.X 0 * MvPolynomial.X 2 +
              MvPolynomial.C (-5 * W.b₄) * MvPolynomial.X 1 * MvPolynomial.X 2 +
            MvPolynomial.C (W.b₂ * W.b₄ - 27 * W.b₆) * MvPolynomial.X 2 ^ 2,
          MvPolynomial.C (-8 * W.b₄) * MvPolynomial.X 0 * MvPolynomial.X 2 +
              MvPolynomial.C (-12 * W.b₆) * MvPolynomial.X 1 * MvPolynomial.X 2 +
            MvPolynomial.C (W.b₄ ^ 2 - 28 * W.b₈) * MvPolynomial.X 2 ^ 2]]