-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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)
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)
rw₃ 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 ∨
          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'.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)

Tactic:
rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]

Premises used: WeierstrassCurve.Jacobian.eval_polynomialY, WeierstrassCurve.Jacobian.eval_polynomialX, WeierstrassCurve.Jacobian.Nonsingular, WeierstrassCurve.Jacobian.eval_polynomialZ