-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))
e_s :
  HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
        ((C : (a : F[X]) → F[X][Y])
            ((C : (a : F) → F[X])
              (eval x₂
                (HAdd.hAdd (β := F[X])
                  (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
                    (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
                  ((C : (a : F) → F[X]) y₁ : F[X])))) :
          F[X][Y]) +
      HMul.hMul (α := F[X][Y]) (β := F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) : F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (-W.slope x₁ x₂ y₁ y₂)) : F[X][Y]) =
    HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
      ((C : (a : F[X]) → F[X][Y])
          (HAdd.hAdd (β := F[X])
            (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
              (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
            ((C : (a : F) → F[X]) y₁ : F[X])) :
        F[X][Y])
⊢ Eq (α := Ideal W.CoordinateRing)
    (span
      (insert (α := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing)
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]))) :
          W.CoordinateRing)
        (singleton (α := W.CoordinateRing)
          ((mk W : (a : F[X][Y]) → W.CoordinateRing)
              (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
                  ((C : (a : F[X]) → F[X][Y])
                      ((C : (a : F) → F[X])
                        (eval x₂
                          (HAdd.hAdd (β := F[X])
                            (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
                              (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
                            ((C : (a : F) → F[X]) y₁ : F[X])))) :
                    F[X][Y]) +
                HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                  ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
                    F[X][Y])
                  ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (-W.slope x₁ x₂ y₁ y₂)) : F[X][Y])) :
            W.CoordinateRing))))
    (span
      (insert (α := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing)
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]))) :
          W.CoordinateRing)
        (singleton (α := W.CoordinateRing)
          ((mk W : (a : F[X][Y]) → W.CoordinateRing)
              (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
                ((C : (a : F[X]) → F[X][Y])
                    (HAdd.hAdd (β := F[X])
                      (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (W.slope x₁ x₂ y₁ y₂) : F[X])
                        (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])))
                      ((C : (a : F) → F[X]) y₁ : F[X])) :
                  F[X][Y])) :
            W.CoordinateRing))))

Tactic:
congr 4