-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma addPolynomial_slope {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
    (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) =
      -((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂)))

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
⊢ { a := 1, b := -((y₁ - y₂) / (x₁ - x₂)) ^ 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
      c :=
        2 * x₁ * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) + x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)),
      d := -(x₁ * x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))) }

Tactic:
rw [← sub_eq_zero] at hx

Result:
case neg
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ - x₂ = 0
⊢ { a := 1, b := -((y₁ - y₂) / (x₁ - x₂)) ^ 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
      c :=
        2 * x₁ * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) + x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)),
      d := -(x₁ * x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))) }

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ { a := 1, b := -W.slope x₁ x₂ y₁ y₂ ^ 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c := 2 * x₁ * W.slope x₁ x₂ y₁ y₂ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ + (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * W.slope x₁ x₂ y₁ y₂ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }

Tactic:
rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩

Result:
case pos
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h₁ h₂ : W.Equation x₁ y₁
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ ≠ W.negY x₁ y₁
⊢ { a := 1, b := -W.slope x₁ x₁ y₁ y₁ ^ 2 - W.a₁ * W.slope x₁ x₁ y₁ y₁ + W.a₂,
      c := 2 * x₁ * W.slope x₁ x₁ y₁ y₁ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₁ y₁ y₁ + (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * W.slope x₁ x₁ y₁ y₁ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₁ y₁ y₁ -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₁ + W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)),
      c := x₁ * x₁ + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁) + x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁),
      d := -(x₁ * x₁ * W.addX x₁ x₁ (W.slope x₁ x₁ y₁ y₁)) }

Proof state:
case neg.b
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ - x₂ = 0
⊢ { a := 1, b := -((y₁ - y₂) / (x₁ - x₂)) ^ 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
        c :=
          2 * x₁ * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
            (-W.a₁ * y₁ + W.a₄),
        d :=
          -x₁ ^ 2 * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
            (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) }.b =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))),
        c := x₁ * x₂ + x₁ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) + x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)),
        d := -(x₁ * x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))) }.b

Tactic:
simp only [addX]

Result:
case neg.b
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ - x₂ = 0
⊢ -((y₁ - y₂) / (x₁ - x₂)) ^ 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂ =
    -(x₁ + x₂ + (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂))

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h₁ h₂ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - W.a₁ * x₁ - W.a₃) ≠ 0
⊢ -(x₁ ^ 2 * (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) ^ 2 * (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃))) +
            (2 * x₁ * y₁ + W.a₃ * x₁) * (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) *
              (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2 -
          (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2 * (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) +
        (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁) *
          ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2 * (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃))) -
      (-(x₁ * x₁ *
            ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) ^ 2 * (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) +
                    W.a₁ * (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) * (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2 -
                  (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2 * (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * W.a₂ -
                (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2 * (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * x₁ -
              (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2 * (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * x₁)) +
        (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆) *
          ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2 * (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)))) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) =
    -((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

Tactic:
rw [addPolynomial_eq, neg_inj, Cubic.prod_X_sub_C_eq, Cubic.toPoly_injective]

Result:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ { a := 1, b := -W.slope x₁ x₂ y₁ y₂ ^ 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c := 2 * x₁ * W.slope x₁ x₂ y₁ y₂ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ + (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * W.slope x₁ x₂ y₁ y₂ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }