-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negDblY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P : Fin 3 → R),
  W'.negDblY P =
    ⋯ + ⋯ - ⋯ * P 2 - ⋯ * P 1 * P 2 + 9 * W'.a₂ * W'.a₄ * P 0 ^ 3 * P 2 - 4 * W'.a₂ * W'.a₄ * P 1 ^ 2 * P 2 ^ 2 -
                                                                                      27 * W'.a₂ * W'.a₆ * P 0 ^ 2 *
                                                                                        P 2 ^ 2 -
                                                                                    9 * W'.a₃ ^ 2 * P 0 ^ 3 * P 2 +
                                                                                  6 * W'.a₃ ^ 2 * P 1 ^ 2 * P 2 ^ 2 -
                                                                                12 * W'.a₃ * W'.a₄ * P 0 * P 1 *
                                                                                  P 2 ^ 2 +
                                                                              9 * W'.a₄ ^ 2 * P 0 ^ 2 * P 2 ^ 2 -
                                                                            2 * W'.a₁ ^ 3 * P 0 ^ 3 * P 1 +
                                                                          W'.a₁ ^ 3 * P 1 ^ 3 * P 2 +
                                                                        3 * W'.a₁ ^ 2 * W'.a₂ * P 0 ^ 4 +
                                                                      2 * W'.a₁ ^ 2 * W'.a₂ * P 0 * P 1 ^ 2 * P 2 +
                                                                    3 * W'.a₁ ^ 2 * W'.a₃ * P 0 ^ 2 * P 1 * P 2 +
                                                                  3 * W'.a₁ ^ 2 * W'.a₄ * P 0 ^ 3 * P 2 -
                                                                W'.a₁ ^ 2 * W'.a₄ * P 1 ^ 2 * P 2 ^ 2 -
                                                              12 * W'.a₁ * W'.a₂ ^ 2 * P 0 ^ 2 * P 1 * P 2 -
                                                            6 * W'.a₁ * W'.a₂ * W'.a₃ * P 0 ^ 3 * P 2 +
                                                          4 * W'.a₁ * W'.a₂ * W'.a₃ * P 1 ^ 2 * P 2 ^ 2 -
                                                        8 * W'.a₁ * W'.a₂ * W'.a₄ * P 0 * P 1 * P 2 ^ 2 +
                                                      6 * W'.a₁ * W'.a₃ ^ 2 * P 0 * P 1 * P 2 ^ 2 -
                                                    W'.a₁ * W'.a₄ ^ 2 * P 1 * P 2 ^ 3 +
                                                  8 * W'.a₂ ^ 3 * P 0 ^ 3 * P 2 -
                                                8 * W'.a₂ ^ 2 * W'.a₃ * P 0 * P 1 * P 2 ^ 2 +
                                              12 * W'.a₂ ^ 2 * W'.a₄ * P 0 ^ 2 * P 2 ^ 2 -
                                            9 * W'.a₂ * W'.a₃ ^ 2 * P 0 ^ 2 * P 2 ^ 2 -
                                          4 * W'.a₂ * W'.a₃ * W'.a₄ * P 1 * P 2 ^ 3 +
                                        6 * W'.a₂ * W'.a₄ ^ 2 * P 0 * P 2 ^ 3 +
                                      W'.a₃ ^ 3 * P 1 * P 2 ^ 3 -
                                    3 * W'.a₃ ^ 2 * W'.a₄ * P 0 * P 2 ^ 3 +
                                  W'.a₄ ^ 3 * P 2 ^ 4 +
                                W'.a₁ ^ 4 * P 0 * P 1 ^ 2 * P 2 -
                              3 * W'.a₁ ^ 3 * W'.a₂ * P 0 ^ 2 * P 1 * P 2 +
                            W'.a₁ ^ 3 * W'.a₃ * P 1 ^ 2 * P 2 ^ 2 -
                          2 * W'.a₁ ^ 3 * W'.a₄ * P 0 * P 1 * P 2 ^ 2 +
                        2 * W'.a₁ ^ 2 * W'.a₂ ^ 2 * P 0 ^ 3 * P 2 -
                      2 * W'.a₁ ^ 2 * W'.a₂ * W'.a₃ * P 0 * P 1 * P 2 ^ 2 +
                    3 * W'.a₁ ^ 2 * W'.a₂ * W'.a₄ * P 0 ^ 2 * P 2 ^ 2 -
                  2 * W'.a₁ ^ 2 * W'.a₃ * W'.a₄ * P 1 * P 2 ^ 3 +
                W'.a₁ ^ 2 * W'.a₄ ^ 2 * P 0 * P 2 ^ 3 +
              W'.a₁ * W'.a₂ * W'.a₃ ^ 2 * P 1 * P 2 ^ 3 +
            2 * W'.a₁ * W'.a₂ * W'.a₃ * W'.a₄ * P 0 * P 2 ^ 3 +
          W'.a₁ * W'.a₃ * W'.a₄ ^ 2 * P 2 ^ 4 -
        2 * W'.a₂ ^ 2 * W'.a₃ ^ 2 * P 0 * P 2 ^ 3 -
      W'.a₂ * W'.a₃ ^ 2 * W'.a₄ * P 2 ^ 4