-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negAddY_smul (P Q : Fin 3 → R) (u v : R) :
    W'.negAddY (u • P) (v • Q) = (u * v) ^ 2 * W'.negAddY P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -3 * (u * P x) ^ 2 * (v * Q x) * (v * Q y) + 3 * (u * P x) * (v * Q x) ^ 2 * (u * P y) -
                                    (u * P y) ^ 2 * (v * Q y) * (v * Q z) +
                                  u * P y * (v * Q y) ^ 2 * (u * P z) +
                                W'.a₁ * (u * P x) * (v * Q y) ^ 2 * (u * P z) -
                              W'.a₁ * (v * Q x) * (u * P y) ^ 2 * (v * Q z) -
                            W'.a₂ * (u * P x) ^ 2 * (v * Q y) * (v * Q z) +
                          W'.a₂ * (v * Q x) ^ 2 * (u * P y) * (u * P z) +
                        2 * W'.a₂ * (u * P x) * (v * Q x) * (u * P y) * (v * Q z) -
                      2 * W'.a₂ * (u * P x) * (v * Q x) * (v * Q y) * (u * P z) -
                    W'.a₃ * (u * P y) ^ 2 * (v * Q z) ^ 2 +
                  W'.a₃ * (v * Q y) ^ 2 * (u * P z) ^ 2 +
                W'.a₄ * (u * P x) * (u * P y) * (v * Q z) ^ 2 -
              2 * W'.a₄ * (u * P x) * (v * Q y) * (u * P z) * (v * Q z) +
            2 * W'.a₄ * (v * Q x) * (u * P y) * (u * P z) * (v * Q z) -
          W'.a₄ * (v * Q x) * (v * Q y) * (u * P z) ^ 2 +
        3 * W'.a₆ * (u * P y) * (u * P z) * (v * Q z) ^ 2 -
      3 * W'.a₆ * (v * Q y) * (u * P z) ^ 2 * (v * Q z) =
    (u * v) ^ 2 *
      (-3 * P x ^ 2 * Q x * Q y + 3 * P x * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * P z +
                                  W'.a₁ * P x * Q y ^ 2 * P z -
                                W'.a₁ * Q x * P y ^ 2 * Q z -
                              W'.a₂ * P x ^ 2 * Q y * Q z +
                            W'.a₂ * Q x ^ 2 * P y * P z +
                          2 * W'.a₂ * P x * Q x * P y * Q z -
                        2 * W'.a₂ * P x * Q x * Q y * P z -
                      W'.a₃ * P y ^ 2 * Q z ^ 2 +
                    W'.a₃ * Q y ^ 2 * P z ^ 2 +
                  W'.a₄ * P x * P y * Q z ^ 2 -
                2 * W'.a₄ * P x * Q y * P z * Q z +
              2 * W'.a₄ * Q x * P y * P z * Q z -
            W'.a₄ * Q x * Q y * P z ^ 2 +
          3 * W'.a₆ * P y * P z * Q z ^ 2 -
        3 * W'.a₆ * Q y * P z ^ 2 * Q z)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ W'.negAddY (u • P) (v • Q) = (u * v) ^ 2 * W'.negAddY P Q

Tactic:
simp only [negAddY, smul_fin3_ext]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -3 * (u * P x) ^ 2 * (v * Q x) * (v * Q y) + 3 * (u * P x) * (v * Q x) ^ 2 * (u * P y) -
                                    (u * P y) ^ 2 * (v * Q y) * (v * Q z) +
                                  u * P y * (v * Q y) ^ 2 * (u * P z) +
                                W'.a₁ * (u * P x) * (v * Q y) ^ 2 * (u * P z) -
                              W'.a₁ * (v * Q x) * (u * P y) ^ 2 * (v * Q z) -
                            W'.a₂ * (u * P x) ^ 2 * (v * Q y) * (v * Q z) +
                          W'.a₂ * (v * Q x) ^ 2 * (u * P y) * (u * P z) +
                        2 * W'.a₂ * (u * P x) * (v * Q x) * (u * P y) * (v * Q z) -
                      2 * W'.a₂ * (u * P x) * (v * Q x) * (v * Q y) * (u * P z) -
                    W'.a₃ * (u * P y) ^ 2 * (v * Q z) ^ 2 +
                  W'.a₃ * (v * Q y) ^ 2 * (u * P z) ^ 2 +
                W'.a₄ * (u * P x) * (u * P y) * (v * Q z) ^ 2 -
              2 * W'.a₄ * (u * P x) * (v * Q y) * (u * P z) * (v * Q z) +
            2 * W'.a₄ * (v * Q x) * (u * P y) * (u * P z) * (v * Q z) -
          W'.a₄ * (v * Q x) * (v * Q y) * (u * P z) ^ 2 +
        3 * W'.a₆ * (u * P y) * (u * P z) * (v * Q z) ^ 2 -
      3 * W'.a₆ * (v * Q y) * (u * P z) ^ 2 * (v * Q z) =
    (u * v) ^ 2 *
      (-3 * P x ^ 2 * Q x * Q y + 3 * P x * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * P z +
                                  W'.a₁ * P x * Q y ^ 2 * P z -
                                W'.a₁ * Q x * P y ^ 2 * Q z -
                              W'.a₂ * P x ^ 2 * Q y * Q z +
                            W'.a₂ * Q x ^ 2 * P y * P z +
                          2 * W'.a₂ * P x * Q x * P y * Q z -
                        2 * W'.a₂ * P x * Q x * Q y * P z -
                      W'.a₃ * P y ^ 2 * Q z ^ 2 +
                    W'.a₃ * Q y ^ 2 * P z ^ 2 +
                  W'.a₄ * P x * P y * Q z ^ 2 -
                2 * W'.a₄ * P x * Q y * P z * Q z +
              2 * W'.a₄ * Q x * P y * P z * Q z -
            W'.a₄ * Q x * Q y * P z ^ 2 +
          3 * W'.a₆ * P y * P z * Q z ^ 2 -
        3 * W'.a₆ * Q y * P z ^ 2 * Q z)