-- 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 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₂
⊢ { 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:
have hy : y₁ ≠ W.negY x₂ y₂ := fun h => hxy ⟨hx, h⟩

Result:
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₂)) }

Proof state:
case neg.c
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₆) }.c =
    { 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₂))) }.c

Tactic:
apply mul_right_injective₀ hx

Result:
case neg.c.a
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
⊢ (fun x => (x₁ - 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₆) }.c =
    (fun x => (x₁ - x₂) * x)
      { 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₂))) }.c

Proof state:
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₁)) }

Tactic:
rw [equation_iff] at h₁ h₂

Result:
case pos
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₁ ≠ 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 pos.b
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
⊢ -((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) ^ 2 -
        W.a₁ * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
      W.a₂ =
    -(x₁ + x₁ +
        (((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) ^ 2 +
                W.a₁ * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
              W.a₂ -
            x₁ -
          x₁))

Tactic:
ring1

Result:
no goals

Proof state:
case a.a
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
⊢ (x₁ - x₂) *
          (2 * x₁ * (y₁ - y₂) ^ 2 * (x₁ - x₂) + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * (y₁ - y₂) * (x₁ - x₂) ^ 2 +
            (-(W.a₁ * y₁) + W.a₄) * ((x₁ - x₂) ^ 2 * (x₁ - x₂))) +
        (x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆ + (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁)) *
          ((x₁ - x₂) ^ 2 * (x₁ - x₂)) -
      ((x₁ - x₂) *
          (x₁ * x₂ * ((x₁ - x₂) ^ 2 * (x₁ - 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₂) +
            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₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ + (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆)) *
          ((x₁ - x₂) ^ 2 * (x₁ - x₂))) =
    0

Tactic:
ring1

Result:
no goals