-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ W'.negAddY (u • P) (v • Q) = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.negAddY P Q
have 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)
Tactic: simp only [negAddY, smul_fin3_ext]