-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
⊢ (↑2 : MvPolynomial (Fin 3) R) * HPow.hPow (α := MvPolynomial (Fin 3) R) Y (HSub.hSub (α := ℕ) 2 1) * 1 +
          (((HMul.hMul (α := MvPolynomial (Fin 3) R) 0 X +
                    HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                      ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R)
                      (0 : MvPolynomial (Fin 3) R)) *
                  Y +
                HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                    ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) X *
                  1) *
              Z +
            HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                  ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) X *
                Y *
              0) +
        ((HMul.hMul (α := MvPolynomial (Fin 3) R) 0 Y +
              HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₃ : MvPolynomial (Fin 3) R) (1 : MvPolynomial (Fin 3) R)) *
            HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 3 +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₃ : MvPolynomial (Fin 3) R) Y *
            ((↑3 : MvPolynomial (Fin 3) R) * HPow.hPow (α := MvPolynomial (Fin 3) R) Z (HSub.hSub (α := ℕ) 3 1) * 0)) -
      ((↑3 : MvPolynomial (Fin 3) R) * HPow.hPow (α := MvPolynomial (Fin 3) R) X (HSub.hSub (α := ℕ) 3 1) * 0 +
            ((0 * HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2 +
                  HMul.hMul (α := MvPolynomial (Fin 3) R)
                    ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₂ : MvPolynomial (Fin 3) R)
                    ((↑2 : MvPolynomial (Fin 3) R) *
                        HPow.hPow (α := MvPolynomial (Fin 3) R) X (HSub.hSub (α := ℕ) 2 1) *
                      0)) *
                HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 +
              HMul.hMul (α := MvPolynomial (Fin 3) R)
                  ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₂ : MvPolynomial (Fin 3) R)
                  (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2) *
                ((↑2 : MvPolynomial (Fin 3) R) * HPow.hPow (α := MvPolynomial (Fin 3) R) Z (HSub.hSub (α := ℕ) 2 1) *
                  0)) +
          ((HMul.hMul (α := MvPolynomial (Fin 3) R) 0 X +
                HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                  ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₄ : MvPolynomial (Fin 3) R)
                  (0 : MvPolynomial (Fin 3) R)) *
              HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 4 +
            HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₄ : MvPolynomial (Fin 3) R) X *
              ((↑4 : MvPolynomial (Fin 3) R) * HPow.hPow (α := MvPolynomial (Fin 3) R) Z (HSub.hSub (α := ℕ) 4 1) *
                0)) +
        (0 * HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 6 +
          HMul.hMul (α := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₆ : MvPolynomial (Fin 3) R)
            ((↑6 : MvPolynomial (Fin 3) R) * HPow.hPow (α := MvPolynomial (Fin 3) R) Z (HSub.hSub (α := ℕ) 6 1) * 0))) =
    HMul.hMul (α := MvPolynomial (Fin 3) R) 2 Y +
        HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) X *
          Z +
      HMul.hMul (α := MvPolynomial (Fin 3) R) ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₃ : MvPolynomial (Fin 3) R)
        (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 3)

Tactic:
ring1