-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
e_s :
  HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
        ((C : (a : R[X]) → R[X][Y])
            ((C : (a : R) → R[X]) (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) :
          R[X][Y]) +
      HMul.hMul (α := R[X][Y]) (β := R[X][Y])
        ((C : (a : R[X]) → R[X][Y])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X])) :
          R[X][Y])
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (W'.a₁ + ℓ)) : R[X][Y]) =
    HAdd.hAdd (α := 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])
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X])
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
                (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x₁ : R[X])))
              ((C : (a : R) → R[X]) y₁ : R[X])) :
          R[X][Y]) +
      Y
⊢ Eq (α := Ideal W'.CoordinateRing)
    (span
      (insert (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
            ((C : (a : R[X]) → R[X][Y])
              (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X]))) :
          W'.CoordinateRing)
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y
                  ((C : (a : R[X]) → R[X][Y])
                      ((C : (a : R) → R[X]) (-(ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁) - W'.a₁ * W'.addX x₁ x₂ ℓ - W'.a₃)) :
                    R[X][Y]) +
                HMul.hMul (α := R[X][Y]) (β := R[X][Y])
                  ((C : (a : R[X]) → R[X][Y])
                      (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X])) :
                    R[X][Y])
                  ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) (W'.a₁ + ℓ)) : R[X][Y])) :
            W'.CoordinateRing))))
    (span
      (insert (α := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
            ((C : (a : R[X]) → R[X][Y])
              (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (W'.addX x₁ x₂ ℓ) : R[X]))) :
          W'.CoordinateRing)
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              (HAdd.hAdd (α := 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])
                  ((C : (a : R[X]) → R[X][Y])
                      (HAdd.hAdd (β := R[X])
                        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
                          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x₁ : R[X])))
                        ((C : (a : R) → R[X]) y₁ : R[X])) :
                    R[X][Y]) +
                Y) :
            W'.CoordinateRing))))

Tactic:
congr 4