-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ 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))))
have 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
Tactic: congr 4