-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
private lemma toAffine_negAddY_of_ne {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) {n d : F}
    (hd : d ≠ 0) : W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z) (n / d) =
      (n * (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2
        - P x * Q z * d ^ 2 - Q x * P z * d ^ 2 - P x * Q z * d ^ 2) + P y * Q z * d ^ 3)
        / (P z * Q z) ^ 2 / (d ^ 3 / (P z * Q z))

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ (toAffine W).negAddY (P x / P z) (Q x / Q z) (P y / P z) (n / d) =
    (n *
            (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                Q x * P z * d ^ 2 -
              P x * Q z * d ^ 2) +
          P y * Q z * d ^ 3) /
        (P z * Q z) ^ 2 /
      (d ^ 3 / (P z * Q z))

Tactic:
rw [Affine.negAddY, toAffine_addX_of_ne hPz hQz hd]

Result:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ n / d *
        ((n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                  Q x * P z * d ^ 2) *
                d /
              (P z * Q z) ^ 2 /
            (d ^ 3 / (P z * Q z)) -
          P x / P z) +
      P y / P z =
    (n *
            (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                Q x * P z * d ^ 2 -
              P x * Q z * d ^ 2) +
          P y * Q z * d ^ 3) /
        (P z * Q z) ^ 2 /
      (d ^ 3 / (P z * Q z))

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ (n *
            ((n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                      Q x * P z * d ^ 2) *
                    d *
                  (P z * Q z) *
                P z -
              (P z * Q z) ^ 2 * d ^ 3 * P x) *
          P z +
        P y * (d * ((P z * Q z) ^ 2 * d ^ 3 * P z))) *
      ((P z * Q z) ^ 2 * d ^ 3) =
    (n *
            (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                Q x * P z * d ^ 2 -
              P x * Q z * d ^ 2) +
          P y * Q z * d ^ 3) *
        (P z * Q z) *
      (d * ((P z * Q z) ^ 2 * d ^ 3 * P z) * P z)

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ n / d *
        ((n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                  Q x * P z * d ^ 2) *
                d /
              (P z * Q z) ^ 2 /
            (d ^ 3 / (P z * Q z)) -
          P x / P z) +
      P y / P z =
    (n *
            (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                Q x * P z * d ^ 2 -
              P x * Q z * d ^ 2) +
          P y * Q z * d ^ 3) /
        (P z * Q z) ^ 2 /
      (d ^ 3 / (P z * Q z))

Tactic:
field_simp [mul_ne_zero (pow_ne_zero 2 <| mul_ne_zero hPz hQz) <| pow_ne_zero 3 hd]

Result:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ (n *
            ((n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                      Q x * P z * d ^ 2) *
                    d *
                  (P z * Q z) *
                P z -
              (P z * Q z) ^ 2 * d ^ 3 * P x) *
          P z +
        P y * (d * ((P z * Q z) ^ 2 * d ^ 3 * P z))) *
      ((P z * Q z) ^ 2 * d ^ 3) =
    (n *
            (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                Q x * P z * d ^ 2 -
              P x * Q z * d ^ 2) +
          P y * Q z * d ^ 3) *
        (P z * Q z) *
      (d * ((P z * Q z) ^ 2 * d ^ 3 * P z) * P z)