awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x / P z = Q x / Q z
hy : ¬P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z)
⊢ (3 * HPow.hPow (β := ℕ) (P x / P z) 2 + 2 * W.toAffine.a₂ * (P x / P z) + W.toAffine.a₄ -
        W.toAffine.a₁ * (P y / P z)) /
      (P y / P z - W.negY P / P z) =
    HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (P z) / (P y - W.negY P)

Tactic:
simp [field, eval_polynomialX]

Premises used: WeierstrassCurve.Projective.eval_polynomialX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
a :
  W'.dblX P * P z + 9 * (W'.a₁ * HPow.hPow (β := ℕ) (P x) 2 + 2 * P x * P y) * 0 -
      ((HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 2 -
                HMul.hMul (β := R) W'.a₁ ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) * P z *
                  (P y - W'.negY P) -
              W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
            2 * P x * P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 2) *
          (P y - W'.negY P) +
        9 * (W'.a₁ * HPow.hPow (β := ℕ) (P x) 2 + 2 * P x * P y) *
          (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))) =
    0
⊢ W'.dblX P * P z =
    (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 2 -
            HMul.hMul (β := R) W'.a₁ ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) * P z *
              (P y - W'.negY P) -
          W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
        2 * P x * P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 2) *
      (P y - W'.negY P)

Tactic:
linear_combination (norm := (rw [dblX, eval_polynomialX, negY]; ring1))
    9 * (W'.a₁ * P x ^ 2 + 2 * P x * P y) * (equation_iff _).mp hP

Premises used: WeierstrassCurve.Projective.negY, HMul.hMul, WeierstrassCurve.Projective.eval_polynomialX, WeierstrassCurve.Projective.dblX, HPow.hPow, HAdd.hAdd, Iff.mp, OfNat.ofNat, WeierstrassCurve.Projective.equation_iff, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
rw : W.dblX P = W.dblX P * P z / P z
rw₁ rw₂ : W.dblX P = W.dblX P
⊢ W.dblX P =
    (HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
              HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * P z *
                (P y - W.negY P) -
            W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
          2 * P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) *
        (P y - W.negY P) /
      P z

Tactic:
rw [← dblX_eq' hP, mul_div_cancel_right₀ _ hPz]

Premises used: mul_div_cancel_right₀, WeierstrassCurve.Projective.dblX_eq'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
apply : W'.dblX P * P z = 0
⊢ W'.dblX P = 0

Tactic:
apply eq_zero_of_ne_zero_of_mul_right_eq_zero hPz

Premises used: eq_zero_of_ne_zero_of_mul_right_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
rw :
  (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 2 -
            HMul.hMul (β := R) W'.a₁ ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) * P z *
              (W'.negY P - W'.negY P) -
          W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2 -
        2 * P x * P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2) *
      (W'.negY P - W'.negY P) =
    0
⊢ W'.dblX P * P z = 0

Tactic:
rw [dblX_eq' hP, Y_eq_negY_of_Y_eq hQz hx hy hy']

Premises used: WeierstrassCurve.Projective.Y_eq_negY_of_Y_eq, WeierstrassCurve.Projective.dblX_eq'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 2 -
            HMul.hMul (β := R) W'.a₁ ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) * P z *
              (W'.negY P - W'.negY P) -
          W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2 -
        2 * P x * P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2) *
      (W'.negY P - W'.negY P) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
simp :
  n * (n + -(P z * d * W.toAffine.a₁)) - HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 * W.toAffine.a₂ -
        P z * HPow.hPow (β := ℕ) d 2 * P x -
      P z * HPow.hPow (β := ℕ) d 2 * P x =
    n * (n - P z * d * W.toAffine.a₁) - HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 * W.toAffine.a₂ -
      P z * HPow.hPow (β := ℕ) d 2 * P x * 2
⊢ W.toAffine.addX (P x / P z) (P x / P z) (-n / P z / d) =
    (HPow.hPow (β := ℕ) n 2 - W.a₁ * n * P z * d - W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 -
            2 * P x * P z * HPow.hPow (β := ℕ) d 2) *
          d /
        P z /
      (P z * HPow.hPow (β := ℕ) d 3)

Tactic:
simp [field]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ n * (n + -(P z * d * W.toAffine.a₁)) - HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 * W.toAffine.a₂ -
        P z * HPow.hPow (β := ℕ) d 2 * P x -
      P z * HPow.hPow (β := ℕ) d 2 * P x =
    n * (n - P z * d * W.toAffine.a₁) - HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 * W.toAffine.a₂ -
      P z * HPow.hPow (β := ℕ) d 2 * P x * 2

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
a :
  W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 +
        -9 *
            (HPow.hPow (β := ℕ) (P y) 2 * P z + 2 * W'.a₁ * P x * P y * P z - 3 * HPow.hPow (β := ℕ) (P x) 3 -
              3 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z) *
          0 -
      (HMul.hMul (α := R) (-(eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R)
            (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 2 -
                    HMul.hMul (β := R) W'.a₁ ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) * P z *
                      (P y - W'.negY P) -
                  W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
                2 * P x * P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
              P x * P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 2) +
          P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 +
        -9 *
            (HPow.hPow (β := ℕ) (P y) 2 * P z + 2 * W'.a₁ * P x * P y * P z - 3 * HPow.hPow (β := ℕ) (P x) 3 -
              3 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z) *
          (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))) =
    0
⊢ W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 =
    HMul.hMul (α := R) (-(eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R)
        (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 2 -
                HMul.hMul (β := R) W'.a₁ ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) * P z *
                  (P y - W'.negY P) -
              W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
            2 * P x * P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
          P x * P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 2) +
      P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 3

Tactic:
linear_combination (norm := (rw [negDblY, eval_polynomialX, negY]; ring1))
    -9 * (P y ^ 2 * P z + 2 * W'.a₁ * P x * P y * P z - 3 * P x ^ 3 - 3 * W'.a₂ * P x ^ 2 * P z)
      * (equation_iff _).mp hP

Premises used: WeierstrassCurve.Projective.negY, HMul.hMul, WeierstrassCurve.Projective.eval_polynomialX, HSub.hSub, WeierstrassCurve.Projective.negDblY, WeierstrassCurve.a₂, HPow.hPow, HAdd.hAdd, Iff.mp, OfNat.ofNat, WeierstrassCurve.Projective.equation_iff, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
rw : W.negDblY P = W.negDblY P * HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2
rw₁ rw₂ : W.negDblY P = W.negDblY P
⊢ W.negDblY P =
    (HMul.hMul (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F)
          (HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                  HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * P z *
                    (P y - W.negY P) -
                W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
              2 * P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (P z) 2

Tactic:
rw [← negDblY_eq' hP, mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]

Premises used: pow_ne_zero, mul_div_cancel_right₀, WeierstrassCurve.Projective.negDblY_eq', OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
rw :
  HMul.hMul (α := R) (-(eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R)
        (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 2 -
                HMul.hMul (β := R) W'.a₁ ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) * P z *
                  (W'.negY P - W'.negY P) -
              W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2 -
            2 * P x * P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2 -
          P x * P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2) +
      W'.negY P * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 3 =
    -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3
⊢ W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 =
    -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3

Tactic:
rw [negDblY_eq' hP, Y_eq_negY_of_Y_eq hQz hx hy hy']

Premises used: WeierstrassCurve.Projective.Y_eq_negY_of_Y_eq, WeierstrassCurve.Projective.negDblY_eq'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ HMul.hMul (α := R) (-(eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R)
        (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 2 -
                HMul.hMul (β := R) W'.a₁ ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) * P z *
                  (W'.negY P - W'.negY P) -
              W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2 -
            2 * P x * P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2 -
          P x * P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2) +
      W'.negY P * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 3 =
    -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
rw :
  W.negDblY P =
    -(HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
        HPow.hPow (β := ℕ) (P z) 2)
rw₁ :
  W.negDblY P =
    -HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
      HPow.hPow (β := ℕ) (P z) 2
rw₂ : W.negDblY P = W.negDblY P * HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2
rw₃ rw₄ : W.negDblY P = W.negDblY P
⊢ W.negDblY P = -W.dblU P

Tactic:
rw [dblU, ← neg_div, ← negDblY_of_Y_eq' hP hQz hx hy hy',
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]

Premises used: neg_div, WeierstrassCurve.Projective.dblU, pow_ne_zero, mul_div_cancel_right₀, OfNat.ofNat, WeierstrassCurve.Projective.negDblY_of_Y_eq'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
rw :
  -n / P z / d *
        ((HPow.hPow (β := ℕ) n 2 - W.a₁ * n * P z * d - W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 -
                  2 * P x * P z * HPow.hPow (β := ℕ) d 2) *
                d /
              P z /
            (P z * HPow.hPow (β := ℕ) d 3) -
          P x / P z) +
      P y / P z =
    (-n *
            (HPow.hPow (β := ℕ) n 2 - W.a₁ * n * P z * d - W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 -
                2 * P x * P z * HPow.hPow (β := ℕ) d 2 -
              P x * P z * HPow.hPow (β := ℕ) d 2) +
          P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 3) /
        HPow.hPow (β := ℕ) (P z) 2 /
      (P z * HPow.hPow (β := ℕ) d 3)
⊢ W.toAffine.negAddY (P x / P z) (P x / P z) (P y / P z) (-n / P z / d) =
    (-n *
            (HPow.hPow (β := ℕ) n 2 - W.a₁ * n * P z * d - W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 -
                2 * P x * P z * HPow.hPow (β := ℕ) d 2 -
              P x * P z * HPow.hPow (β := ℕ) d 2) +
          P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 3) /
        HPow.hPow (β := ℕ) (P z) 2 /
      (P z * HPow.hPow (β := ℕ) d 3)

Tactic:
rw [Affine.negAddY, toAffine_addX_of_eq hPz hd]

Premises used: _private.0.WeierstrassCurve.Projective.toAffine_addX_of_eq, WeierstrassCurve.Affine.negAddY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ -n / P z / d *
        ((HPow.hPow (β := ℕ) n 2 - W.a₁ * n * P z * d - W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 -
                  2 * P x * P z * HPow.hPow (β := ℕ) d 2) *
                d /
              P z /
            (P z * HPow.hPow (β := ℕ) d 3) -
          P x / P z) +
      P y / P z =
    (-n *
            (HPow.hPow (β := ℕ) n 2 - W.a₁ * n * P z * d - W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 -
                2 * P x * P z * HPow.hPow (β := ℕ) d 2 -
              P x * P z * HPow.hPow (β := ℕ) d 2) +
          P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 3) /
        HPow.hPow (β := ℕ) (P z) 2 /
      (P z * HPow.hPow (β := ℕ) d 3)

Tactic:
simp [field]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
simp :
  -(HPow.hPow (β := ℕ) u 4 * W'.negDblY P) - W'.a₁ * (HPow.hPow (β := ℕ) u 4 * W'.dblX P) -
      W'.a₃ * (HPow.hPow (β := ℕ) u 4 * W'.dblZ P) =
    HPow.hPow (β := ℕ) u 4 * (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P)
⊢ W'.dblY (u • P) = HPow.hPow (β := ℕ) u 4 * W'.dblY P

Tactic:
simp only [dblY, negY_eq, negDblY_smul, dblX_smul, dblZ_smul]

Premises used: WeierstrassCurve.Projective.negY_eq, WeierstrassCurve.Projective.dblY, WeierstrassCurve.Projective.dblX_smul, WeierstrassCurve.Projective.negDblY_smul, WeierstrassCurve.Projective.dblZ_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ -(HPow.hPow (β := ℕ) u 4 * W'.negDblY P) - W'.a₁ * (HPow.hPow (β := ℕ) u 4 * W'.dblX P) -
      W'.a₃ * (HPow.hPow (β := ℕ) u 4 * W'.dblZ P) =
    HPow.hPow (β := ℕ) u 4 * (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : - -HPow.hPow (β := ℕ) (P y) 4 - W'.a₁ * 0 - W'.a₃ * 0 = HPow.hPow (β := ℕ) (P y) 4
⊢ W'.dblY P = HPow.hPow (β := ℕ) (P y) 4

Tactic:
rw [dblY, negY_eq, negDblY_of_Z_eq_zero hP hPz, dblX_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz]

Premises used: WeierstrassCurve.Projective.negY_eq, WeierstrassCurve.Projective.dblY, WeierstrassCurve.Projective.dblZ_of_Z_eq_zero, WeierstrassCurve.Projective.negDblY_of_Z_eq_zero, WeierstrassCurve.Projective.dblX_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ - -HPow.hPow (β := ℕ) (P y) 4 - W'.a₁ * 0 - W'.a₃ * 0 = HPow.hPow (β := ℕ) (P y) 4

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
a :
  (-W'.negDblY P - W'.a₁ * 0 - W'.a₃ * 0) * HPow.hPow (β := ℕ) (P z) 2 + W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3 +
        -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3) =
    0
⊢ W'.dblY P * HPow.hPow (β := ℕ) (P z) 2 + W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3 +
        -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3) =
    0

Tactic:
rw [dblY, negY_eq, dblX_of_Y_eq hP hPz hQz hx hy hy',
    dblZ_of_Y_eq hQz hx hy hy']

Premises used: WeierstrassCurve.Projective.negY_eq, WeierstrassCurve.Projective.dblY, WeierstrassCurve.Projective.dblZ_of_Y_eq, WeierstrassCurve.Projective.dblX_of_Y_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ (-W'.negDblY P - W'.a₁ * 0 - W'.a₃ * 0) * HPow.hPow (β := ℕ) (P z) 2 + W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3 +
        -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
a :
  W'.dblY P * HPow.hPow (β := ℕ) (P z) 2 + W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3 +
        -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3) =
    0
⊢ W'.dblY P * HPow.hPow (β := ℕ) (P z) 2 =
    HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3

Tactic:
linear_combination (norm := (rw [dblY, negY_eq, dblX_of_Y_eq hP hPz hQz hx hy hy',
    dblZ_of_Y_eq hQz hx hy hy']; ring1)) -negDblY_of_Y_eq' hP hQz hx hy hy'

Premises used: WeierstrassCurve.Projective.negY_eq, WeierstrassCurve.Projective.dblY, WeierstrassCurve.Projective.dblZ_of_Y_eq, WeierstrassCurve.Projective.dblX_of_Y_eq, WeierstrassCurve.Projective.negDblY_of_Y_eq'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
rw :
  W.dblY P =
    HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
      HPow.hPow (β := ℕ) (P z) 2
rw₁ : W.dblY P = W.dblY P * HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2
rw₂ rw₃ : W.dblY P = W.dblY P
⊢ W.dblY P = W.dblU P

Tactic:
rw [dblU, ← dblY_of_Y_eq' hP hPz hQz hx hy hy', mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]

Premises used: WeierstrassCurve.Projective.dblU, pow_ne_zero, mul_div_cancel_right₀, OfNat.ofNat, WeierstrassCurve.Projective.dblY_of_Y_eq'