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
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
erw :
  W.negY ![W.dblX P, W.negDblY P, W.dblZ P] / W.dblZ P =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
erw₁ :
  W.toAffine.negY (![W.dblX P, W.negDblY P, W.dblZ P] x / ![W.dblX P, W.negDblY P, W.dblZ P] z)
      (![W.dblX P, W.negDblY P, W.dblZ P] y / ![W.dblX P, W.negDblY P, W.dblZ P] z) =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
erw₂ :
  W.toAffine.negY
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (![W.dblX P, W.negDblY P, W.dblZ P] y / ![W.dblX P, W.negDblY P, W.dblZ P] z) =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
erw₃ :
  W.toAffine.negY
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))) =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
erw₄ erw₅ :
  W.toAffine.negY
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))) =
    W.toAffine.negY
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
⊢ W.dblY P / W.dblZ P =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hQz hx hy,
    dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, negDblY_of_Z_ne_zero hP hQ hPz hQz hx hy, Affine.addY]

Premises used: WeierstrassCurve.Projective.dblY, WeierstrassCurve.Projective.negY_of_Z_ne_zero, WeierstrassCurve.Projective.negDblY_of_Z_ne_zero, WeierstrassCurve.Affine.addY, WeierstrassCurve.Projective.dblX_of_Z_ne_zero, WeierstrassCurve.Projective.dblZ_ne_zero_of_Y_ne'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.dblXYZ P x = W'.dblX P

Tactic:
rfl

Premises used: Eq.mpr, WeierstrassCurve.Projective.dblXYZ, Fin.cons, WeierstrassCurve.Projective.dblX, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.dblXYZ P y = W'.dblY P

Tactic:
rfl

Premises used: WeierstrassCurve.Projective.negY, Eq.mpr, WeierstrassCurve.Projective.dblY, WeierstrassCurve.Projective.dblXYZ, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.dblXYZ P z = W'.dblZ P

Tactic:
rfl

Premises used: Eq.mpr, WeierstrassCurve.Projective.dblXYZ, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, WeierstrassCurve.Projective.dblZ, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
rw : ![W'.dblX (u • P), W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₁ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₂ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, W'.dblZ (u • P)] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₃ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₄ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P x, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P y,
      HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
rw₅ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P y,
      HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
rw₆ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
rw₇ rw₈ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P]
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P

Tactic:
rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]

Premises used: WeierstrassCurve.Projective.dblXYZ, WeierstrassCurve.Projective.dblX_smul, WeierstrassCurve.Projective.dblXYZ_Z, WeierstrassCurve.Projective.smul_fin3, WeierstrassCurve.Projective.dblY_smul, WeierstrassCurve.Projective.dblXYZ_X, WeierstrassCurve.Projective.dblXYZ_Y, WeierstrassCurve.Projective.dblZ_smul
-- 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
erw :
  ![W'.dblX P, W'.dblY P, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₁ :
  ![0, W'.dblY P, W'.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₂ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₃ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, 0] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₄ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, 0] =
    ![HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] x, HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] y,
      HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] z]
erw₅ : ![0, HPow.hPow (β := ℕ) (P y) 4, 0] = ![0, HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] y, 0]
erw₆ erw₇ : ![0, HPow.hPow (β := ℕ) (P y) 4, 0] = ![0, HPow.hPow (β := ℕ) (P y) 4, 0]
⊢ W'.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]

Tactic:
erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, smul_fin3,
    mul_zero, mul_one]

