Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
⊢ (-P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * Q z +
                                        3 * P x * P y * Q x ^ 2 * P z * Q z ^ 2 +
                                      P x ^ 3 * Q y * Q z ^ 3 -
                                    2 * P y ^ 2 * Q y * Q z ^ 3 +
                                  W'.a₁ * P x * Q y ^ 2 * P z ^ 4 +
                                W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
                              W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
                            W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                          2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
                        2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
                      W'.a₃ * Q y ^ 2 * P z ^ 6 -
                    W'.a₃ * P y ^ 2 * Q z ^ 6 -
                  W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
                W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
              W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
            W'.a₄ * P x * P y * P z * Q z ^ 6 -
          2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
        2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6) *
      (P z * Q z) ^ 3 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) *
        ((P x * Q x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * Q z + P x ^ 2 * Q x * Q z ^ 2 -
                            W'.a₁ * P x * Q y * P z ^ 2 * Q z -
                          W'.a₁ * P y * Q x * P z * Q z ^ 2 +
                        2 * W'.a₂ * P x * Q x * P z ^ 2 * Q z ^ 2 -
                      W'.a₃ * Q y * P z ^ 4 * Q z -
                    W'.a₃ * P y * P z * Q z ^ 4 +
                  W'.a₄ * Q x * P z ^ 4 * Q z ^ 2 +
                W'.a₄ * P x * P z ^ 2 * Q z ^ 4 +
              2 * W'.a₆ * P z ^ 4 * Q z ^ 4) *
            (P z * Q z) ^ 2 -
          P x * Q z ^ 2 * addZ P Q ^ 2) +
      P y * Q z ^ 3 * addZ P Q ^ 3

Tactic:
addZ

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
⊢ (-P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * Q z +
                                        3 * P x * P y * Q x ^ 2 * P z * Q z ^ 2 +
                                      P x ^ 3 * Q y * Q z ^ 3 -
                                    2 * P y ^ 2 * Q y * Q z ^ 3 +
                                  W'.a₁ * P x * Q y ^ 2 * P z ^ 4 +
                                W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
                              W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
                            W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                          2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
                        2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
                      W'.a₃ * Q y ^ 2 * P z ^ 6 -
                    W'.a₃ * P y ^ 2 * Q z ^ 6 -
                  W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
                W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
              W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
            W'.a₄ * P x * P y * P z * Q z ^ 6 -
          2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
        2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6) *
      (P z * Q z) ^ 3 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) *
        ((P x * Q x ^ 2 * P z ^ 2 - 2 * P y * Q y * P z * Q z + P x ^ 2 * Q x * Q z ^ 2 -
                            W'.a₁ * P x * Q y * P z ^ 2 * Q z -
                          W'.a₁ * P y * Q x * P z * Q z ^ 2 +
                        2 * W'.a₂ * P x * Q x * P z ^ 2 * Q z ^ 2 -
                      W'.a₃ * Q y * P z ^ 4 * Q z -
                    W'.a₃ * P y * P z * Q z ^ 4 +
                  W'.a₄ * Q x * P z ^ 4 * Q z ^ 2 +
                W'.a₄ * P x * P z ^ 2 * Q z ^ 4 +
              2 * W'.a₆ * P z ^ 4 * Q z ^ 4) *
            (P z * Q z) ^ 2 -
          P x * Q z ^ 2 * (P x * Q z ^ 2 - Q x * P z ^ 2) ^ 2) +
      P y * Q z ^ 3 * (P x * Q z ^ 2 - Q x * P z ^ 2) ^ 3