awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
a :
  (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)) /
          HPow.hPow (β := ℕ) (P z) 6 +
        (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * 1 + W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * 1 +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 *
                (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
            W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * (HPow.hPow (β := ℕ) (P z) 4 / HPow.hPow (β := ℕ) (P z) 4) +
          W.a₆ * (HPow.hPow (β := ℕ) (P z) 6 / HPow.hPow (β := ℕ) (P z) 6)) -
      (HPow.hPow (β := ℕ) (P y / HPow.hPow (β := ℕ) (P z) 3) 2 +
              W.toAffine.a₁ * (P x / HPow.hPow (β := ℕ) (P z) 2) * (P y / HPow.hPow (β := ℕ) (P z) 3) +
            W.toAffine.a₃ * (P y / HPow.hPow (β := ℕ) (P z) 3) -
          (HPow.hPow (β := ℕ) (P x / HPow.hPow (β := ℕ) (P z) 2) 3 +
                W.toAffine.a₂ * HPow.hPow (β := ℕ) (P x / HPow.hPow (β := ℕ) (P z) 2) 2 +
              W.toAffine.a₄ * (P x / HPow.hPow (β := ℕ) (P z) 2) +
            W.toAffine.a₆) +
        (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * (P z / P z) +
                W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3) +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 * 1 +
            W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₆ * 1)) =
    0
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomial : F) (HPow.hPow (β := ℕ) (P z) 6) +
        (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * 1 + W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * 1 +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 *
                (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
            W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * (HPow.hPow (β := ℕ) (P z) 4 / HPow.hPow (β := ℕ) (P z) 4) +
          W.a₆ * (HPow.hPow (β := ℕ) (P z) 6 / HPow.hPow (β := ℕ) (P z) 6)) -
      (Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) W.toAffine.polynomial +
        (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * (P z / P z) +
                W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3) +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 * 1 +
            W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₆ * 1)) =
    0

Tactic:
rw [eval_polynomial, Affine.evalEval_polynomial]

Premises used: WeierstrassCurve.Jacobian.eval_polynomial, WeierstrassCurve.Affine.evalEval_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (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)) /
          HPow.hPow (β := ℕ) (P z) 6 +
        (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * 1 + W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * 1 +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 *
                (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
            W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * (HPow.hPow (β := ℕ) (P z) 4 / HPow.hPow (β := ℕ) (P z) 4) +
          W.a₆ * (HPow.hPow (β := ℕ) (P z) 6 / HPow.hPow (β := ℕ) (P z) 6)) -
      (HPow.hPow (β := ℕ) (P y / HPow.hPow (β := ℕ) (P z) 3) 2 +
              W.toAffine.a₁ * (P x / HPow.hPow (β := ℕ) (P z) 2) * (P y / HPow.hPow (β := ℕ) (P z) 3) +
            W.toAffine.a₃ * (P y / HPow.hPow (β := ℕ) (P z) 3) -
          (HPow.hPow (β := ℕ) (P x / HPow.hPow (β := ℕ) (P z) 2) 3 +
                W.toAffine.a₂ * HPow.hPow (β := ℕ) (P x / HPow.hPow (β := ℕ) (P z) 2) 2 +
              W.toAffine.a₄ * (P x / HPow.hPow (β := ℕ) (P z) 2) +
            W.toAffine.a₆) +
        (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * (P z / P z) +
                W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3) +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 * 1 +
            W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₆ * 1)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
a :
  HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomial : F) (HPow.hPow (β := ℕ) (P z) 6) +
        (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * 1 + W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * 1 +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 *
                (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2) +
            W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * (HPow.hPow (β := ℕ) (P z) 4 / HPow.hPow (β := ℕ) (P z) 4) +
          W.a₆ * (HPow.hPow (β := ℕ) (P z) 6 / HPow.hPow (β := ℕ) (P z) 6)) -
      (Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) W.toAffine.polynomial +
        (W.a₁ * P x * P y / HPow.hPow (β := ℕ) (P z) 5 * (P z / P z) +
                W.a₃ * P y / HPow.hPow (β := ℕ) (P z) 3 * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3) +
              W.a₂ * HPow.hPow (β := ℕ) (P x) 2 / HPow.hPow (β := ℕ) (P z) 4 * 1 +
            W.a₄ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₆ * 1)) =
    0
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomial : F) (HPow.hPow (β := ℕ) (P z) 6) =
    Polynomial.evalEval (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) W.toAffine.polynomial

Tactic:
linear_combination (norm := (rw [eval_polynomial, Affine.evalEval_polynomial]; ring1))
    W.a₁ * P x * P y / P z ^ 5 * div_self hPz + W.a₃ * P y / P z ^ 3 * div_self (pow_ne_zero 3 hPz)
      - W.a₂ * P x ^ 2 / P z ^ 4 * div_self (pow_ne_zero 2 hPz)
      - W.a₄ * P x / P z ^ 2 * div_self (pow_ne_zero 4 hPz) - W.a₆ * div_self (pow_ne_zero 6 hPz)

