-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
rw :
  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))))
⊢ 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])) :
            W'.CoordinateRing))))
    (span
        (singleton (α := W'.CoordinateRing)
          ((mk W' : (a : R[X][Y]) → W'.CoordinateRing)
              (HSub.hSub (β := R[X][Y])
                (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) (-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])) :
            W'.CoordinateRing)) ⊔
      span
        (singleton (α := 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)))

Tactic:
rw [sub_sub <| -(Y : R[X][Y]), neg_sub_left (Y : R[X][Y]), map_neg, span_singleton_neg, sup_comm,
    ← span_insert, ← span_pair_add_left_mul _ _ <| mk W' <| C <| C <| W'.a₁ + ℓ, ← map_mul,
    ← map_add]

Premises used: Polynomial.C, WeierstrassCurve.Affine.CoordinateRing.mk, neg_sub_left, Ideal.span_pair_add_left_mul, map_add, map_neg, sub_sub, map_mul, sup_comm, Polynomial.X, Ideal.span_insert, WeierstrassCurve.a₁, Ideal.span_singleton_neg