-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
simp :
  HSub.hSub (α := R[X][Y])
      ((C : (a : R[X]) → R[X][Y])
          (HPow.hPow (β := ℕ) p 2 -
              p * q *
                HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W'.a₃ : R[X]) -
            HPow.hPow (β := ℕ) q 2 *
              HAdd.hAdd (β := R[X])
                (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
                ((C : (a : R) → R[X]) W'.a₆ : R[X])) :
        R[X][Y])
      (HAdd.hAdd (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) p : R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) q : R[X][Y]) Y) *
        HAdd.hAdd (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) p : R[X][Y])
          (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) q : R[X][Y])
            (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) (-Y)
              ((C : (a : R[X]) → R[X][Y])
                  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                    ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
                R[X][Y])))) =
    HSub.hSub (β := R[X][Y])
        (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
          HMul.hMul (α := R[X][Y]) (β := R[X][Y])
            ((C : (a : R[X]) → R[X][Y])
                (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
              R[X][Y])
            Y)
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X])
              (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W'.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₄ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₆ : R[X])) :
          R[X][Y]) *
      HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) q : R[X][Y]) 2
⊢ HSub.hSub (α := R[X][Y])
      ((C : (a : R[X]) → R[X][Y])
          ((Algebra.norm R[X] : (a : W'.CoordinateRing) → R[X])
            (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
              HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y))) :
        R[X][Y])
      (HAdd.hAdd (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) p : R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) q : R[X][Y]) Y) *
        HAdd.hAdd (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) p : R[X][Y])
          (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) q : R[X][Y])
            (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) (-Y)
              ((C : (a : R[X]) → R[X][Y])
                  (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
                    ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
                R[X][Y])))) =
    W'.polynomial * HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) q : R[X][Y]) 2

Tactic:
simp only [norm_smul_basis, polynomial]

Premises used: WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis, WeierstrassCurve.Affine.polynomial