-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
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₂))
⊢ 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))))
have 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])
Tactic: congr 4