-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma addPolynomial_eq (x y ℓ : R) : W'.addPolynomial x y ℓ = -Cubic.toPoly
    ⟨1, -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
      2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
      -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆)⟩

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ W'.addPolynomial x y ℓ =
    -{ a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
          c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
          d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.toPoly

Tactic:
rw [addPolynomial, linePolynomial, polynomial, Cubic.toPoly]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ eval (C ℓ * (X - C x) + C y)
      (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) =
    -(C
                { a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
                    c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
                    d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.a *
              X ^ 3 +
            C
                { a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
                    c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
                    d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.b *
              X ^ 2 +
          C
              { a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
                  c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
                  d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.c *
            X +
        C
          { a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
              c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
              d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.d)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ eval (C ℓ * (X - C x) + C y)
      (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) =
    -(C
                { a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
                    c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
                    d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.a *
              X ^ 3 +
            C
                { a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
                    c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
                    d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.b *
              X ^ 2 +
          C
              { a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
                  c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
                  d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.c *
            X +
        C
          { a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂,
              c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄),
              d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.d)

Tactic:
eval_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ (C ℓ * (X - C x) + C y) ^ 2 + (C W'.a₁ * X + C W'.a₃) * (C ℓ * (X - C x) + C y) -
      (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) =
    -(C 1 * X ^ 3 + C (-ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂) * X ^ 2 +
          C (2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄)) * X +
        C (-x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆)))

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ (C ℓ * (X - C x) + C y) ^ 2 + (C W'.a₁ * X + C W'.a₃) * (C ℓ * (X - C x) + C y) -
      (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) =
    -(1 * X ^ 3 + (-C ℓ ^ 2 - C W'.a₁ * C ℓ + C W'.a₂) * X ^ 2 +
          (2 * C x * C ℓ ^ 2 + (C W'.a₁ * C x - 2 * C y - C W'.a₃) * C ℓ + (-C W'.a₁ * C y + C W'.a₄)) * X +
        (-C x ^ 2 * C ℓ ^ 2 + (2 * C x * C y + C W'.a₃ * C x) * C ℓ - (C y ^ 2 + C W'.a₃ * C y - C W'.a₆)))

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ (C ℓ * (X - C x) + C y) ^ 2 + (C W'.a₁ * X + C W'.a₃) * (C ℓ * (X - C x) + C y) -
      (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) =
    -(C 1 * X ^ 3 + C (-ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂) * X ^ 2 +
          C (2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄)) * X +
        C (-x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆)))

Tactic:
C_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ (C ℓ * (X - C x) + C y) ^ 2 + (C W'.a₁ * X + C W'.a₃) * (C ℓ * (X - C x) + C y) -
      (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) =
    -(1 * X ^ 3 + (-C ℓ ^ 2 - C W'.a₁ * C ℓ + C W'.a₂) * X ^ 2 +
          (2 * C x * C ℓ ^ 2 + (C W'.a₁ * C x - 2 * C y - C W'.a₃) * C ℓ + (-C W'.a₁ * C y + C W'.a₄)) * X +
        (-C x ^ 2 * C ℓ ^ 2 + (2 * C x * C y + C W'.a₃ * C x) * C ℓ - (C y ^ 2 + C W'.a₃ * C y - C W'.a₆)))