awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P_1 : Fin 3 → R
u_1 : R
hu_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP_1 : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * (u • P) y * (u • P) z -
        (3 * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₂ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
          W'.a₄ * HPow.hPow (β := ℕ) ((u • P) z) 4) ≠
      0 ∨
    2 * (u • P) y + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * HPow.hPow (β := ℕ) ((u • P) z) 3 ≠ 0 ∨
      W'.a₁ * (u • P) x * (u • P) y + 3 * W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
              4 * W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 5) ≠
        0
⊢ W'.Nonsingular P
have refine : 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: refine (nonsingular_iff P).mpr ⟨(equation_smul P hu).mp hP, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P_1 : Fin 3 → R
u_1 : R
hu_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP_1 : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  W'.a₁ * (u • P) y * (u • P) z -
        (3 * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₂ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
          W'.a₄ * HPow.hPow (β := ℕ) ((u • P) z) 4) ≠
      0 ∨
    2 * (u • P) y + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * HPow.hPow (β := ℕ) ((u • P) z) 3 ≠ 0 ∨
      W'.a₁ * (u • P) x * (u • P) y + 3 * W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
              4 * W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 5) ≠
        0
⊢ 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 contrapose! : ∀
  (hP' :
    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'.a₁ * (u • P) y * (u • P) z -
        (3 * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₂ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
          W'.a₄ * HPow.hPow (β := ℕ) ((u • P) z) 4) =
      0 ∧
    2 * (u • P) y + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * HPow.hPow (β := ℕ) ((u • P) z) 3 = 0 ∧
      W'.a₁ * (u • P) x * (u • P) y + 3 * W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
              4 * W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 5) =
        0
Tactic: contrapose! hP'
Cleared hypotheses: hP'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P_1 : Fin 3 → R
u_1 : R
hu_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP_1 : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  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'.a₁ * (u • P) y * (u • P) z -
        (3 * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₂ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 2 +
          W'.a₄ * HPow.hPow (β := ℕ) ((u • P) z) 4) =
      0 ∧
    2 * (u • P) y + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * HPow.hPow (β := ℕ) ((u • P) z) 3 = 0 ∧
      W'.a₁ * (u • P) x * (u • P) y + 3 * W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 2 -
          (2 * W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * (u • P) z +
              4 * W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 3 +
            6 * W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 5) =
        0
have simp : W'.a₁ * (HPow.hPow (β := ℕ) u 3 * P y) * (u * P z) -
      (3 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 +
          2 * W'.a₂ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (u * P z) 4) =
    0 ∧
  2 * (HPow.hPow (β := ℕ) u 3 * P y) + W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (u * P z) +
        W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 3 =
      0 ∧
    W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) +
          3 * W'.a₃ * (HPow.hPow (β := ℕ) u 3 * P y) * HPow.hPow (β := ℕ) (u * P z) 2 -
        (2 * W'.a₂ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 * (u * P z) +
            4 * W'.a₄ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 3 +
          6 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 5) =
      0
Tactic: simp only [smul_fin3_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P_1 : Fin 3 → R
u_1 : R
hu_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP_1 : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  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'.a₁ * (HPow.hPow (β := ℕ) u 3 * P y) * (u * P z) -
      (3 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 +
          2 * W'.a₂ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (u * P z) 4) =
    0
have a : W'.a₁ * (HPow.hPow (β := ℕ) u 3 * P y) * (u * P z) -
        (3 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 +
            2 * W'.a₂ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 2 +
          W'.a₄ * HPow.hPow (β := ℕ) (u * P z) 4) +
      HPow.hPow (β := ℕ) u 4 * 0 -
    (0 +
      HPow.hPow (β := ℕ) u 4 *
        (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
Tactic: linear_combination (norm := ring1) u ^ 4 * hP'.left
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P_1 : Fin 3 → R
u_1 : R
hu_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP_1 : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  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
⊢ 2 * (HPow.hPow (β := ℕ) u 3 * P y) + W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (u * P z) +
      W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 3 =
    0
have a : 2 * (HPow.hPow (β := ℕ) u 3 * P y) + W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (u * P z) +
        W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 3 +
      HPow.hPow (β := ℕ) u 3 * 0 -
    (0 + HPow.hPow (β := ℕ) u 3 * (2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) =
  0
Tactic: linear_combination (norm := ring1) u ^ 3 * hP'.right.left
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P_1 : Fin 3 → R
u_1 : R
hu_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP_1 : W'.Nonsingular (u • P)
hP : W'.Equation (u • P)
hP' :
  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'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) +
        3 * W'.a₃ * (HPow.hPow (β := ℕ) u 3 * P y) * HPow.hPow (β := ℕ) (u * P z) 2 -
      (2 * W'.a₂ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 * (u * P z) +
          4 * W'.a₄ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 3 +
        6 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 5) =
    0
have a : W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) +
          3 * W'.a₃ * (HPow.hPow (β := ℕ) u 3 * P y) * HPow.hPow (β := ℕ) (u * P z) 2 -
        (2 * W'.a₂ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 * (u * P z) +
            4 * W'.a₄ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 3 +
          6 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 5) +
      HPow.hPow (β := ℕ) u 5 * 0 -
    (0 +
      HPow.hPow (β := ℕ) u 5 *
        (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: linear_combination (norm := ring1) u ^ 5 * hP'.right.right
-- 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
u : R
hu : IsUnit u
hP : ∀ {u : R} (hu : IsUnit u) {P : Fin 3 → R} (hP : W'.Nonsingular (u • P)), W'.Nonsingular P
h : W'.Nonsingular P
⊢ W'.Nonsingular ((↑hu.unit⁻¹ : R) • u • P)
have rwa : W'.Nonsingular (((↑hu.unit⁻¹ : R) * u) • P)
Tactic: rwa [smul_smul, hu.val_inv_mul, one_smul]
-- 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
u : R
hu : IsUnit u
hP : ∀ {u : R} (hu : IsUnit u) {P : Fin 3 → R} (hP : W'.Nonsingular (u • P)), W'.Nonsingular P
h : W'.Nonsingular P
rwa : W'.Nonsingular (((↑hu.unit⁻¹ : R) * u) • P)
⊢ W'.Nonsingular ((↑hu.unit⁻¹ : R) • u • P)
have rwa₁ : W'.Nonsingular (HSMul.hSMul (α := R) 1 P)
Tactic: rwa [smul_smul, hu.val_inv_mul, one_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.Nonsingular P ↔ W'.Nonsingular Q
have rcases : ∀ (u : Rˣ), W'.Nonsingular ((fun (m : Rˣ) ↦ m • Q) u) ↔ W'.Nonsingular Q
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: P, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : Nontrivial R
⊢ W'.Nonsingular ![1, 1, 0]
have simp : ¬(3 * HPow.hPow (α := R) (β := ℕ) 1 2 = 0 ∧ HMul.hMul (α := R) 2 1 = 0 ∧ W'.a₁ * 1 * 1 = 0)
Tactic: simp only [nonsingular_of_Z_eq_zero, equation_zero, true_and, fin3_def_ext, ← not_and_or]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : Nontrivial R
h : 3 * HPow.hPow (α := R) (β := ℕ) 1 2 = 0 ∧ HMul.hMul (α := R) 2 1 = 0 ∧ W'.a₁ * 1 * 1 = 0
⊢ Eq.{r + 1} (α := R) 1 0
have a : 1 + (0 + HMul.hMul (α := R) 2 1) - (0 + (3 * HPow.hPow (α := R) (β := ℕ) 1 2 + 0)) = 0
Tactic: linear_combination (norm := ring1) h.1 - h.2.1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
a b : R
⊢ W'.Nonsingular ![a, b, 1] ↔ W'.toAffine.Nonsingular a b
have simp_rw : HPow.hPow (β := ℕ) b 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
      (HPow.hPow (β := ℕ) a 3 + W'.toAffine.a₂ * HPow.hPow (β := ℕ) a 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
    0 →
  W'.a₁ * b - (3 * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₂ * a + W'.a₄) = 0 →
    2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0 →
      W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * HPow.hPow (β := ℕ) a 2 + 4 * W'.a₄ * a + 6 * W'.a₆) = 0
Tactic: simp_rw [nonsingular_iff, equation_some, fin3_def_ext, Affine.nonsingular_iff',
    Affine.equation_iff', and_congr_right_iff, ← not_and_or, not_iff_not, one_pow, mul_one,
    and_congr_right_iff, Iff.comm, iff_self_and]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
a b : R
h :
  HPow.hPow (β := ℕ) b 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
      (HPow.hPow (β := ℕ) a 3 + W'.toAffine.a₂ * HPow.hPow (β := ℕ) a 2 + W'.toAffine.a₄ * a + W'.toAffine.a₆) =
    0
ha : W'.a₁ * b - (3 * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₂ * a + W'.a₄) = 0
hb : 2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃ = 0
⊢ W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * HPow.hPow (β := ℕ) a 2 + 4 * W'.a₄ * a + 6 * W'.a₆) = 0
have a₁ : W'.a₁ * a * b + 3 * W'.a₃ * b - (2 * W'.a₂ * HPow.hPow (β := ℕ) a 2 + 4 * W'.a₄ * a + 6 * W'.a₆) +
      (HMul.hMul (α := R) 6 0 + 2 * a * (W'.a₁ * b - (3 * HPow.hPow (β := ℕ) a 2 + 2 * W'.a₂ * a + W'.a₄)) +
        3 * b * (2 * b + W'.toAffine.a₁ * a + W'.toAffine.a₃)) -
    (0 +
      (6 *
            (HPow.hPow (β := ℕ) b 2 + W'.toAffine.a₁ * a * b + W'.toAffine.a₃ * b -
              (HPow.hPow (β := ℕ) a 3 + W'.toAffine.a₂ * HPow.hPow (β := ℕ) a 2 + W'.toAffine.a₄ * a +
                W'.toAffine.a₆)) +
          2 * a * 0 +
        3 * b * 0)) =
  0
Tactic: linear_combination (norm := ring1) 6 * h - 2 * a * ha - 3 * b * hb
-- 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
⊢ 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.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))
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]
-- 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))
⊢ 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.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))
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]
-- 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))
⊢ 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 ∧
    (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))
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]
-- 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))
⊢ 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 ∧
    (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))
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]