-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula (goal)
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
⊢ { 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 +
        (HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁) -
      ({ 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₁))) :
            Cubic F }.d +
        (HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆)) =
    0
have a : x₁ * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
          (-(x₁ * (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁)) + (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) * (2 * y₁ + W.a₃)) -
        HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 * (y₁ * (y₁ + W.a₃) - W.a₆) +
      y₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 * (y₁ + x₁ * W.a₁ + W.a₃) -
    (-(HPow.hPow (β := ℕ) x₁ 2 *
          ((x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁) *
                  (x₁ * (x₁ * 3 + 2 * W.a₂) + W.a₄ - W.a₁ * y₁ + W.a₁ * (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃))) -
                W.a₂ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
              x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 -
            x₁ * HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2)) +
      HPow.hPow (β := ℕ) (y₁ - (-y₁ - x₁ * W.a₁ - W.a₃)) 2 * (x₁ * (x₁ * (x₁ + W.a₂) + W.a₄) + W.a₆)) =
  0
Tactic: simp [field]