-- 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))
⊢ 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:
ring1