awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * Z +
          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 2)) =
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialY =
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2

Tactic:
rw [polynomialY_eq]

Premises used: WeierstrassCurve.Projective.polynomialY_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * Z +
          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 2)) =
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2

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

Tactic:
rw [eval_polynomialY, Affine.evalEval_polynomialY]

Premises used: WeierstrassCurve.Affine.evalEval_polynomialY, WeierstrassCurve.Projective.eval_polynomialY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (2 * P y * P z + W.a₁ * P x * P z + W.a₃ * HPow.hPow (β := ℕ) (P z) 2) / HPow.hPow (β := ℕ) (P z) 2 +
        (2 * P y / P z * 1 + W.a₁ * P x / P z * 1 + W.a₃ * 1) -
      (2 * (P y / P z) + W.toAffine.a₁ * (P x / P z) + W.toAffine.a₃ +
        (2 * P y / P z * (P z / P z) + W.a₁ * P x / P z * (P z / P z) +
          W.a₃ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2))) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
F : Type u
inst : Field F
W : Projective 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) 2) +
        (2 * P y / P z * 1 + W.a₁ * P x / P z * 1 + W.a₃ * 1) -
      (Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY +
        (2 * P y / P z * (P z / P z) + W.a₁ * P x / P z * (P z / P z) +
          W.a₃ * (HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2))) =
    0
⊢ HDiv.hDiv (α := F) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialY : F) (HPow.hPow (β := ℕ) (P z) 2) =
    Polynomial.evalEval (P x / P z) (P y / P z) W.toAffine.polynomialY

Tactic:
linear_combination (norm := (rw [eval_polynomialY, Affine.evalEval_polynomialY]; ring1))
    2 * P y / P z * div_self hPz + W.a₁ * P x / P z * div_self hPz
      + W.a₃ * div_self (pow_ne_zero 2 hPz)

Premises used: pow_ne_zero, WeierstrassCurve.a₃, WeierstrassCurve.Affine.evalEval_polynomialY, OfNat.ofNat, WeierstrassCurve.Projective.eval_polynomialY, div_self, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
rw :
  (eval P : (a : MvPolynomial (Fin 3) R) → R)
      (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Y 2 +
            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) (2 * W'.a₃) : MvPolynomial (Fin 3) R) Y *
            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) (β := ℕ) 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 *
              Z +
          HMul.hMul (α := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) (3 * W'.a₆) : MvPolynomial (Fin 3) R)
            (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2))) =
    HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
      (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2)
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialZ =
    HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
      (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2)

Tactic:
rw [polynomialZ_eq]

Premises used: WeierstrassCurve.Projective.polynomialZ_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P : (a : MvPolynomial (Fin 3) R) → R)
      (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Y 2 +
            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) (2 * W'.a₃) : MvPolynomial (Fin 3) R) Y *
            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) (β := ℕ) 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 *
              Z +
          HMul.hMul (α := MvPolynomial (Fin 3) R)
            ((C : (a : R) → MvPolynomial (Fin 3) R) (3 * W'.a₆) : MvPolynomial (Fin 3) R)
            (HPow.hPow (α := MvPolynomial (Fin 3) R) (β := ℕ) Z 2))) =
    HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
      (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
rw :
  3 *
      (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3)) =
    P x *
          (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2)) +
        P y * (2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2) +
      P z *
        (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2))
⊢ HMul.hMul (α := R) (β := R) (3 : R) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomial : R) =
    HMul.hMul (β := R) (P x) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) +
        HMul.hMul (β := R) (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.Projective.eval_polynomial, WeierstrassCurve.Projective.eval_polynomialX, WeierstrassCurve.Projective.eval_polynomialZ, WeierstrassCurve.Projective.eval_polynomialY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ 3 *
      (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
        (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₆ * HPow.hPow (β := ℕ) (P z) 3)) =
    P x *
          (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2)) +
        P y * (2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2) +
      P z *
        (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2))

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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: WeierstrassCurve.Projective.nonsingular_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * (u • P) z +
          W'.a₄ * HPow.hPow (β := ℕ) ((u • P) z) 2) ≠
      0 ∨
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * HPow.hPow (β := ℕ) ((u • P) z) 2 ≠ 0 ∨
      HPow.hPow (β := ℕ) ((u • P) y) 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₄ * (u • P) x * (u • P) z +
            3 * W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 2) ≠
        0

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

Premises used: WeierstrassCurve.Projective.nonsingular_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * (u • P) z +
          W'.a₄ * HPow.hPow (β := ℕ) ((u • P) z) 2) ≠
      0 ∨
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * HPow.hPow (β := ℕ) ((u • P) z) 2 ≠ 0 ∨
      HPow.hPow (β := ℕ) ((u • P) y) 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₄ * (u • P) x * (u • P) z +
            3 * W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 2) ≠
        0
⊢ W'.Nonsingular P

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

Premises used: Iff.mpr, WeierstrassCurve.Projective.nonsingular_iff, And.intro, WeierstrassCurve.Projective.equation_smul, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * (u • P) z +
          W'.a₄ * HPow.hPow (β := ℕ) ((u • P) z) 2) ≠
      0 ∨
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * HPow.hPow (β := ℕ) ((u • P) z) 2 ≠ 0 ∨
      HPow.hPow (β := ℕ) ((u • P) y) 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₄ * (u • P) x * (u • P) z +
            3 * W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 2) ≠
        0
refine :
  W'.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) ≠
      0 ∨
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 ≠ 0 ∨
      HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) ≠
        0
⊢ W'.Nonsingular P

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

