-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
⊢ (pderiv z : (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) R)
      (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Y 2 +
            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 *
              Z +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₃ : MvPolynomial (Fin 3) R) Y *
            HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 3 -
        (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 3 +
              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) *
                HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 +
            HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
                ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₄ : MvPolynomial (Fin 3) R) X *
              HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 4 +
          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 6))) =
    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 +
        HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) (3 * W'.a₃) : MvPolynomial (Fin 3) R) Y *
          HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 -
      (HMul.hMul (α := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) (2 * W'.a₂) : MvPolynomial (Fin 3) R)
              (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2) *
            Z +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) (4 * W'.a₄) : MvPolynomial (Fin 3) R) X *
            HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 3 +
        HMul.hMul (α := MvPolynomial (Fin 3) R)
          ((C : (a : R) → MvPolynomial (Fin 3) R) (6 * W'.a₆) : MvPolynomial (Fin 3) R)
          (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 5))
have pderiv_simp : (↑2 : MvPolynomial (Fin 3) R) * HPow.hPow (α := MvPolynomial (Fin 3) R) Y (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)) *
                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 *
                0) *
            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 *
            1) +
      ((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) (0 : 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) * 1)) -
    ((↑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) *
                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)) *
            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) * 1)) +
      (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) * 1))) =
  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 +
      HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R) (3 : MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₃ : MvPolynomial (Fin 3) R) *
          Y *
        HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 -
    (HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R) (2 : 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 *
          Z +
        HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R) (4 : MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₄ : MvPolynomial (Fin 3) R) *
            X *
          HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 3 +
      HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R) (6 : MvPolynomial (Fin 3) R)
          ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₆ : MvPolynomial (Fin 3) R) *
        HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 5)
Tactic: pderiv_simp