Premises used: WeierstrassCurve.Projective.dblXYZ, WeierstrassCurve.Projective.dblZ_of_Z_eq_zero, MulZeroClass.mul_zero, WeierstrassCurve.Projective.smul_fin3, WeierstrassCurve.Projective.dblX_of_Z_eq_zero, WeierstrassCurve.Projective.dblY_of_Z_eq_zero, mul_one
-- 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
erw : ![W.dblX P, W.dblY P, W.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₁ : ![0, W.dblY P, W.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₂ : ![0, W.dblU P, W.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₃ : ![0, W.dblU P, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₄ : ![0, W.dblU P, 0] = ![W.dblU P * ![0, 1, 0] x, W.dblU P * ![0, 1, 0] y, W.dblU P * ![0, 1, 0] z]
erw₅ : ![0, W.dblU P, 0] = ![0, W.dblU P * ![0, 1, 0] y, 0]
erw₆ erw₇ : ![0, W.dblU P, 0] = ![0, W.dblU P, 0]
⊢ W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]

Tactic:
erw [dblXYZ, dblX_of_Y_eq hP hPz hQz hx hy hy', dblY_of_Y_eq hP hPz hQz hx hy hy',
    dblZ_of_Y_eq hQz hx hy hy', smul_fin3, mul_zero, mul_one]

Premises used: WeierstrassCurve.Projective.dblXYZ, MulZeroClass.mul_zero, WeierstrassCurve.Projective.smul_fin3, WeierstrassCurve.Projective.dblZ_of_Y_eq, WeierstrassCurve.Projective.dblX_of_Y_eq, mul_one, WeierstrassCurve.Projective.dblY_of_Y_eq
-- 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
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ IsUnit (W.dblZ P)

Tactic:
have hZ : IsUnit <| W.dblZ P := isUnit_dblZ_of_Y_ne' hP hQ hPz hQz hx hy
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
u v : F
⊢ addU (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 * addU P Q

Tactic:
simp [field, addU]

Premises used: WeierstrassCurve.Projective.addU
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z = 0
rw : -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z) = 0
rw₁ : -HPow.hPow (β := ℕ) (P y * Q z - Q y * 0) 3 / (0 * Q z) = 0
rw₂ : -HPow.hPow (β := ℕ) (P y * Q z - Q y * 0) 3 / 0 = 0
rw₃ rw₄ : Eq.{u + 1} (α := F) 0 0
⊢ addU P Q = 0

Tactic:
rw [addU, hPz, zero_mul, div_zero]

Premises used: MulZeroClass.zero_mul, WeierstrassCurve.Projective.addU, div_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hQz : Q z = 0
rw : -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z) = 0
rw₁ : -HPow.hPow (β := ℕ) (P y * 0 - Q y * P z) 3 / (P z * 0) = 0
rw₂ : -HPow.hPow (β := ℕ) (P y * 0 - Q y * P z) 3 / 0 = 0
rw₃ rw₄ : Eq.{u + 1} (α := F) 0 0
⊢ addU P Q = 0

Tactic:
rw [addU, hQz, mul_zero <| P z, div_zero]

Premises used: MulZeroClass.mul_zero, WeierstrassCurve.Projective.addU, OfNat.ofNat, div_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hy : P y * Q z ≠ Q y * P z
⊢ addU P Q ≠ 0

Tactic:
div_ne_zero (neg_ne_zero.mpr <| pow_ne_zero 3 <| sub_ne_zero.mpr hy) <| mul_ne_zero hPz hQz

Premises used: Iff.mpr, sub_ne_zero, pow_ne_zero, div_ne_zero, WeierstrassCurve.Projective.addU, neg_ne_zero, mul_ne_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hy : P y * Q z ≠ Q y * P z
⊢ IsUnit (addU P Q)

Tactic:
(addU_ne_zero_of_Y_ne hPz hQz hy).isUnit

Premises used: Ne.isUnit, WeierstrassCurve.Projective.addU_ne_zero_of_Y_ne
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
a :
  (-3 * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q z + 3 * P x * HPow.hPow (β := ℕ) (Q x) 2 * P z +
                              HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
                            HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                          W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (Q z) 2 -
                        W'.a₁ * Q x * Q y * HPow.hPow (β := ℕ) (P z) 2 -
                      W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                    W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                  W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (Q z) 2 -
                W'.a₃ * Q y * HPow.hPow (β := ℕ) (P z) 2 * Q z -
              W'.a₄ * P x * P z * HPow.hPow (β := ℕ) (Q z) 2 +
            W'.a₄ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z) *
          (P z * Q z) +
        (HPow.hPow (β := ℕ) (Q z) 3 * 0 +
          HPow.hPow (β := ℕ) (P z) 3 *
            (HPow.hPow (β := ℕ) (Q y) 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * HPow.hPow (β := ℕ) (Q z) 2 -
              (HPow.hPow (β := ℕ) (Q x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * Q z +
                  W'.a₄ * Q x * HPow.hPow (β := ℕ) (Q z) 2 +
                W'.a₆ * HPow.hPow (β := ℕ) (Q z) 3))) -
      (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 +
        (HPow.hPow (β := ℕ) (Q z) 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)) +
          HPow.hPow (β := ℕ) (P z) 3 * 0)) =
    0
⊢ W'.addZ P Q * (P z * Q z) +
        (HPow.hPow (β := ℕ) (Q z) 3 * 0 +
          HPow.hPow (β := ℕ) (P z) 3 *
            (HPow.hPow (β := ℕ) (Q y) 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * HPow.hPow (β := ℕ) (Q z) 2 -
              (HPow.hPow (β := ℕ) (Q x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * Q z +
                  W'.a₄ * Q x * HPow.hPow (β := ℕ) (Q z) 2 +
                W'.a₆ * HPow.hPow (β := ℕ) (Q z) 3))) -
      (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 +
        (HPow.hPow (β := ℕ) (Q z) 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)) +
          HPow.hPow (β := ℕ) (P z) 3 * 0)) =
    0

Tactic:
rw [addZ]

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

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

Tactic:
linear_combination (norm := (rw [addZ]; ring1))
    Q z ^ 3 * (equation_iff _).mp hP - P z ^ 3 * (equation_iff _).mp hQ

Premises used: WeierstrassCurve.Projective.addZ, Iff.mp, OfNat.ofNat, WeierstrassCurve.Projective.equation_iff
-- 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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
rw : W.addZ P Q = W.addZ P Q * (P z * Q z) / (P z * Q z)
rw₁ rw₂ : W.addZ P Q = W.addZ P Q
⊢ W.addZ P Q = HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 / (P z * Q z)

Tactic:
rw [← addZ_eq' hP hQ, mul_div_cancel_right₀ _ <| mul_ne_zero hPz hQz]

Premises used: WeierstrassCurve.Projective.addZ_eq', mul_div_cancel_right₀, mul_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
simp :
  -3 * HPow.hPow (β := ℕ) (u * P x) 2 * (v * Q x) * (v * Q z) +
                          3 * (u * P x) * HPow.hPow (β := ℕ) (v * Q x) 2 * (u * P z) +
                        HPow.hPow (β := ℕ) (u * P y) 2 * HPow.hPow (β := ℕ) (v * Q z) 2 -
                      HPow.hPow (β := ℕ) (v * Q y) 2 * HPow.hPow (β := ℕ) (u * P z) 2 +
                    W'.a₁ * (u * P x) * (u * P y) * HPow.hPow (β := ℕ) (v * Q z) 2 -
                  W'.a₁ * (v * Q x) * (v * Q y) * HPow.hPow (β := ℕ) (u * P z) 2 -
                W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 * HPow.hPow (β := ℕ) (v * Q z) 2 +
              W'.a₂ * HPow.hPow (β := ℕ) (v * Q x) 2 * HPow.hPow (β := ℕ) (u * P z) 2 +
            W'.a₃ * (u * P y) * (u * P z) * HPow.hPow (β := ℕ) (v * Q z) 2 -
          W'.a₃ * (v * Q y) * HPow.hPow (β := ℕ) (u * P z) 2 * (v * Q z) -
        W'.a₄ * (u * P x) * (u * P z) * HPow.hPow (β := ℕ) (v * Q z) 2 +
      W'.a₄ * (v * Q x) * HPow.hPow (β := ℕ) (u * P z) 2 * (v * Q z) =
    HPow.hPow (β := ℕ) (u * v) 2 *
      (-3 * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q z + 3 * P x * HPow.hPow (β := ℕ) (Q x) 2 * P z +
                          HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
                        HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                      W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (Q z) 2 -
                    W'.a₁ * Q x * Q y * HPow.hPow (β := ℕ) (P z) 2 -
                  W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (Q z) 2 -
            W'.a₃ * Q y * HPow.hPow (β := ℕ) (P z) 2 * Q z -
          W'.a₄ * P x * P z * HPow.hPow (β := ℕ) (Q z) 2 +
        W'.a₄ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z)
⊢ W'.addZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q

Tactic:
simp only [addZ, smul_fin3_ext]

Premises used: WeierstrassCurve.Projective.addZ, WeierstrassCurve.Projective.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -3 * HPow.hPow (β := ℕ) (u * P x) 2 * (v * Q x) * (v * Q z) +
                          3 * (u * P x) * HPow.hPow (β := ℕ) (v * Q x) 2 * (u * P z) +
                        HPow.hPow (β := ℕ) (u * P y) 2 * HPow.hPow (β := ℕ) (v * Q z) 2 -
                      HPow.hPow (β := ℕ) (v * Q y) 2 * HPow.hPow (β := ℕ) (u * P z) 2 +
                    W'.a₁ * (u * P x) * (u * P y) * HPow.hPow (β := ℕ) (v * Q z) 2 -
                  W'.a₁ * (v * Q x) * (v * Q y) * HPow.hPow (β := ℕ) (u * P z) 2 -
                W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 * HPow.hPow (β := ℕ) (v * Q z) 2 +
              W'.a₂ * HPow.hPow (β := ℕ) (v * Q x) 2 * HPow.hPow (β := ℕ) (u * P z) 2 +
            W'.a₃ * (u * P y) * (u * P z) * HPow.hPow (β := ℕ) (v * Q z) 2 -
          W'.a₃ * (v * Q y) * HPow.hPow (β := ℕ) (u * P z) 2 * (v * Q z) -
        W'.a₄ * (u * P x) * (u * P z) * HPow.hPow (β := ℕ) (v * Q z) 2 +
      W'.a₄ * (v * Q x) * HPow.hPow (β := ℕ) (u * P z) 2 * (v * Q z) =
    HPow.hPow (β := ℕ) (u * v) 2 *
      (-3 * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q z + 3 * P x * HPow.hPow (β := ℕ) (Q x) 2 * P z +
                          HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
                        HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                      W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (Q z) 2 -
                    W'.a₁ * Q x * Q y * HPow.hPow (β := ℕ) (P z) 2 -
                  W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (Q z) 2 -
            W'.a₃ * Q y * HPow.hPow (β := ℕ) (P z) 2 * Q z -
          W'.a₄ * P x * P z * HPow.hPow (β := ℕ) (Q z) 2 +
        W'.a₄ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
rw :
  -3 * HPow.hPow (β := ℕ) (P x) 2 * P x * P z + 3 * P x * HPow.hPow (β := ℕ) (P x) 2 * P z +
                        HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                      HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                    W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 -
                  W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 -
                W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (P z) 2 -
          W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 * P z -
        W'.a₄ * P x * P z * HPow.hPow (β := ℕ) (P z) 2 +
      W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * P z =
    0
⊢ W'.addZ P P = 0

Tactic:
rw [addZ]

Premises used: WeierstrassCurve.Projective.addZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * HPow.hPow (β := ℕ) (P x) 2 * P x * P z + 3 * P x * HPow.hPow (β := ℕ) (P x) 2 * P z +
                        HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                      HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                    W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 -
                  W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 -
                W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (P z) 2 -
          W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 * P z -
        W'.a₄ * P x * P z * HPow.hPow (β := ℕ) (P z) 2 +
      W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * P z =
    0

Tactic:
ring1