-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
Y_sq :
  HPow.hPow (α := W'.CoordinateRing) (β := ℕ) ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) 2 =
    (mk W' : (a : R[X][Y]) → W'.CoordinateRing)
      (HSub.hSub (α := R[X][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])
        (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))
simp :
  HMul.hMul (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) p) : W'.CoordinateRing)
        (HMul.hMul (α := W'.CoordinateRing) 1 ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)) +
      HMul.hMul (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) q) : W'.CoordinateRing)
        (HSub.hSub (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              ((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]))) :
            W'.CoordinateRing)
          (HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
            ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
                ((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]))) :
              W'.CoordinateRing)
            ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y))) =
    HMul.hMul (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) q) : W'.CoordinateRing)
        (HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              ((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]))) :
            W'.CoordinateRing)
          (1 : W'.CoordinateRing)) +
      HSub.hSub (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) p) : W'.CoordinateRing)
          (HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
            ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) q) : W'.CoordinateRing)
            ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
                ((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]))) :
              W'.CoordinateRing)) *
        (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y
⊢ (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
        HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)) *
      (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y =
    HSMul.hSMul (β := W'.CoordinateRing)
        (q *
          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]))
        1 +
      HSMul.hSMul (β := W'.CoordinateRing)
        (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]))
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)

Tactic:
simp only [smul, add_mul, mul_assoc, ← sq, Y_sq, map_sub, map_mul]

Premises used: add_mul, WeierstrassCurve.Affine.CoordinateRing.smul, map_sub, mul_assoc, sq, map_mul