-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian 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 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₄ * HPow.hPow (β := ℕ) (P z) 4) ≠
          0 ∨
        2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 ≠ 0 ∨
          W'.a₁ * P x * P y + 3 * W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
              (2 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + 4 * W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 3 +
                6 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 5) ≠
            0)
rw₁ :
  W'.Equation P ∧
      (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₄ * HPow.hPow (β := ℕ) (P z) 4) ≠
          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 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₄ * HPow.hPow (β := ℕ) (P z) 4) ≠
          0 ∨
        2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 ≠ 0 ∨
          W'.a₁ * P x * P y + 3 * W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
              (2 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + 4 * W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 3 +
                6 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 5) ≠
            0)
⊢ W'.Nonsingular P ↔
    W'.Equation P ∧
      (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₄ * HPow.hPow (β := ℕ) (P z) 4) ≠
          0 ∨
        2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 ≠ 0 ∨
          W'.a₁ * P x * P y + 3 * W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
              (2 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + 4 * W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 3 +
                6 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 5) ≠
            0)
have rw₂ : W'.Equation P ∧
    (W'.a₁ * P y * P z -
          (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₄ * HPow.hPow (β := ℕ) (P z) 4) ≠
        0 ∨
      2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 ≠ 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 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₄ * HPow.hPow (β := ℕ) (P z) 4) ≠
        0 ∨
      2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 ≠ 0 ∨
        W'.a₁ * P x * P y + 3 * W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
            (2 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z + 4 * W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 3 +
              6 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 5) ≠
          0)
Tactic: rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]