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 : IsUnit u_1
u : R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.Equation (u • P)
have rw : ∀
  (hP :
    HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 6) =
      0),
  HPow.hPow (β := ℕ) ((u • P) y) 2 + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
        W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 3 -
      (HPow.hPow (β := ℕ) ((u • P) x) 3 + W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * HPow.hPow (β := ℕ) ((u • P) z) 2 +
          W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 4 +
        W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 6) =
    0
Tactic: rw [equation_iff] at 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 : IsUnit u_1
u : R
P : Fin 3 → R
hP :
  HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 6) =
    0
⊢ HPow.hPow (β := ℕ) ((u • P) y) 2 + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
            W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 3 -
          (HPow.hPow (β := ℕ) ((u • P) x) 3 +
                W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * HPow.hPow (β := ℕ) ((u • P) z) 2 +
              W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 4 +
            W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 6) +
        HPow.hPow (β := ℕ) u 6 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 6 *
          (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 6))) =
    0
have a : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y) 2 +
            W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) u 3 * P y) * (u * P z) +
          W'.a₃ * (HPow.hPow (β := ℕ) u 3 * P y) * HPow.hPow (β := ℕ) (u * P z) 3 -
        (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 3 +
              W'.a₂ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 * HPow.hPow (β := ℕ) (u * P z) 2 +
            W'.a₄ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 4 +
          W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 6) +
      HPow.hPow (β := ℕ) u 6 * 0 -
    (0 +
      HPow.hPow (β := ℕ) u 6 *
        (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
          (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
            W'.a₆ * HPow.hPow (β := ℕ) (P z) 6))) =
  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 : IsUnit u_1
u : R
P : Fin 3 → R
hP :
  HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 6) =
    0
⊢ HPow.hPow (β := ℕ) ((u • P) y) 2 + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
        W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 3 -
      (HPow.hPow (β := ℕ) ((u • P) x) 3 + W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * HPow.hPow (β := ℕ) ((u • P) z) 2 +
          W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 4 +
        W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 6) =
    0
have a : HPow.hPow (β := ℕ) ((u • P) y) 2 + W'.a₁ * (u • P) x * (u • P) y * (u • P) z +
          W'.a₃ * (u • P) y * HPow.hPow (β := ℕ) ((u • P) z) 3 -
        (HPow.hPow (β := ℕ) ((u • P) x) 3 +
              W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 * HPow.hPow (β := ℕ) ((u • P) z) 2 +
            W'.a₄ * (u • P) x * HPow.hPow (β := ℕ) ((u • P) z) 4 +
          W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 6) +
      HPow.hPow (β := ℕ) u 6 * 0 -
    (0 +
      HPow.hPow (β := ℕ) u 6 *
        (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
          (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
            W'.a₆ * HPow.hPow (β := ℕ) (P z) 6))) =
  0
Tactic: linear_combination (norm := (simp only [smul_fin3_ext]; ring1)) u ^ 6 * hP
-- 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) {P : Fin 3 → R} (hP : W'.Equation P), W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ W'.Equation P
have h₁ : P = (↑hu.unit⁻¹ : R) • u • P
Tactic: convert! hP (↑hu.unit⁻¹) h
-- 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) {P : Fin 3 → R} (hP : W'.Equation P), W'.Equation (u • P)
h : W'.Equation (u • P)
⊢ P = (↑hu.unit⁻¹ : R) • u • P
have h₁ : P = ((↑hu.unit⁻¹ : R) * u) • P
Tactic: rw [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) {P : Fin 3 → R} (hP : W'.Equation P), W'.Equation (u • P)
h : W'.Equation (u • P)
h₁ : P = ((↑hu.unit⁻¹ : R) * u) • P
⊢ P = (↑hu.unit⁻¹ : R) • u • P
have h₂ : P = HSMul.hSMul (α := R) 1 P
Tactic: rw [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) {P : Fin 3 → R} (hP : W'.Equation P), W'.Equation (u • P)
h : W'.Equation (u • P)
h₁ : P = ((↑hu.unit⁻¹ : R) * u) • P
h₂ : P = HSMul.hSMul (α := R) 1 P
⊢ P = (↑hu.unit⁻¹ : R) • u • P
have h₃ : P = P
Tactic: rw [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'.Equation P ↔ W'.Equation Q
have rcases : ∀ (u : Rˣ), W'.Equation ((fun (m : Rˣ) ↦ m • Q) u) ↔ W'.Equation 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
P : Fin 3 → R
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX =
    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)
have rw : (eval P : (a : MvPolynomial (Fin 3) R) → R)
    (HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
          ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) Y *
        Z -
      ((C : (a : R) → MvPolynomial (Fin 3) R) 3 * HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2 +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) (2 * W'.a₂) : MvPolynomial (Fin 3) R) X *
            HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 +
        HMul.hMul (α := MvPolynomial (Fin 3) R) ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₄ : MvPolynomial (Fin 3) R)
          (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 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)
Tactic: rw [polynomialX_eq]
-- 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
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 4) +
        (W.a₁ * P y / HPow.hPow (β := ℕ) (P z) 3 * 1 +
            2 * W.a₂ * P x / HPow.hPow (β := ℕ) (P z) 2 * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
          W.a₄ * (HPow.hPow (β := ℕ) (P z) 4 / HPow.hPow (β := ℕ) (P z) 4)) -
      (Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
          W.toAffine.polynomialX +
        (W.a₁ * P y / HPow.hPow (β := ℕ) (P z) 3 * (P z / P z) + 2 * W.a₂ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₄ * 1)) =
    0
have a : (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)) /
        HPow.hPow (β := ℕ) (P z) 4 +
      (W.a₁ * P y / HPow.hPow (β := ℕ) (P z) 3 * 1 +
          2 * W.a₂ * P x / HPow.hPow (β := ℕ) (P z) 2 * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
        W.a₄ * (HPow.hPow (β := ℕ) (P z) 4 / HPow.hPow (β := ℕ) (P z) 4)) -
    (W.toAffine.a₁ * (P y / HPow.hPow (β := ℕ) (P z) 3) -
        (3 * HPow.hPow (β := ℕ) (P x / HPow.hPow (β := ℕ) (P z) 2) 2 +
            2 * W.toAffine.a₂ * (P x / HPow.hPow (β := ℕ) (P z) 2) +
          W.toAffine.a₄) +
      (W.a₁ * P y / HPow.hPow (β := ℕ) (P z) 3 * (P z / P z) + 2 * W.a₂ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
        W.a₄ * 1)) =
  0
Tactic: rw [eval_polynomialX, Affine.evalEval_polynomialX]
-- 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
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 4) =
    Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) W.toAffine.polynomialX
have a : HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (HPow.hPow (β := ℕ) (P z) 4) +
      (W.a₁ * P y / HPow.hPow (β := ℕ) (P z) 3 * 1 +
          2 * W.a₂ * P x / HPow.hPow (β := ℕ) (P z) 2 * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
        W.a₄ * (HPow.hPow (β := ℕ) (P z) 4 / HPow.hPow (β := ℕ) (P z) 4)) -
    (Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) W.toAffine.polynomialX +
      (W.a₁ * P y / HPow.hPow (β := ℕ) (P z) 3 * (P z / P z) + 2 * W.a₂ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
        W.a₄ * 1)) =
  0
Tactic: linear_combination (norm := (rw [eval_polynomialX, Affine.evalEval_polynomialX]; ring1))
    W.a₁ * P y / P z ^ 3 * div_self hPz - 2 * W.a₂ * P x / P z ^ 2 * div_self (pow_ne_zero 2 hPz)
      - W.a₄ * div_self (pow_ne_zero 4 hPz)
-- 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
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY =
    2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3
have rw : (eval P : (a : MvPolynomial (Fin 3) R) → R)
    (HMul.hMul (α := MvPolynomial (Fin 3) R) ((C : (a : R) → MvPolynomial (Fin 3) R) 2) Y +
        HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) X *
          Z +
      HMul.hMul (α := MvPolynomial (Fin 3) R) ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₃ : MvPolynomial (Fin 3) R)
        (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 3)) =
  2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3
