-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma C_addPolynomial (x y ℓ : R) : C (W'.addPolynomial x y ℓ) =
    (Y - C (linePolynomial x y ℓ)) * (W'.negPolynomial - C (linePolynomial x y ℓ)) +
      W'.polynomial

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ C
      (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₆))) =
    (Y - C (C ℓ * (X - C x) + C y)) * (-Y - C (C W'.a₁ * X + C W'.a₃) - C (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₆))

Tactic:
eval_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ C
      ((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₆)) =
    (Y - C (C ℓ * (X - C x) + C y)) * (-Y - C (C W'.a₁ * X + C W'.a₃) - C (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₆))

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ C (W'.addPolynomial x y ℓ) =
    (Y - C (linePolynomial x y ℓ)) * (W'.negPolynomial - C (linePolynomial x y ℓ)) + W'.polynomial

Tactic:
rw [addPolynomial, linePolynomial, polynomial, negPolynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ C
      (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₆))) =
    (Y - C (C ℓ * (X - C x) + C y)) * (-Y - C (C W'.a₁ * X + C W'.a₃) - C (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₆))

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

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y ℓ : R
⊢ C
      ((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₆)) =
    (Y - C (C ℓ * (X - C x) + C y)) * (-Y - C (C W'.a₁ * X + C W'.a₃) - C (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₆))

Tactic:
C_simp

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