-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
simp :
  -(HPow.hPow (β := ℕ) u 3 * P y) * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) v 2 * Q x) 3 *
                                            HPow.hPow (β := ℕ) (u * P z) 3 +
                                          2 * (HPow.hPow (β := ℕ) u 3 * P y) *
                                              HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) v 3 * Q y) 2 *
                                            HPow.hPow (β := ℕ) (u * P z) 3 -
                                        3 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 *
                                                (HPow.hPow (β := ℕ) v 2 * Q x) *
                                              (HPow.hPow (β := ℕ) v 3 * Q y) *
                                            HPow.hPow (β := ℕ) (u * P z) 2 *
                                          (v * Q z) +
                                      3 * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) *
                                            HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) v 2 * Q x) 2 *
                                          (u * P z) *
                                        HPow.hPow (β := ℕ) (v * Q z) 2 +
                                    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 3 *
                                        (HPow.hPow (β := ℕ) v 3 * Q y) *
                                      HPow.hPow (β := ℕ) (v * Q z) 3 -
                                  2 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y) 2 *
                                      (HPow.hPow (β := ℕ) v 3 * Q y) *
                                    HPow.hPow (β := ℕ) (v * Q z) 3 +
                                W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) *
                                    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) v 3 * Q y) 2 *
                                  HPow.hPow (β := ℕ) (u * P z) 4 +
                              W'.a₁ * (HPow.hPow (β := ℕ) u 3 * P y) * (HPow.hPow (β := ℕ) v 2 * Q x) *
                                    (HPow.hPow (β := ℕ) v 3 * Q y) *
                                  HPow.hPow (β := ℕ) (u * P z) 3 *
                                (v * Q z) -
                            W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) *
                                  (HPow.hPow (β := ℕ) v 3 * Q y) *
                                (u * P z) *
                              HPow.hPow (β := ℕ) (v * Q z) 3 -
                          W'.a₁ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y) 2 * (HPow.hPow (β := ℕ) v 2 * Q x) *
                            HPow.hPow (β := ℕ) (v * Q z) 4 -
                        2 * W'.a₂ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) v 2 * Q x) *
                              (HPow.hPow (β := ℕ) v 3 * Q y) *
                            HPow.hPow (β := ℕ) (u * P z) 4 *
                          (v * Q z) +
                      2 * W'.a₂ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) *
                            (HPow.hPow (β := ℕ) v 2 * Q x) *
                          (u * P z) *
                        HPow.hPow (β := ℕ) (v * Q z) 4 +
                    W'.a₃ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) v 3 * Q y) 2 * HPow.hPow (β := ℕ) (u * P z) 6 -
                  W'.a₃ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y) 2 * HPow.hPow (β := ℕ) (v * Q z) 6 -
                W'.a₄ * (HPow.hPow (β := ℕ) v 2 * Q x) * (HPow.hPow (β := ℕ) v 3 * Q y) *
                    HPow.hPow (β := ℕ) (u * P z) 6 *
                  (v * Q z) -
              W'.a₄ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) v 3 * Q y) * HPow.hPow (β := ℕ) (u * P z) 4 *
                HPow.hPow (β := ℕ) (v * Q z) 3 +
            W'.a₄ * (HPow.hPow (β := ℕ) u 3 * P y) * (HPow.hPow (β := ℕ) v 2 * Q x) * HPow.hPow (β := ℕ) (u * P z) 3 *
              HPow.hPow (β := ℕ) (v * Q z) 4 +
          W'.a₄ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) * (u * P z) *
            HPow.hPow (β := ℕ) (v * Q z) 6 -
        2 * W'.a₆ * (HPow.hPow (β := ℕ) v 3 * Q y) * HPow.hPow (β := ℕ) (u * P z) 6 * HPow.hPow (β := ℕ) (v * Q z) 3 +
      2 * W'.a₆ * (HPow.hPow (β := ℕ) u 3 * P y) * HPow.hPow (β := ℕ) (u * P z) 3 * HPow.hPow (β := ℕ) (v * Q z) 6 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 *
      (-P y * HPow.hPow (β := ℕ) (Q x) 3 * HPow.hPow (β := ℕ) (P z) 3 +
                                            2 * P y * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 3 -
                                          3 * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q y * HPow.hPow (β := ℕ) (P z) 2 *
                                            Q z +
                                        3 * P x * P y * HPow.hPow (β := ℕ) (Q x) 2 * P z * HPow.hPow (β := ℕ) (Q z) 2 +
                                      HPow.hPow (β := ℕ) (P x) 3 * Q y * HPow.hPow (β := ℕ) (Q z) 3 -
                                    2 * HPow.hPow (β := ℕ) (P y) 2 * Q y * HPow.hPow (β := ℕ) (Q z) 3 +
                                  W'.a₁ * P x * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 4 +
                                W'.a₁ * P y * Q x * Q y * HPow.hPow (β := ℕ) (P z) 3 * Q z -
                              W'.a₁ * P x * P y * Q y * P z * HPow.hPow (β := ℕ) (Q z) 3 -
                            W'.a₁ * HPow.hPow (β := ℕ) (P y) 2 * Q x * HPow.hPow (β := ℕ) (Q z) 4 -
                          2 * W'.a₂ * P x * Q x * Q y * HPow.hPow (β := ℕ) (P z) 4 * Q z +
                        2 * W'.a₂ * P x * P y * Q x * P z * HPow.hPow (β := ℕ) (Q z) 4 +
                      W'.a₃ * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 6 -
                    W'.a₃ * HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (Q z) 6 -
                  W'.a₄ * Q x * Q y * HPow.hPow (β := ℕ) (P z) 6 * Q z -
                W'.a₄ * P x * Q y * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 3 +
              W'.a₄ * P y * Q x * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (β := ℕ) (Q z) 4 +
            W'.a₄ * P x * P y * P z * HPow.hPow (β := ℕ) (Q z) 6 -
          2 * W'.a₆ * Q y * HPow.hPow (β := ℕ) (P z) 6 * HPow.hPow (β := ℕ) (Q z) 3 +
        2 * W'.a₆ * P y * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (β := ℕ) (Q z) 6)
⊢ W'.negAddY (u • P) (v • Q) = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.negAddY P Q

Tactic:
simp only [negAddY, smul_fin3_ext]

Premises used: WeierstrassCurve.Jacobian.negAddY, WeierstrassCurve.Jacobian.smul_fin3_ext