-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
Y_rw :
  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]) (W.negY x y)) : 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)) =
    HMul.hMul (α := F[X][Y]) W.polynomial 1
hx : W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄) ≠ 0
W_X : F := W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄)
h₁ :
  HMul.hMul (α := F[X][Y]) 1 (-1) *
      (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) =
    (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]) -
              HAdd.hAdd (β := F[X][Y])
                (3 *
                    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])
                    (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (2 : 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])) *
            1 +
          1 *
              -HAdd.hAdd (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
                  (HAdd.hAdd (β := F[X][Y])
                    (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (2 : 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]) +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (1 : 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]) 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]) -
            HAdd.hAdd (β := F[X][Y])
              (3 * 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])
                  (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (2 : 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 *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y])
⊢ HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (HMul.hMul (α := F) 1 (-1))) : 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)) =
    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₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄))) :
              F[X][Y])
            (1 : F[X][Y]))
          ((C : (a : F[X]) → F[X][Y])
              ((C : (a : F) → F[X]) 1 *
                  -HAdd.hAdd (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (2 * x + W.a₂) : F[X]) *
                HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x : F[X])) :
            F[X][Y]) +
        HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (1 * W.a₁)) : 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])) +
      HMul.hMul (α := F[X][Y]) (β := F[X][Y])
          ((C : (a : F[X]) → F[X][Y])
              ((C : (a : F) → F[X]) (W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄))) :
            F[X][Y])
          (0 : F[X][Y]) *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) Y
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (W.negY x y)) : F[X][Y])

Tactic:
C_simp