-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma XYIdeal_neg_mul {x y : F} (h : W.Nonsingular x y) :
    XYIdeal W x (C <| W.negY x y) * XYIdeal W x (C y) = XIdeal W x

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (Y - C (C y)) * (Y - C (C (-y - W.a₁ * x - W.a₃))) -
          C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) +
        C (C (y ^ 2 + W.a₁ * x * y + W.a₃ * 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₆)) * 1 +
        C (C (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆))) =
    0

Tactic:
C_simp

Result:
case a.a
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (Y - C (C y)) * (Y - (-C (C y) - C (C W.a₁) * C (C x) - C (C W.a₃))) -
          (C X - C (C x)) *
            (C X ^ 2 + (C (C x) + C (C W.a₂)) * C X + (C (C x) ^ 2 + C (C W.a₂) * C (C x) + C (C W.a₄)) -
              C (C W.a₁) * Y) +
        (C (C y) ^ 2 + C (C W.a₁) * C (C x) * C (C y) + C (C W.a₃) * 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₆))) *
          1 +
        (C (C x) ^ 3 + C (C W.a₂) * C (C x) ^ 2 + C (C W.a₄) * C (C x) + C (C W.a₆))) =
    0

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ XYIdeal W x (C (W.negY x y)) * XYIdeal W x (C y) = XIdeal W x

Tactic:
have Y_rw : (Y - C (C y)) * (Y - C (C <| W.negY x y)) -
    C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
      W.polynomial * 1 := by
  linear_combination (norm := (rw [negY, polynomial]; C_simp; ring1))
    congr_arg C (congr_arg C ((equation_iff ..).mp h.left).symm)

Result:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
⊢ XYIdeal W x (C (W.negY x y)) * XYIdeal W x (C y) = XIdeal W x

Proof state:
case h.e'_2.h.inr
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0
W_Y : F := 2 * y + W.a₁ * x + W.a₃
⊢ 0 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    1 + 0 * C (X - C x) + C (C W_Y⁻¹) * (Y - C (C y)) + C (C (W_Y⁻¹ * -1)) * (Y - C (C (W.negY x y)))

Tactic:
rw [negY, ← mul_right_inj' <| C_ne_zero.mpr <| C_ne_zero.mpr hy]

Result:
case h.e'_2.h.inr
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0
W_Y : F := 2 * y + W.a₁ * x + W.a₃
⊢ C (C (2 * y + W.a₁ * x + W.a₃)) *
      (0 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y)) =
    C (C (2 * y + W.a₁ * x + W.a₃)) *
      (1 + 0 * C (X - C x) + C (C W_Y⁻¹) * (Y - C (C y)) + C (C (W_Y⁻¹ * -1)) * (Y - C (C (-y - W.a₁ * x - W.a₃))))

Proof state:
case h.e'_2.h
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
⊢ ∃ a a_1 a_2 a_3,
    a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
      1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))

Tactic:
rcases ((nonsingular_iff' ..).mp h).right with hx | hy

Result:
case h.e'_2.h.inl
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hx : W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0
⊢ ∃ a a_1 a_2 a_3,
    a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
      1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))

case h.e'_2.h.inr
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0
⊢ ∃ a a_1 a_2 a_3,
    a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
      1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1

Tactic:
linear_combination (norm := (rw [negY, polynomial]; C_simp; ring1))
  congr_arg C (congr_arg C ((equation_iff ..).mp h.left).symm)

Result:
no goals

Proof state:
case h.e'_2.h.inl
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hx : W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0
W_X : F := W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
⊢ C (C (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄))) *
      (C (C (W_X⁻¹ * -1)) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y)) =
    C (C (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄))) *
      (1 + C (C W_X⁻¹ * -(X + C (2 * x + W.a₂))) * C (X - C x) + C (C (W_X⁻¹ * W.a₁)) * (Y - C (C y)) +
        0 * (Y - C (C (W.negY x y))))

Tactic:
simp only [W_X, mul_add, ← mul_assoc, ← C_mul, mul_inv_cancel₀ hx]

Result:
case h.e'_2.h.inl
F : Type u
inst✝ : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  (Y - C (C y)) * (Y - C (C (W.negY x y))) -
      C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    W.polynomial * 1
hx : W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0
W_X : F := W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)
⊢ C (C (1 * -1)) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) =
    C (C (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄))) * 1 + C (C 1 * -(X + C (2 * x + W.a₂)) * (X - C x)) +
        C (C (1 * W.a₁)) * (Y - C (C y)) +
      C (C (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄))) * 0 * (Y - C (C (W.negY x y)))