Premises used: Iff.mpr, WeierstrassCurve.Projective.nonsingular_iff, And.intro, WeierstrassCurve.Projective.equation_smul, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * (u • P) z +
          W'.a₄ * HPow.hPow (β := ℕ) ((u • P) z) 2) ≠
      0 ∨
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * HPow.hPow (β := ℕ) ((u • P) z) 2 ≠ 0 ∨
      HPow.hPow (β := ℕ) ((u • P) y) 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₄ * (u • P) x * (u • P) z +
            3 * W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 2) ≠
        0
contrapose! :
  ∀
    (hP' :
      W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) =
          0 ∧
        2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 = 0 ∧
          HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
              (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) =
            0),
    W'.a₁ * (u • P) y * (u • P) z -
          (3 * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₂ * (u • P) x * (u • P) z +
            W'.a₄ * HPow.hPow (β := ℕ) ((u • P) z) 2) =
        0 ∧
      2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * HPow.hPow (β := ℕ) ((u • P) z) 2 = 0 ∧
        HPow.hPow (β := ℕ) ((u • P) y) 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
            (W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₄ * (u • P) x * (u • P) z +
              3 * W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 2) =
          0
⊢ W'.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) ≠
      0 ∨
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 ≠ 0 ∨
      HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) ≠
        0

Tactic:
contrapose! hP'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) =
      0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 = 0 ∧
      HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) =
        0
simp :
  W'.a₁ * (u * P y) * (u * P z) -
        (3 * HPow.hPow (β := ℕ) (u * P x) 2 + 2 * W'.a₂ * (u * P x) * (u * P z) +
          W'.a₄ * HPow.hPow (β := ℕ) (u * P z) 2) =
      0 ∧
    2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 2 = 0 ∧
      HPow.hPow (β := ℕ) (u * P y) 2 + W'.a₁ * (u * P x) * (u * P y) + 2 * W'.a₃ * (u * P y) * (u * P z) -
          (W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 + 2 * W'.a₄ * (u * P x) * (u * P z) +
            3 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 2) =
        0
⊢ W'.a₁ * (u • P) y * (u • P) z -
        (3 * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₂ * (u • P) x * (u • P) z +
          W'.a₄ * HPow.hPow (β := ℕ) ((u • P) z) 2) =
      0 ∧
    2 * (u • P) y * (u • P) z + W'.a₁ * (u • P) x * (u • P) z + W'.a₃ * HPow.hPow (β := ℕ) ((u • P) z) 2 = 0 ∧
      HPow.hPow (β := ℕ) ((u • P) y) 2 + W'.a₁ * (u • P) x * (u • P) y + 2 * W'.a₃ * (u • P) y * (u • P) z -
          (W'.a₂ * HPow.hPow (β := ℕ) ((u • P) x) 2 + 2 * W'.a₄ * (u • P) x * (u • P) z +
            3 * W'.a₆ * HPow.hPow (β := ℕ) ((u • P) z) 2) =
        0

Tactic:
simp only [smul_fin3_ext]

Premises used: WeierstrassCurve.Projective.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) =
      0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 = 0 ∧
      HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) =
        0
⊢ W'.a₁ * (u * P y) * (u * P z) -
          (3 * HPow.hPow (β := ℕ) (u * P x) 2 + 2 * W'.a₂ * (u * P x) * (u * P z) +
            W'.a₄ * HPow.hPow (β := ℕ) (u * P z) 2) +
        HPow.hPow (β := ℕ) u 2 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 2 *
          (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2))) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) =
      0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 = 0 ∧
      HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) =
        0
a :
  W'.a₁ * (u * P y) * (u * P z) -
          (3 * HPow.hPow (β := ℕ) (u * P x) 2 + 2 * W'.a₂ * (u * P x) * (u * P z) +
            W'.a₄ * HPow.hPow (β := ℕ) (u * P z) 2) +
        HPow.hPow (β := ℕ) u 2 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 2 *
          (W'.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2))) =
    0
⊢ W'.a₁ * (u * P y) * (u * P z) -
      (3 * HPow.hPow (β := ℕ) (u * P x) 2 + 2 * W'.a₂ * (u * P x) * (u * P z) +
        W'.a₄ * HPow.hPow (β := ℕ) (u * P z) 2) =
    0

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

Premises used: And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) =
      0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 = 0 ∧
      HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) =
        0
⊢ 2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 2 +
        HPow.hPow (β := ℕ) u 2 * 0 -
      (0 + HPow.hPow (β := ℕ) u 2 * (2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) =
      0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 = 0 ∧
      HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) =
        0
a :
  2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 2 +
        HPow.hPow (β := ℕ) u 2 * 0 -
      (0 + HPow.hPow (β := ℕ) u 2 * (2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2)) =
    0
⊢ 2 * (u * P y) * (u * P z) + W'.a₁ * (u * P x) * (u * P z) + W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 2 = 0

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

Premises used: And.right, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
Goal:
R : Type r
inst : CommRing R
W' : Projective 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 * P z + W'.a₄ * HPow.hPow (β := ℕ) (P z) 2) =
      0 ∧
    2 * P y * P z + W'.a₁ * P x * P z + W'.a₃ * HPow.hPow (β := ℕ) (P z) 2 = 0 ∧
      HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
          (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2) =
        0
⊢ HPow.hPow (β := ℕ) (u * P y) 2 + W'.a₁ * (u * P x) * (u * P y) + 2 * W'.a₃ * (u * P y) * (u * P z) -
          (W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 + 2 * W'.a₄ * (u * P x) * (u * P z) +
            3 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 2) +
        HPow.hPow (β := ℕ) u 2 * 0 -
      (0 +
        HPow.hPow (β := ℕ) u 2 *
          (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
            (W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 2))) =
    0

Tactic:
ring1