Tactic: rw [polynomialY_eq]
-- 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
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (HPow.hPow (β := ℕ) (P z) 3) +
        (W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 + W.a₃ * 1) -
      (Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)
          W.toAffine.polynomialY +
        (W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
          W.a₃ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3))) =
    0
have a : (2 * P y + W.a₁ * P x * P z + W.a₃ * HPow.hPow (β := ℕ) (P z) 3) / HPow.hPow (β := ℕ) (P z) 3 +
      (W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 + W.a₃ * 1) -
    (2 * (P y / HPow.hPow (β := ℕ) (P z) 3) + W.toAffine.a₁ * (P x / HPow.hPow (β := ℕ) (P z) 2) + W.toAffine.a₃ +
      (W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
        W.a₃ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3))) =
  0
Tactic: rw [eval_polynomialY, Affine.evalEval_polynomialY]
-- 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
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (HPow.hPow (β := ℕ) (P z) 3) =
    Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) W.toAffine.polynomialY
have a : HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (HPow.hPow (β := ℕ) (P z) 3) +
      (W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 + W.a₃ * 1) -
    (Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) W.toAffine.polynomialY +
      (W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) +
        W.a₃ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3))) =
  0
Tactic: linear_combination (norm := (rw [eval_polynomialY, Affine.evalEval_polynomialY]; ring1))
    W.a₁ * P x / P z ^ 2 * div_self hPz + W.a₃ * div_self (pow_ne_zero 3 hPz)
