Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case «0»
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
x : Fin 3 → R
⊢ ((-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * x 0 ^ 2 +
                  (2 * W.b₂ * W.b₄ * W.b₈ - 2 * W.b₄ ^ 2 * W.b₆ - 10 * W.b₆ * W.b₈) * x 0 * x 1 +
                (-(W.b₂ * W.b₆ * W.b₈) + W.b₄ * W.b₆ ^ 2) * x 0 * x 2 +
              (3 * W.b₄ ^ 2 * W.b₈ - 3 * W.b₄ * W.b₆ ^ 2) * x 1 ^ 2 +
            (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * x 1 * x 2) *
          (x 0 ^ 2 - W.b₄ * x 0 * x 2 - W.b₆ * x 1 * x 2 - W.b₈ * x 2 ^ 2) +
        ((-(W.b₂ * W.b₄ * W.b₈) + W.b₄ ^ 2 * W.b₆ + 5 * W.b₆ * W.b₈) * x 0 ^ 2 +
                  (2 * W.b₂ * W.b₆ * W.b₈ - 2 * W.b₄ * W.b₆ ^ 2 - 10 * W.b₈ ^ 2) * x 0 * x 1 +
                (-(W.b₂ * W.b₈ ^ 2) + W.b₄ * W.b₆ * W.b₈) * x 0 * x 2 +
              (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * x 1 ^ 2 +
            (3 * W.b₄ * W.b₈ ^ 2 - 3 * W.b₆ ^ 2 * W.b₈) * x 1 * x 2) *
          (2 * x 1 * x 0 + W.b₂ * x 0 * x 2 + W.b₄ * x 1 * x 2 + W.b₆ * x 2 ^ 2) +
      ((W.b₂ * W.b₆ * W.b₈ - 8 * W.b₄ ^ 2 * W.b₈ + 7 * W.b₄ * W.b₆ ^ 2) * x 0 ^ 2 +
            (-(6 * W.b₄ * W.b₆ * W.b₈) + 6 * W.b₆ ^ 3) * x 0 * x 1 +
          (-(8 * W.b₄ * W.b₈ ^ 2) + 8 * W.b₆ ^ 2 * W.b₈) * x 0 * x 2) *
        (x 1 ^ 2 - 4 * x 0 * x 2) =
    (-(W.b₂ ^ 2 * W.b₈) - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆) * x 0 ^ 4

pp: case «1»
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
x : Fin 3 → R
⊢ (96 * W.b₆ * x 0 * x 1 + (12 * W.b₂ * W.b₆ - 64 * W.b₈) * x 1 ^ 2 + 16 * W.b₄ * W.b₆ * x 1 * x 2) *
          (x 0 ^ 2 - W.b₄ * x 0 * x 2 - W.b₆ * x 1 * x 2 - W.b₈ * x 2 ^ 2) +
        (-(48 * W.b₆ * x 0 ^ 2) + 32 * W.b₈ * x 0 * x 1 + (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * x 1 ^ 2 +
            16 * W.b₄ * W.b₈ * x 1 * x 2) *
          (2 * x 1 * x 0 + W.b₂ * x 0 * x 2 + W.b₄ * x 1 * x 2 + W.b₆ * x 2 ^ 2) +
      (-(12 * W.b₂ * W.b₆ * x 0 ^ 2) + (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * x 0 * x 1 + -(12 * W.b₆ ^ 2 * x 0 * x 2) +
            (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * x 1 ^ 2 +
          (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * x 1 * x 2) *
        (x 1 ^ 2 - 4 * x 0 * x 2) =
    (-(W.b₂ ^ 2 * W.b₈) - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆) * x 1 ^ 4

pp: case «2»
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
x : Fin 3 → R
⊢ (-(12 * x 1 ^ 2) + -(4 * W.b₂ * x 1 * x 2) + (W.b₂ ^ 2 - 32 * W.b₄) * x 2 ^ 2) *
          (x 0 ^ 2 - W.b₄ * x 0 * x 2 - W.b₆ * x 1 * x 2 - W.b₈ * x 2 ^ 2) +
        (6 * x 0 * x 1 + -(W.b₂ * x 0 * x 2) + -(5 * W.b₄ * x 1 * x 2) + (W.b₂ * W.b₄ - 27 * W.b₆) * x 2 ^ 2) *
          (2 * x 1 * x 0 + W.b₂ * x 0 * x 2 + W.b₄ * x 1 * x 2 + W.b₆ * x 2 ^ 2) +
      (-(8 * W.b₄ * x 0 * x 2) + -(12 * W.b₆ * x 1 * x 2) + (W.b₄ ^ 2 - 28 * W.b₈) * x 2 ^ 2) *
        (x 1 ^ 2 - 4 * x 0 * x 2) =
    (-(W.b₂ ^ 2 * W.b₈) - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆) * x 2 ^ 4

Tactic:
<;>

Goal state after:
case «0»
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
x : Fin 3 → R
⊢ ((-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * x 0 ^ 2 +
                  (2 * W.b₂ * W.b₄ * W.b₈ - 2 * W.b₄ ^ 2 * W.b₆ - 10 * W.b₆ * W.b₈) * x 0 * x 1 +
                (-(W.b₂ * W.b₆ * W.b₈) + W.b₄ * W.b₆ ^ 2) * x 0 * x 2 +
              (3 * W.b₄ ^ 2 * W.b₈ - 3 * W.b₄ * W.b₆ ^ 2) * x 1 ^ 2 +
            (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * x 1 * x 2) *
          (x 0 ^ 2 - W.b₄ * x 0 * x 2 - W.b₆ * x 1 * x 2 - W.b₈ * x 2 ^ 2) +
        ((-(W.b₂ * W.b₄ * W.b₈) + W.b₄ ^ 2 * W.b₆ + 5 * W.b₆ * W.b₈) * x 0 ^ 2 +
                  (2 * W.b₂ * W.b₆ * W.b₈ - 2 * W.b₄ * W.b₆ ^ 2 - 10 * W.b₈ ^ 2) * x 0 * x 1 +
                (-(W.b₂ * W.b₈ ^ 2) + W.b₄ * W.b₆ * W.b₈) * x 0 * x 2 +
              (3 * W.b₄ * W.b₆ * W.b₈ - 3 * W.b₆ ^ 3) * x 1 ^ 2 +
            (3 * W.b₄ * W.b₈ ^ 2 - 3 * W.b₆ ^ 2 * W.b₈) * x 1 * x 2) *
          (2 * x 1 * x 0 + W.b₂ * x 0 * x 2 + W.b₄ * x 1 * x 2 + W.b₆ * x 2 ^ 2) +
      ((W.b₂ * W.b₆ * W.b₈ - 8 * W.b₄ ^ 2 * W.b₈ + 7 * W.b₄ * W.b₆ ^ 2) * x 0 ^ 2 +
            (-(6 * W.b₄ * W.b₆ * W.b₈) + 6 * W.b₆ ^ 3) * x 0 * x 1 +
          (-(8 * W.b₄ * W.b₈ ^ 2) + 8 * W.b₆ ^ 2 * W.b₈) * x 0 * x 2) *
        (x 1 ^ 2 - 4 * x 0 * x 2) =
    (-(W.b₂ ^ 2 * W.b₈) - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆) * x 0 ^ 4

case «1»
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
x : Fin 3 → R
⊢ (96 * W.b₆ * x 0 * x 1 + (12 * W.b₂ * W.b₆ - 64 * W.b₈) * x 1 ^ 2 + 16 * W.b₄ * W.b₆ * x 1 * x 2) *
          (x 0 ^ 2 - W.b₄ * x 0 * x 2 - W.b₆ * x 1 * x 2 - W.b₈ * x 2 ^ 2) +
        (-(48 * W.b₆ * x 0 ^ 2) + 32 * W.b₈ * x 0 * x 1 + (-(4 * W.b₂ * W.b₈) + 16 * W.b₄ * W.b₆) * x 1 ^ 2 +
            16 * W.b₄ * W.b₈ * x 1 * x 2) *
          (2 * x 1 * x 0 + W.b₂ * x 0 * x 2 + W.b₄ * x 1 * x 2 + W.b₆ * x 2 ^ 2) +
      (-(12 * W.b₂ * W.b₆ * x 0 ^ 2) + (8 * W.b₂ * W.b₈ - 32 * W.b₄ * W.b₆) * x 0 * x 1 + -(12 * W.b₆ ^ 2 * x 0 * x 2) +
            (-(W.b₂ ^ 2 * W.b₈) + 9 * W.b₂ * W.b₄ * W.b₆ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2) * x 1 ^ 2 +
          (4 * W.b₂ * W.b₄ * W.b₈ - 4 * W.b₂ * W.b₆ ^ 2) * x 1 * x 2) *
        (x 1 ^ 2 - 4 * x 0 * x 2) =
    (-(W.b₂ ^ 2 * W.b₈) - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆) * x 1 ^ 4

case «2»
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsElliptic
x : Fin 3 → R
⊢ (-(12 * x 1 ^ 2) + -(4 * W.b₂ * x 1 * x 2) + (W.b₂ ^ 2 - 32 * W.b₄) * x 2 ^ 2) *
          (x 0 ^ 2 - W.b₄ * x 0 * x 2 - W.b₆ * x 1 * x 2 - W.b₈ * x 2 ^ 2) +
        (6 * x 0 * x 1 + -(W.b₂ * x 0 * x 2) + -(5 * W.b₄ * x 1 * x 2) + (W.b₂ * W.b₄ - 27 * W.b₆) * x 2 ^ 2) *
          (2 * x 1 * x 0 + W.b₂ * x 0 * x 2 + W.b₄ * x 1 * x 2 + W.b₆ * x 2 ^ 2) +
      (-(8 * W.b₄ * x 0 * x 2) + -(12 * W.b₆ * x 1 * x 2) + (W.b₄ ^ 2 - 28 * W.b₈) * x 2 ^ 2) *
        (x 1 ^ 2 - 4 * x 0 * x 2) =
    (-(W.b₂ ^ 2 * W.b₈) - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆) * x 2 ^ 4