-- 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.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
⊢ { a := 1,
        b :=
          -((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₂,
        c :=
          2 * x₁ * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) ^ 2 +
              (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            (-W.a₁ * y₁ + W.a₄),
        d :=
          -x₁ ^ 2 * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) ^ 2 +
              (2 * x₁ * y₁ + W.a₃ * x₁) * ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
            (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) }.a =
    { a := 1, b := -(x₁ + x₁ + W.addX x₁ x₁ ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))),
        c :=
          x₁ * x₁ + x₁ * W.addX x₁ x₁ ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            x₁ * W.addX x₁ x₁ ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
        d := -(x₁ * x₁ * W.addX x₁ x₁ ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }.a

Tactic:
rfl

Result:
no goals

Proof state:
case neg
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:
rw [equation_iff] at h₁ h₂

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

Tactic:
field_simp [hx]

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

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

Tactic:
ring1

Result:
no goals