-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.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 ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (n / (P z * Q z * d)) =
      (n * (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2
        - P x * Q z ^ 2 * d ^ 2 - Q x * P z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2)
        + P y * Q z ^ 3 * d ^ 3) / (P z * Q z) ^ 3 / d ^ 3

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

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

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

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

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (n / (P z * Q z * d)) =
    (n *
            (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
                Q x * P z ^ 2 * d ^ 2 -
              P x * Q z ^ 2 * d ^ 2) +
          P y * Q z ^ 3 * d ^ 3) /
        (P z * Q z) ^ 3 /
      d ^ 3

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

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