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