Premises used: pow_ne_zero, WeierstrassCurve.a₂, WeierstrassCurve.a₃, WeierstrassCurve.a₆, WeierstrassCurve.Jacobian.eval_polynomial, WeierstrassCurve.a₄, WeierstrassCurve.Affine.evalEval_polynomial, OfNat.ofNat, div_self, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
rw :
  Eq (α := R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) (0 : R) ↔
    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
rw₁ rw₂ :
  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 (β := ℕ) (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
⊢ W'.Equation P ↔
    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:
rw [Equation, eval_polynomial]

Premises used: WeierstrassCurve.Jacobian.Equation, WeierstrassCurve.Jacobian.eval_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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
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
⊢ W'.Equation (u • P)

Tactic:
rw [equation_iff] at hP ⊢

Premises used: WeierstrassCurve.Jacobian.equation_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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
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
⊢ 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:
simp only [smul_fin3_ext]

Premises used: WeierstrassCurve.Jacobian.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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 (β := ℕ) (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:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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
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
⊢ 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:
linear_combination (norm := (simp only [smul_fin3_ext]; ring1)) u ^ 6 * hP

Premises used: WeierstrassCurve.Jacobian.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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 ((↑hu.unit⁻¹ : R) • u • P)

Tactic:
hP (↑hu.unit⁻¹) h

Premises used: Units.val, Inv.inv, IsUnit.unit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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
⊢ W'.Equation P

Tactic:
convert! hP (↑hu.unit⁻¹) h

Premises used: Units.val, Inv.inv, IsUnit.unit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
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
h₃ h₄ : P = P
⊢ P = (↑hu.unit⁻¹ : R) • u • P

Tactic:
rw [smul_smul, hu.val_inv_mul, one_smul]

Premises used: smul_smul, one_smul, IsUnit.val_inv_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
rcases : ∀ (u : Rˣ), W'.Equation ((fun (m : Rˣ) ↦ m • Q) u) ↔ W'.Equation Q
⊢ W'.Equation P ↔ W'.Equation Q

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Equation ((fun (m : Rˣ) ↦ m • Q) u) ↔ W'.Equation Q

Tactic:
equation_smul Q u.isUnit

Premises used: WeierstrassCurve.Jacobian.equation_smul, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
Q : Fin 3 → R
u : Rˣ
⊢ W'.Equation ((fun (m : Rˣ) ↦ m • Q) u) ↔ W'.Equation Q

Tactic:
exact equation_smul Q u.isUnit

Premises used: WeierstrassCurve.Jacobian.equation_smul, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.Equation P ↔ HPow.hPow (β := ℕ) (P y) 2 = HPow.hPow (β := ℕ) (P x) 3

Tactic:
simp only [equation_iff, hPz, add_zero, mul_zero, zero_pow <| OfNat.ofNat_ne_zero _, sub_eq_zero]

Premises used: OfNat.ofNat_ne_zero, sub_eq_zero, MulZeroClass.mul_zero, WeierstrassCurve.Jacobian.equation_iff, add_zero, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
⊢ W'.Equation ![1, 1, 0]

Tactic:
simp only [equation_of_Z_eq_zero, fin3_def_ext, one_pow]

Premises used: one_pow, WeierstrassCurve.Jacobian.fin3_def_ext, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
a b : R
⊢ W'.Equation ![a, b, 1] ↔ W'.toAffine.Equation a b

Tactic:
simp only [equation_iff, Affine.equation_iff', fin3_def_ext, one_pow, mul_one]

Premises used: one_pow, WeierstrassCurve.Affine.equation_iff', WeierstrassCurve.Jacobian.fin3_def_ext, WeierstrassCurve.Jacobian.equation_iff, mul_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.Equation P ↔ W.toAffine.Equation (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)

Tactic:
(equation_of_equiv <| equiv_some_of_Z_ne_zero hPz).trans <| equation_some ..

Premises used: WeierstrassCurve.Jacobian.equation_of_equiv, Iff.trans, WeierstrassCurve.Jacobian.equation_some, WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
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)
⊢ (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)

Tactic:
rw [polynomialX_eq]

Premises used: WeierstrassCurve.Jacobian.polynomialX_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (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:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
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
⊢ 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:
rw [eval_polynomialX, Affine.evalEval_polynomialX]

Premises used: WeierstrassCurve.Jacobian.eval_polynomialX, WeierstrassCurve.Affine.evalEval_polynomialX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 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)) /
          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:
ring1