-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
rw :
  W.toAffine.Nonsingular (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ↔
    W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F))
rw₁ :
  W.toAffine.Equation (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ∧
      (Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
            W.toAffine.polynomialX ≠
          0 ∨
        Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
            W.toAffine.polynomialY ≠
          0) ↔
    W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F))
rw₂ :
  W.Equation P ∧
      (Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
            W.toAffine.polynomialX ≠
          0 ∨
        Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
            W.toAffine.polynomialY ≠
          0) ↔
    W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F))
rw₃ :
  W.Equation P ∧
      (HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 4) ≠
          0 ∨
        Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
            W.toAffine.polynomialY ≠
          0) ↔
    W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F))
rw₄ :
  W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∧
          HPow.hPow (β := ℕ) (P z) 4 ≠ 0 ∨
        Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
            W.toAffine.polynomialY ≠
          0) ↔
    W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F))
⊢ W.Nonsingular P ↔
    W.Equation P ∧
      (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
        Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F))
have rw₅ : W.Equation P ∧
    (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
      Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) W.toAffine.polynomialY ≠
        0) ↔
  W.Equation P ∧
    (Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (0 : F) ∨
      Ne (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (0 : F))
Tactic: rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz,
    ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 4 hPz,
    ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 3 hPz]