-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ h₂ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ - (-y₁ - x₁ * W.a₁ - W.a₃) ≠ 0
pos :
  { a := 1,
        b :=
          -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
                  2 -
              W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            W.a₂,
        c :=
          2 * x₁ *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) 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 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            (-W.a₁ * y₁ + W.a₄),
        d :=
          -HPow.hPow (β := ℕ) x₁ 2 *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
              (2 * x₁ * y₁ + W.a₃ * x₁) *
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
            (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
        Cubic F }.a =
    { a := 1,
        b :=
          -(x₁ + x₁ +
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) 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 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
        d :=
          -(x₁ * x₁ *
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }.a
pos₁ :
  { a := 1,
        b :=
          -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
                  2 -
              W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            W.a₂,
        c :=
          2 * x₁ *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) 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 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            (-W.a₁ * y₁ + W.a₄),
        d :=
          -HPow.hPow (β := ℕ) x₁ 2 *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
              (2 * x₁ * y₁ + W.a₃ * x₁) *
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
            (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
        Cubic F }.b =
    { a := 1,
        b :=
          -(x₁ + x₁ +
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) 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 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
        d :=
          -(x₁ * x₁ *
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }.b
pos₂ :
  { a := 1,
        b :=
          -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
                  2 -
              W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            W.a₂,
        c :=
          2 * x₁ *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) 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 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            (-W.a₁ * y₁ + W.a₄),
        d :=
          -HPow.hPow (β := ℕ) x₁ 2 *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
              (2 * x₁ * y₁ + W.a₃ * x₁) *
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
            (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
        Cubic F }.c =
    { a := 1,
        b :=
          -(x₁ + x₁ +
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) 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 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
        d :=
          -(x₁ * x₁ *
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }.c
pos₃ :
  { a := 1,
        b :=
          -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
                  2 -
              W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            W.a₂,
        c :=
          2 * x₁ *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) 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 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            (-W.a₁ * y₁ + W.a₄),
        d :=
          -HPow.hPow (β := ℕ) x₁ 2 *
                HPow.hPow (β := ℕ)
                  ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
              (2 * x₁ * y₁ + W.a₃ * x₁) *
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
            (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
        Cubic F }.d =
    { a := 1,
        b :=
          -(x₁ + x₁ +
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) 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 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
            x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
        d :=
          -(x₁ * x₁ *
              W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }.d
⊢ { a := 1,
      b :=
        -HPow.hPow (β := ℕ) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 -
            W.a₁ * ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
          W.a₂,
      c :=
        2 * x₁ *
              HPow.hPow (β := ℕ)
                ((3 * HPow.hPow (β := ℕ) 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 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -HPow.hPow (β := ℕ) x₁ 2 *
              HPow.hPow (β := ℕ)
                ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) 2 +
            (2 * x₁ * y₁ + W.a₃ * x₁) *
              ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) -
          (HPow.hPow (β := ℕ) y₁ 2 + W.a₃ * y₁ - W.a₆) :
      Cubic F } =
    { a := 1,
      b :=
        -(x₁ + x₁ +
            W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) 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 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)) +
          x₁ * W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)),
      d :=
        -(x₁ * x₁ *
            W.addX x₁ x₁ ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))) }

Tactic:
ext