-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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))
⊢ (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)
have 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
Tactic: simp only [smul, add_mul, mul_assoc, ← sq, Y_sq, map_sub, map_mul]