-- 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
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ =
    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)
have rw : (eval P : (a : MvPolynomial (Fin 3) R) → R)
    (HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) W'.a₁ : MvPolynomial (Fin 3) R) X *
          Y +
        HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) (3 * W'.a₃) : MvPolynomial (Fin 3) R) Y *
          HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2 -
      (HMul.hMul (α := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) (2 * W'.a₂) : MvPolynomial (Fin 3) R)
              (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) X 2) *
            Z +
          HMul.hMul (α := MvPolynomial (Fin 3) R) (β := MvPolynomial (Fin 3) R)
              ((C : (a : R) → MvPolynomial (Fin 3) R) (4 * W'.a₄) : MvPolynomial (Fin 3) R) X *
            HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 3 +
        HMul.hMul (α := MvPolynomial (Fin 3) R)
          ((C : (a : R) → MvPolynomial (Fin 3) R) (6 * W'.a₆) : MvPolynomial (Fin 3) R)
          (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 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)
Tactic: rw [polynomialZ_eq]
-- 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
⊢ HMul.hMul (α := R) (β := R) (6 : R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) =
    HMul.hMul (β := R) (2 * P x) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) +
        HMul.hMul (β := R) (3 * P y) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY : R) +
      HMul.hMul (β := R) (P z) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ : R)
have rw : 6 *
    (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
      (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
        W'.a₆ * HPow.hPow (β := ℕ) (P z) 6)) =
  2 * P x *
        (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)) +
      3 * P y * (2 * P y + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) +
    P z *
      (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))
Tactic: rw [eval_polynomial, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
-- 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
⊢ 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 ∧
    (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)
Tactic: rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
-- 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)
⊢ 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 ∨
      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)
Tactic: rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (hypothesis)
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 : W'.Nonsingular (u • P)
⊢ W'.Nonsingular P
have hP₁ : W'.Equation (u • P)
Tactic: rcases (nonsingular_iff _).mp hP with ⟨hP, hP'⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic (hypothesis)
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 : W'.Nonsingular (u • P)
hP₁ : W'.Equation (u • P)
⊢ W'.Nonsingular P
have 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
Tactic: rcases (nonsingular_iff _).mp hP with ⟨hP, hP'⟩