-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ HAdd.hAdd (β := F[X][Y])
        (HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) *
            HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
              ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (-y - W.a₁ * x - W.a₃)) : F[X][Y]) -
          HMul.hMul (α := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) : F[X][Y])
            (HSub.hSub (α := F[X][Y])
              ((C : (a : F[X]) → F[X][Y])
                  (HAdd.hAdd (β := F[X])
                    (HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                      HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (x + W.a₂) : F[X]) X)
                    ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 2 + W.a₂ * x + W.a₄) : F[X])) :
                F[X][Y])
              (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y]) Y)))
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) y 2 + W.a₁ * x * y + W.a₃ * y)) :
          F[X][Y]) -
      HAdd.hAdd (β := F[X][Y])
        (HSub.hSub (β := F[X][Y])
            (HPow.hPow (α := F[X][Y]) (β := ℕ) Y 2 +
              HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                ((C : (a : F[X]) → F[X][Y])
                    (HAdd.hAdd (β := F[X]) (HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) W.a₁ : F[X]) X)
                      ((C : (a : F) → F[X]) W.a₃ : F[X])) :
                  F[X][Y])
                Y)
            ((C : (a : F[X]) → F[X][Y])
                (HAdd.hAdd (β := F[X])
                  (HPow.hPow (α := F[X]) (β := ℕ) X 3 +
                      HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) W.a₂ : F[X]) (HPow.hPow (α := F[X]) (β := ℕ) X 2) +
                    HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) W.a₄ : F[X]) X)
                  ((C : (a : F) → F[X]) W.a₆ : F[X])) :
              F[X][Y]) *
          1)
        ((C : (a : F[X]) → F[X][Y])
            ((C : (a : F) → F[X]) (HPow.hPow (β := ℕ) x 3 + W.a₂ * HPow.hPow (β := ℕ) x 2 + W.a₄ * x + W.a₆)) :
          F[X][Y]) =
    0
have a : HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) *
          (Y -
            HSub.hSub (β := F[X][Y])
              (HSub.hSub (α := F[X][Y]) (-(C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y])
                (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                  ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
                  ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y])))
              ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₃) : F[X][Y])) -
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]) *
          (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]) 2 +
                HMul.hMul (β := F[X][Y])
                  (HAdd.hAdd (α := F[X][Y]) (β := F[X][Y])
                    ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y])
                    ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₂) : F[X][Y]))
                  ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]) +
              HAdd.hAdd (β := F[X][Y])
                (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]) 2 +
                  HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                    ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₂) : F[X][Y])
                    ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]))
                ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₄) : F[X][Y]) -
            HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
              Y) +
      (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) 2 +
          HMul.hMul (β := F[X][Y])
            (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
              ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]))
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y]) +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₃) : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y) : F[X][Y])) -
    ((HPow.hPow (α := F[X][Y]) (β := ℕ) Y 2 +
            HAdd.hAdd (β := F[X][Y])
                (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
                  ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₁) : F[X][Y])
                  ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]))
                ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₃) : F[X][Y]) *
              Y -
          HAdd.hAdd (β := F[X][Y])
            (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]) 3 +
                HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₂) : F[X][Y])
                  (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]) 2) +
              HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₄) : F[X][Y])
                ((C : (a : F[X]) → F[X][Y]) X : F[X][Y]))
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₆) : F[X][Y])) *
        1 +
      HAdd.hAdd (β := F[X][Y])
        (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]) 3 +
            HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₂) : F[X][Y])
              (HPow.hPow (α := F[X][Y]) (β := ℕ) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]) 2) +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₄) : F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x) : F[X][Y]))
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) W.a₆) : F[X][Y])) =
  0
Tactic: C_simp