-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
/-- The formula `y(P₁)(x(P₂) - x(P₃)) + y(P₂)(x(P₃) - x(P₁)) + y(P₃)(x(P₁) - x(P₂)) = 0`,
assuming that `P₁ + P₂ + P₃ = O`. -/
lemma cyclic_sum_Y_mul_X_sub_X {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) :
    let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)
    y₁ * (x₂ - x₃) + y₂ * (x₃ - x₁) + W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) = 0

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ (y₁ *
            (x₂ * ((x₁ - x₂) ^ 2 * (x₁ - x₂)) -
              ((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ -
                  (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁ -
                (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂)) +
          y₂ *
            ((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ -
                  (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁ -
                (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂ -
              (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁)) *
        ((x₁ - x₂) * ((x₁ - x₂) ^ 2 * (x₁ - x₂))) +
      ((y₁ - y₂) *
              ((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ -
                    (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁ -
                  (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂ -
                (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁) +
            y₁ * ((x₁ - x₂) * ((x₁ - x₂) ^ 2 * (x₁ - x₂)))) *
          (x₁ - x₂) *
        ((x₁ - x₂) ^ 2 * (x₁ - x₂)) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂);
  y₁ * (x₂ - x₃) + y₂ * (x₃ - x₁) + W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) = 0

Tactic:
simp_rw [slope_of_X_ne hx, negAddY, addX]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ y₁ * (x₂ - (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)) +
        y₂ * (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
      ((y₁ - y₂) / (x₁ - x₂) * (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
          y₁) *
        (x₁ - x₂) =
    0

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ y₁ * (x₂ - (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂)) +
        y₂ * (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
      ((y₁ - y₂) / (x₁ - x₂) * (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂ - x₁) +
          y₁) *
        (x₁ - x₂) =
    0

Tactic:
field_simp [sub_ne_zero.mpr hx]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ (y₁ *
            (x₂ * ((x₁ - x₂) ^ 2 * (x₁ - x₂)) -
              ((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ -
                  (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁ -
                (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂)) +
          y₂ *
            ((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ -
                  (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁ -
                (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂ -
              (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁)) *
        ((x₁ - x₂) * ((x₁ - x₂) ^ 2 * (x₁ - x₂))) +
      ((y₁ - y₂) *
              ((y₁ - y₂) ^ 2 * (x₁ - x₂) + W.a₁ * (y₁ - y₂) * (x₁ - x₂) ^ 2 - (x₁ - x₂) ^ 2 * (x₁ - x₂) * W.a₂ -
                    (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁ -
                  (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₂ -
                (x₁ - x₂) ^ 2 * (x₁ - x₂) * x₁) +
            y₁ * ((x₁ - x₂) * ((x₁ - x₂) ^ 2 * (x₁ - x₂)))) *
          (x₁ - x₂) *
        ((x₁ - x₂) ^ 2 * (x₁ - x₂)) =
    0