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 :
  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
⊢ 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

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)

Premises used: WeierstrassCurve.Jacobian.eval_polynomialX, pow_ne_zero, WeierstrassCurve.a₂, WeierstrassCurve.a₄, WeierstrassCurve.Affine.evalEval_polynomialX, 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 :
  (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
⊢ (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

Tactic:
rw [polynomialY_eq]

Premises used: WeierstrassCurve.Jacobian.polynomialY_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) ((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:
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 :
  (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
⊢ 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:
rw [eval_polynomialY, Affine.evalEval_polynomialY]

Premises used: WeierstrassCurve.Jacobian.eval_polynomialY, WeierstrassCurve.Affine.evalEval_polynomialY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (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:
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.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
⊢ 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

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)

Premises used: WeierstrassCurve.Jacobian.eval_polynomialY, pow_ne_zero, WeierstrassCurve.a₃, WeierstrassCurve.Affine.evalEval_polynomialY, 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 :
  (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)
⊢ (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)

Tactic:
rw [polynomialZ_eq]

Premises used: WeierstrassCurve.Jacobian.polynomialZ_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) 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:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
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))
⊢ 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)

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

Premises used: WeierstrassCurve.Jacobian.eval_polynomialY, WeierstrassCurve.Jacobian.eval_polynomialX, WeierstrassCurve.Jacobian.eval_polynomial, WeierstrassCurve.Jacobian.eval_polynomialZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ 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:
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_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP : W'.Nonsingular (u • P)
⊢ W'.Equation (u • P)

Tactic:
rcases (nonsingular_iff _).mp hP with ⟨hP, hP'⟩

Premises used: Iff.mp, WeierstrassCurve.Jacobian.nonsingular_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_1 : IsUnit u_1
u : R
hu : IsUnit u
P : Fin 3 → R
hP : W'.Nonsingular (u • P)
hP₁ : W'.Equation (u • P)
⊢ 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'⟩

Premises used: Iff.mp, WeierstrassCurve.Jacobian.nonsingular_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_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

Tactic:
(nonsingular_iff P).mpr ⟨(equation_smul P hu).mp hP, ?_⟩

Premises used: Iff.mpr, And.intro, Iff.mp, WeierstrassCurve.Jacobian.equation_smul, WeierstrassCurve.Jacobian.nonsingular_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_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
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
⊢ W'.Nonsingular P

Tactic:
refine (nonsingular_iff P).mpr ⟨(equation_smul P hu).mp hP, ?_⟩

Premises used: Iff.mpr, And.intro, Iff.mp, WeierstrassCurve.Jacobian.equation_smul, WeierstrassCurve.Jacobian.nonsingular_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_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
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
⊢ 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:
contrapose! hP'
-- 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_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
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
⊢ 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:
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_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) +
        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:
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_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
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
⊢ 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

Tactic:
linear_combination (norm := ring1) u ^ 4 * hP'.left

Premises used: And.left