-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
rw :
  W'.Equation P ∧
      (Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) (0 : R) ∨
        Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY : R) (0 : R) ∨
          Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ : R) (0 : R)) ↔
    W'.Equation P ∧
      (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) ≠
          0 ∨
        2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 ≠ 0 ∨
          HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
              (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) ≠
            0)
rw₁ :
  W'.Equation P ∧
      (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) ≠
          0 ∨
        Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY : R) (0 : R) ∨
          Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ : R) (0 : R)) ↔
    W'.Equation P ∧
      (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) ≠
          0 ∨
        2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 ≠ 0 ∨
          HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
              (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) ≠
            0)
rw₂ :
  W'.Equation P ∧
      (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) ≠
          0 ∨
        2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 ≠ 0 ∨
          Ne (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ : R) (0 : R)) ↔
    W'.Equation P ∧
      (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) ≠
          0 ∨
        2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 ≠ 0 ∨
          HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
              (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) ≠
            0)
⊢ W'.Nonsingular P ↔
    W'.Equation P ∧
      (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) ≠
          0 ∨
        2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 ≠ 0 ∨
          HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
              (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) ≠
            0)
have rw₃ : W'.Equation P ∧
    (W'.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) ≠
        0 ∨
      2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 ≠ 0 ∨
        HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
            (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) ≠
          0) ↔
  W'.Equation P ∧
    (W'.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) ≠
        0 ∨
      2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 ≠ 0 ∨
        HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
            (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) ≠
          0)
Tactic: rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]