-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma eval_polynomial_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) : eval P W.polynomial / P z ^ 3 =
    W.toAffine.polynomial.evalEval (P x / P z) (P y / P z)

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (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 +
        (P y ^ 2 / P z ^ 2 * 1 + W.a₁ * P x * P y / P z ^ 2 * 1 + W.a₃ * P y / P z * 1 +
              W.a₂ * P x ^ 2 / P z ^ 2 * (P z / P z) +
            W.a₄ * P x / P z * (P z ^ 2 / P z ^ 2) +
          W.a₆ * (P z ^ 3 / P z ^ 3)) -
      ((P y / P z) ^ 2 + (toAffine W).a₁ * (P x / P z) * (P y / P z) + (toAffine W).a₃ * (P y / P z) -
          ((P x / P z) ^ 3 + (toAffine W).a₂ * (P x / P z) ^ 2 + (toAffine W).a₄ * (P x / P z) + (toAffine W).a₆) +
        (P y ^ 2 / P z ^ 2 * (P z / P z) + W.a₁ * P x * P y / P z ^ 2 * (P z / P z) +
                W.a₃ * P y / P z * (P z ^ 2 / P z ^ 2) +
              W.a₂ * P x ^ 2 / P z ^ 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomial / P z ^ 3 = Polynomial.evalEval (P x / P z) (P y / P z) (toAffine W).polynomial

Tactic:
linear_combination (norm := (rw [eval_polynomial, Affine.evalEval_polynomial]; ring1))
  P y ^ 2 / P z ^ 2 * div_self hPz + W.a₁ * P x * P y / P z ^ 2 * div_self hPz
    + W.a₃ * P y / P z * div_self (pow_ne_zero 2 hPz) - W.a₂ * P x ^ 2 / P z ^ 2 * div_self hPz
    - W.a₄ * P x / P z * div_self (pow_ne_zero 2 hPz) - W.a₆ * div_self (pow_ne_zero 3 hPz)

Result:
no goals

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomial / P z ^ 3 +
        (P y ^ 2 / P z ^ 2 * 1 + W.a₁ * P x * P y / P z ^ 2 * 1 + W.a₃ * P y / P z * 1 +
              W.a₂ * P x ^ 2 / P z ^ 2 * (P z / P z) +
            W.a₄ * P x / P z * (P z ^ 2 / P z ^ 2) +
          W.a₆ * (P z ^ 3 / P z ^ 3)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) (toAffine W).polynomial +
        (P y ^ 2 / P z ^ 2 * (P z / P z) + W.a₁ * P x * P y / P z ^ 2 * (P z / P z) +
                W.a₃ * P y / P z * (P z ^ 2 / P z ^ 2) +
              W.a₂ * P x ^ 2 / P z ^ 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0

Tactic:
rw [eval_polynomial, Affine.evalEval_polynomial]

Result:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (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 +
        (P y ^ 2 / P z ^ 2 * 1 + W.a₁ * P x * P y / P z ^ 2 * 1 + W.a₃ * P y / P z * 1 +
              W.a₂ * P x ^ 2 / P z ^ 2 * (P z / P z) +
            W.a₄ * P x / P z * (P z ^ 2 / P z ^ 2) +
          W.a₆ * (P z ^ 3 / P z ^ 3)) -
      ((P y / P z) ^ 2 + (toAffine W).a₁ * (P x / P z) * (P y / P z) + (toAffine W).a₃ * (P y / P z) -
          ((P x / P z) ^ 3 + (toAffine W).a₂ * (P x / P z) ^ 2 + (toAffine W).a₄ * (P x / P z) + (toAffine W).a₆) +
        (P y ^ 2 / P z ^ 2 * (P z / P z) + W.a₁ * P x * P y / P z ^ 2 * (P z / P z) +
                W.a₃ * P y / P z * (P z ^ 2 / P z ^ 2) +
              W.a₂ * P x ^ 2 / P z ^ 2 * 1 +
            W.a₄ * P x / P z * 1 +
          W.a₆ * 1)) =
    0