-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma Y_sub_Y_mul_Y_sub_negY {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) :
    (P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) = 0

Proof state:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) * P z ^ 3) - 0 -
      (Q z ^ 6 *
                  (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
                    (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)) -
                P z ^ 6 *
                  (Q y ^ 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 3 -
                    (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z ^ 2 + W'.a₄ * Q x * Q z ^ 4 + W'.a₆ * Q z ^ 6)) +
              P x * Q z ^ 2 * (P x * Q z ^ 2) * (P x * Q z ^ 2) +
            W'.a₂ * P z ^ 2 * Q z ^ 2 * (P x * Q z ^ 2) * (P x * Q z ^ 2) +
          (W'.a₄ * P z ^ 4 * Q z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4) * (P x * Q z ^ 2) -
        (Q z ^ 6 * 0 - P z ^ 6 * 0 + Q x * P z ^ 2 * (Q x * P z ^ 2) * (Q x * P z ^ 2) +
            W'.a₂ * P z ^ 2 * Q z ^ 2 * (Q x * P z ^ 2) * (Q x * P z ^ 2) +
          (W'.a₄ * P z ^ 4 * Q z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4) * (Q x * P z ^ 2))) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) = 0

Tactic:
linear_combination' (norm := (rw [negY]; ring1)) Q z ^ 6 * (equation_iff P).mp hP
  - P z ^ 6 * (equation_iff Q).mp hQ + hx * hx * hx + W'.a₂ * P z ^ 2 * Q z ^ 2 * hx * hx
  + (W'.a₄ * P z ^ 4 * Q z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4) * hx

Result:
no goals

Proof state:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) - 0 -
      (Q z ^ 6 *
                  (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
                    (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)) -
                P z ^ 6 *
                  (Q y ^ 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 3 -
                    (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z ^ 2 + W'.a₄ * Q x * Q z ^ 4 + W'.a₆ * Q z ^ 6)) +
              P x * Q z ^ 2 * (P x * Q z ^ 2) * (P x * Q z ^ 2) +
            W'.a₂ * P z ^ 2 * Q z ^ 2 * (P x * Q z ^ 2) * (P x * Q z ^ 2) +
          (W'.a₄ * P z ^ 4 * Q z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4) * (P x * Q z ^ 2) -
        (Q z ^ 6 * 0 - P z ^ 6 * 0 + Q x * P z ^ 2 * (Q x * P z ^ 2) * (Q x * P z ^ 2) +
            W'.a₂ * P z ^ 2 * Q z ^ 2 * (Q x * P z ^ 2) * (Q x * P z ^ 2) +
          (W'.a₄ * P z ^ 4 * Q z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4) * (Q x * P z ^ 2))) =
    0

Tactic:
rw [negY]

Result:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) * P z ^ 3) - 0 -
      (Q z ^ 6 *
                  (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
                    (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6)) -
                P z ^ 6 *
                  (Q y ^ 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 3 -
                    (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z ^ 2 + W'.a₄ * Q x * Q z ^ 4 + W'.a₆ * Q z ^ 6)) +
              P x * Q z ^ 2 * (P x * Q z ^ 2) * (P x * Q z ^ 2) +
            W'.a₂ * P z ^ 2 * Q z ^ 2 * (P x * Q z ^ 2) * (P x * Q z ^ 2) +
          (W'.a₄ * P z ^ 4 * Q z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4) * (P x * Q z ^ 2) -
        (Q z ^ 6 * 0 - P z ^ 6 * 0 + Q x * P z ^ 2 * (Q x * P z ^ 2) * (Q x * P z ^ 2) +
            W'.a₂ * P z ^ 2 * Q z ^ 2 * (Q x * P z ^ 2) * (Q x * P z ^ 2) +
          (W'.a₄ * P z ^ 4 * Q z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4) * (Q x * P z ^ 2))) =
    0