-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.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 = Q x * P z) :
    P z * Q z * (P y * Q z - Q y * P z) * (P y * Q z - W'.negY Q * P z) = 0

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

Tactic:
ring1

Result:
no goals

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

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

Result:
no goals

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

Tactic:
rw [negY]

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