-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma XYIdeal_add_eq (x₁ x₂ y₁ L : R) : XYIdeal W (W.addX x₁ x₂ L) (C <| W.addY x₁ x₂ y₁ L) =
    span {mk W <| W.negPolynomial - C (linePolynomial x₁ y₁ L)} ⊔ XIdeal W (W.addX x₁ x₂ L)

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x₁ x₂ y₁ L : R
⊢ Y - C (C (-(L * (W.addX x₁ x₂ L - x₁) + y₁) - W.a₁ * W.addX x₁ x₂ L - W.a₃)) +
      C (X - C (W.addX x₁ x₂ L)) * C (C (W.a₁ + L)) =
    C (C W.a₁ * X + C W.a₃) + C (C L * (X - C x₁) + C y₁) + Y

Tactic:
C_simp

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
x₁ x₂ y₁ L : R
⊢ Y - (-(C (C L) * (C (C (W.addX x₁ x₂ L)) - C (C x₁)) + C (C y₁)) - C (C W.a₁) * C (C (W.addX x₁ x₂ L)) - C (C W.a₃)) +
      (C X - C (C (W.addX x₁ x₂ L))) * (C (C W.a₁) + C (C L)) =
    C (C W.a₁) * C X + C (C W.a₃) + (C (C L) * (C X - C (C x₁)) + C (C y₁)) + Y

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x₁ x₂ y₁ L : R
⊢ span
      {(mk W) (C (X - C (W.addX x₁ x₂ L))),
        (mk W)
          (Y - C (C (-(L * (W.addX x₁ x₂ L - x₁) + y₁) - W.a₁ * W.addX x₁ x₂ L - W.a₃)) +
            C (X - C (W.addX x₁ x₂ L)) * C (C (W.a₁ + L)))} =
    span {(mk W) (C (X - C (W.addX x₁ x₂ L))), (mk W) (C (C W.a₁ * X + C W.a₃) + C (C L * (X - C x₁) + C y₁) + Y)}

Tactic:
apply congr_arg (_ ∘ _ ∘ _ ∘ _)

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
x₁ x₂ y₁ L : R
⊢ Y - C (C (-(L * (W.addX x₁ x₂ L - x₁) + y₁) - W.a₁ * W.addX x₁ x₂ L - W.a₃)) +
      C (X - C (W.addX x₁ x₂ L)) * C (C (W.a₁ + L)) =
    C (C W.a₁ * X + C W.a₃) + C (C L * (X - C x₁) + C y₁) + Y

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x₁ x₂ y₁ L : R
⊢ Y - (-(C (C L) * (C (C (W.addX x₁ x₂ L)) - C (C x₁)) + C (C y₁)) - C (C W.a₁) * C (C (W.addX x₁ x₂ L)) - C (C W.a₃)) +
      (C X - C (C (W.addX x₁ x₂ L))) * (C (C W.a₁) + C (C L)) =
    C (C W.a₁) * C X + C (C W.a₃) + (C (C L) * (C X - C (C x₁)) + C (C y₁)) + Y

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x₁ x₂ y₁ L : R
⊢ span
      {(mk W) (C (X - C (W.addX x₁ x₂ L))),
        (mk W) (Y - C (C (-(L * (W.addX x₁ x₂ L - x₁) + y₁) - W.a₁ * W.addX x₁ x₂ L - W.a₃)))} =
    span {(mk W) (-Y - C (C W.a₁ * X + C W.a₃) - C (C L * (X - C x₁) + C y₁))} ⊔
      span {(mk W) (C (X - C (W.addX x₁ x₂ L)))}

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_mul_right <| mk W <| C <| C <| W.a₁ + L, ← _root_.map_mul,
  ← map_add]

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
x₁ x₂ y₁ L : R
⊢ span
      {(mk W) (C (X - C (W.addX x₁ x₂ L))),
        (mk W)
          (Y - C (C (-(L * (W.addX x₁ x₂ L - x₁) + y₁) - W.a₁ * W.addX x₁ x₂ L - W.a₃)) +
            C (X - C (W.addX x₁ x₂ L)) * C (C (W.a₁ + L)))} =
    span {(mk W) (C (X - C (W.addX x₁ x₂ L))), (mk W) (C (C W.a₁ * X + C W.a₃) + C (C L * (X - C x₁) + C y₁) + Y)}

Proof state:
R : Type u
inst✝ : CommRing R
W : Affine R
x₁ x₂ y₁ L : R
⊢ XYIdeal W (W.addX x₁ x₂ L) (C (W.addY x₁ x₂ y₁ L)) =
    span {(mk W) (W.negPolynomial - C (linePolynomial x₁ y₁ L))} ⊔ XIdeal W (W.addX x₁ x₂ L)

Tactic:
simp only [XYIdeal, XIdeal, XClass, YClass, addY, negAddY, negY, negPolynomial, linePolynomial]

Result:
R : Type u
inst✝ : CommRing R
W : Affine R
x₁ x₂ y₁ L : R
⊢ span
      {(mk W) (C (X - C (W.addX x₁ x₂ L))),
        (mk W) (Y - C (C (-(L * (W.addX x₁ x₂ L - x₁) + y₁) - W.a₁ * W.addX x₁ x₂ L - W.a₃)))} =
    span {(mk W) (-Y - C (C W.a₁ * X + C W.a₃) - C (C L * (X - C x₁) + C y₁))} ⊔
      span {(mk W) (C (X - C (W.addX x₁ x₂ L)))}