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

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

Tactic:
simp only [addX, smul_fin3_ext]

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