awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw :
  -3 * HPow.hPow (α := R) (β := ℕ) 0 2 * Q x * Q z + HMul.hMul (α := R) 3 0 * HPow.hPow (β := ℕ) (Q x) 2 * 0 +
                        HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
                      HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
                    W'.a₁ * 0 * P y * HPow.hPow (β := ℕ) (Q z) 2 -
                  W'.a₁ * Q x * Q y * HPow.hPow (α := R) (β := ℕ) 0 2 -
                W'.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) (Q z) 2 +
              W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
            W'.a₃ * P y * 0 * HPow.hPow (β := ℕ) (Q z) 2 -
          W'.a₃ * Q y * HPow.hPow (α := R) (β := ℕ) 0 2 * Q z -
        W'.a₄ * 0 * 0 * HPow.hPow (β := ℕ) (Q z) 2 +
      W'.a₄ * Q x * HPow.hPow (α := R) (β := ℕ) 0 2 * Q z =
    HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z
⊢ W'.addZ P Q = HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z

Tactic:
rw [addZ, hPz, X_eq_zero_of_Z_eq_zero hP hPz]

Premises used: WeierstrassCurve.Projective.addZ, WeierstrassCurve.Projective.X_eq_zero_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 Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -3 * HPow.hPow (α := R) (β := ℕ) 0 2 * Q x * Q z + HMul.hMul (α := R) 3 0 * HPow.hPow (β := ℕ) (Q x) 2 * 0 +
                        HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
                      HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
                    W'.a₁ * 0 * P y * HPow.hPow (β := ℕ) (Q z) 2 -
                  W'.a₁ * Q x * Q y * HPow.hPow (α := R) (β := ℕ) 0 2 -
                W'.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) (Q z) 2 +
              W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
            W'.a₃ * P y * 0 * HPow.hPow (β := ℕ) (Q z) 2 -
          W'.a₃ * Q y * HPow.hPow (α := R) (β := ℕ) 0 2 * Q z -
        W'.a₄ * 0 * 0 * HPow.hPow (β := ℕ) (Q z) 2 +
      W'.a₄ * Q x * HPow.hPow (α := R) (β := ℕ) 0 2 * Q z =
    HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z

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
hQ : W'.Equation Q
hQz : Q z = 0
rw :
  -3 * HPow.hPow (β := ℕ) (P x) 2 * 0 * 0 + 3 * P x * HPow.hPow (α := R) (β := ℕ) 0 2 * P z +
                        HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
                      HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                    W'.a₁ * P x * P y * HPow.hPow (α := R) (β := ℕ) 0 2 -
                  W'.a₁ * 0 * Q y * HPow.hPow (β := ℕ) (P z) 2 -
                W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
              W'.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₃ * P y * P z * HPow.hPow (α := R) (β := ℕ) 0 2 -
          W'.a₃ * Q y * HPow.hPow (β := ℕ) (P z) 2 * 0 -
        W'.a₄ * P x * P z * HPow.hPow (α := R) (β := ℕ) 0 2 +
      W'.a₄ * 0 * HPow.hPow (β := ℕ) (P z) 2 * 0 =
    -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P z
⊢ W'.addZ P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P z

Tactic:
rw [addZ, hQz, X_eq_zero_of_Z_eq_zero hQ hQz]

Premises used: WeierstrassCurve.Projective.addZ, WeierstrassCurve.Projective.X_eq_zero_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 Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * HPow.hPow (β := ℕ) (P x) 2 * 0 * 0 + 3 * P x * HPow.hPow (α := R) (β := ℕ) 0 2 * P z +
                        HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
                      HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                    W'.a₁ * P x * P y * HPow.hPow (α := R) (β := ℕ) 0 2 -
                  W'.a₁ * 0 * Q y * HPow.hPow (β := ℕ) (P z) 2 -
                W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
              W'.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₃ * P y * P z * HPow.hPow (α := R) (β := ℕ) 0 2 -
          W'.a₃ * Q y * HPow.hPow (β := ℕ) (P z) 2 * 0 -
        W'.a₄ * P x * P z * HPow.hPow (α := R) (β := ℕ) 0 2 +
      W'.a₄ * 0 * HPow.hPow (β := ℕ) (P z) 2 * 0 =
    -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P z

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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
apply : W'.addZ P Q * (P z * Q z) = 0
⊢ W'.addZ P Q = 0

Tactic:
apply eq_zero_of_ne_zero_of_mul_right_eq_zero <| mul_ne_zero hPz hQz

Premises used: eq_zero_of_ne_zero_of_mul_right_eq_zero, mul_ne_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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
rw : HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 = 0
rw₁ : HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 3 = 0
rw₂ : HPow.hPow (α := R) (β := ℕ) 0 3 = 0
rw₃ rw₄ : Eq.{r + 1} (α := R) 0 0
⊢ W'.addZ P Q * (P z * Q z) = 0

Tactic:
rw [addZ_eq' hP hQ, hx, sub_self, zero_pow three_ne_zero]

Premises used: sub_self, WeierstrassCurve.Projective.addZ_eq', three_ne_zero, zero_pow
-- 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
hx : P x * Q z ≠ Q x * P z
⊢ IsUnit (W.addZ P Q)

Tactic:
(addZ_ne_zero_of_X_ne hP hQ hx).isUnit

Premises used: WeierstrassCurve.Projective.addZ_ne_zero_of_X_ne, Ne.isUnit
-- 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 * Q z ≠ Q x * P z
rwa : ¬P x / P z = Q x / Q z
a b : F
rwa₁ : Type u
rwa₂ rwa₃ rwa₄ rwa₅ : ¬P x * Q z = Q x * P z
⊢ P x / P z ≠ Q x / Q z

Tactic:
rwa [ne_eq, ← X_eq_iff hPz hQz]

Premises used: ne_eq, WeierstrassCurve.Projective.X_eq_iff
-- 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 * Q z ≠ Q x * P z
⊢ W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) = (P y * Q z - Q y * P z) / (P x * Q z - Q x * P z)

Tactic:
simp [field, Affine.slope_of_X_ne <| by rwa [ne_eq, ← X_eq_iff hPz hQz]]

Premises used: WeierstrassCurve.Affine.slope_of_X_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
⊢ (-P x * HPow.hPow (β := ℕ) (Q y) 2 * P z + Q x * HPow.hPow (β := ℕ) (P y) 2 * Q z - 2 * P x * P y * Q y * Q z +
                                    2 * Q x * P y * Q y * P z -
                                  W'.a₁ * HPow.hPow (β := ℕ) (P x) 2 * Q y * Q z +
                                W'.a₁ * HPow.hPow (β := ℕ) (Q x) 2 * P y * P z +
                              W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q z -
                            W'.a₂ * P x * HPow.hPow (β := ℕ) (Q x) 2 * P z -
                          W'.a₃ * P x * P y * HPow.hPow (β := ℕ) (Q z) 2 +
                        W'.a₃ * Q x * Q y * HPow.hPow (β := ℕ) (P z) 2 -
                      2 * W'.a₃ * P x * Q y * P z * Q z +
                    2 * W'.a₃ * Q x * P y * P z * Q z +
                  W'.a₄ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
                W'.a₄ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
              3 * W'.a₆ * P x * P z * HPow.hPow (β := ℕ) (Q z) 2 -
            3 * W'.a₆ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z) *
          HPow.hPow (β := ℕ) (P z * Q z) 2 +
        ((2 * Q x * P z * HPow.hPow (β := ℕ) (Q z) 3 - P x * HPow.hPow (β := ℕ) (Q z) 4) * 0 +
          (Q x * HPow.hPow (β := ℕ) (P z) 4 - 2 * P x * HPow.hPow (β := ℕ) (P z) 3 * Q z) * 0) -
      ((HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                W'.a₂ * P z * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
              P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
            Q x * P z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2) *
          (P x * Q z - Q x * P z) +
        ((2 * Q x * P z * HPow.hPow (β := ℕ) (Q z) 3 - P x * HPow.hPow (β := ℕ) (Q z) 4) *
            (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)) +
          (Q x * HPow.hPow (β := ℕ) (P z) 4 - 2 * P x * HPow.hPow (β := ℕ) (P z) 3 * Q z) *
            (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)))) =
    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'.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 +
        ((2 * Q x * P z * HPow.hPow (β := ℕ) (Q z) 3 - P x * HPow.hPow (β := ℕ) (Q z) 4) * 0 +
          (Q x * HPow.hPow (β := ℕ) (P z) 4 - 2 * P x * HPow.hPow (β := ℕ) (P z) 3 * Q z) * 0) -
      ((HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
                W'.a₂ * P z * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
              P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
            Q x * P z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2) *
          (P x * Q z - Q x * P z) +
        ((2 * Q x * P z * HPow.hPow (β := ℕ) (Q z) 3 - P x * HPow.hPow (β := ℕ) (Q z) 4) *
            (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)) +
          (Q x * HPow.hPow (β := ℕ) (P z) 4 - 2 * P x * HPow.hPow (β := ℕ) (P z) 3 * Q z) *
            (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)))) =
    0
⊢ W'.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 =
    (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 2 * P z * Q z +
              W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
            W'.a₂ * P z * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
          P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
        Q x * P z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2) *
      (P x * Q z - Q x * P z)

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

Premises used: HMul.hMul, HSub.hSub, WeierstrassCurve.Projective.addX, HPow.hPow, 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.addX P Q = W.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 / HPow.hPow (β := ℕ) (P z * Q z) 2
rw₁ rw₂ : W.addX P Q = W.addX P Q
⊢ W.addX P Q =
    (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 2 * P z * Q z +
                W.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (P x * Q z - Q x * P z) -
              W.a₂ * P z * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
            P x * Q z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2 -
          Q x * P z * HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 2) *
        (P x * Q z - Q x * P z) /
      HPow.hPow (β := ℕ) (P z * Q z) 2

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

Premises used: pow_ne_zero, mul_div_cancel_right₀, WeierstrassCurve.Projective.addX_eq', mul_ne_zero, OfNat.ofNat
-- 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 :
  -(u * P x) * HPow.hPow (β := ℕ) (v * Q y) 2 * (u * P z) + v * Q x * HPow.hPow (β := ℕ) (u * P y) 2 * (v * Q z) -
                                2 * (u * P x) * (u * P y) * (v * Q y) * (v * Q z) +
                              2 * (v * Q x) * (u * P y) * (v * Q y) * (u * P z) -
                            W'.a₁ * HPow.hPow (β := ℕ) (u * P x) 2 * (v * Q y) * (v * Q z) +
                          W'.a₁ * HPow.hPow (β := ℕ) (v * Q x) 2 * (u * P y) * (u * P z) +
                        W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 * (v * Q x) * (v * Q z) -
                      W'.a₂ * (u * P x) * HPow.hPow (β := ℕ) (v * Q x) 2 * (u * P z) -
                    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 -
                2 * W'.a₃ * (u * P x) * (v * Q y) * (u * P z) * (v * Q z) +
              2 * W'.a₃ * (v * Q x) * (u * P y) * (u * P z) * (v * Q z) +
            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 +
        3 * W'.a₆ * (u * P x) * (u * P z) * HPow.hPow (β := ℕ) (v * Q z) 2 -
      3 * W'.a₆ * (v * Q x) * HPow.hPow (β := ℕ) (u * P z) 2 * (v * Q z) =
    HPow.hPow (β := ℕ) (u * v) 2 *
      (-P x * HPow.hPow (β := ℕ) (Q y) 2 * P z + Q x * HPow.hPow (β := ℕ) (P y) 2 * Q z - 2 * P x * P y * Q y * Q z +
                                2 * Q x * P y * Q y * P z -
                              W'.a₁ * HPow.hPow (β := ℕ) (P x) 2 * Q y * Q z +
                            W'.a₁ * HPow.hPow (β := ℕ) (Q x) 2 * P y * P z +
                          W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q z -
                        W'.a₂ * P x * HPow.hPow (β := ℕ) (Q x) 2 * P z -
                      W'.a₃ * P x * P y * HPow.hPow (β := ℕ) (Q z) 2 +
                    W'.a₃ * Q x * Q y * HPow.hPow (β := ℕ) (P z) 2 -
                  2 * W'.a₃ * P x * Q y * P z * Q z +
                2 * W'.a₃ * Q x * P y * P z * Q z +
              W'.a₄ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
            W'.a₄ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
          3 * W'.a₆ * P x * P z * HPow.hPow (β := ℕ) (Q z) 2 -
        3 * W'.a₆ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z)
⊢ W'.addX (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q

Tactic:
simp only [addX, smul_fin3_ext]

Premises used: WeierstrassCurve.Projective.addX, 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
⊢ -(u * P x) * HPow.hPow (β := ℕ) (v * Q y) 2 * (u * P z) + v * Q x * HPow.hPow (β := ℕ) (u * P y) 2 * (v * Q z) -
                                2 * (u * P x) * (u * P y) * (v * Q y) * (v * Q z) +
                              2 * (v * Q x) * (u * P y) * (v * Q y) * (u * P z) -
                            W'.a₁ * HPow.hPow (β := ℕ) (u * P x) 2 * (v * Q y) * (v * Q z) +
                          W'.a₁ * HPow.hPow (β := ℕ) (v * Q x) 2 * (u * P y) * (u * P z) +
                        W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 * (v * Q x) * (v * Q z) -
                      W'.a₂ * (u * P x) * HPow.hPow (β := ℕ) (v * Q x) 2 * (u * P z) -
                    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 -
                2 * W'.a₃ * (u * P x) * (v * Q y) * (u * P z) * (v * Q z) +
              2 * W'.a₃ * (v * Q x) * (u * P y) * (u * P z) * (v * Q z) +
            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 +
        3 * W'.a₆ * (u * P x) * (u * P z) * HPow.hPow (β := ℕ) (v * Q z) 2 -
      3 * W'.a₆ * (v * Q x) * HPow.hPow (β := ℕ) (u * P z) 2 * (v * Q z) =
    HPow.hPow (β := ℕ) (u * v) 2 *
      (-P x * HPow.hPow (β := ℕ) (Q y) 2 * P z + Q x * HPow.hPow (β := ℕ) (P y) 2 * Q z - 2 * P x * P y * Q y * Q z +
                                2 * Q x * P y * Q y * P z -
                              W'.a₁ * HPow.hPow (β := ℕ) (P x) 2 * Q y * Q z +
                            W'.a₁ * HPow.hPow (β := ℕ) (Q x) 2 * P y * P z +
                          W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q z -
                        W'.a₂ * P x * HPow.hPow (β := ℕ) (Q x) 2 * P z -
                      W'.a₃ * P x * P y * HPow.hPow (β := ℕ) (Q z) 2 +
                    W'.a₃ * Q x * Q y * HPow.hPow (β := ℕ) (P z) 2 -
                  2 * W'.a₃ * P x * Q y * P z * Q z +
                2 * W'.a₃ * Q x * P y * P z * Q z +
              W'.a₄ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
            W'.a₄ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
          3 * W'.a₆ * P x * P z * HPow.hPow (β := ℕ) (Q z) 2 -
        3 * 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 :
  -P x * HPow.hPow (β := ℕ) (P y) 2 * P z + P x * HPow.hPow (β := ℕ) (P y) 2 * P z - 2 * P x * P y * P y * P z +
                              2 * P x * P y * P y * P z -
                            W'.a₁ * HPow.hPow (β := ℕ) (P x) 2 * P y * P z +
                          W'.a₁ * HPow.hPow (β := ℕ) (P x) 2 * P y * P z +
                        W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P x * P z -
                      W'.a₂ * P x * HPow.hPow (β := ℕ) (P x) 2 * P z -
                    W'.a₃ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 +
                  W'.a₃ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 -
                2 * W'.a₃ * P x * P y * P z * P z +
              2 * W'.a₃ * P x * P y * P z * P z +
            W'.a₄ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
          W'.a₄ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
        3 * W'.a₆ * P x * P z * HPow.hPow (β := ℕ) (P z) 2 -
      3 * W'.a₆ * P x * HPow.hPow (β := ℕ) (P z) 2 * P z =
    0
⊢ W'.addX P P = 0

Tactic:
rw [addX]

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

Tactic:
rw [addX, hPz, X_eq_zero_of_Z_eq_zero hP hPz]

Premises used: WeierstrassCurve.Projective.addX, WeierstrassCurve.Projective.X_eq_zero_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 Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -0 * HPow.hPow (β := ℕ) (Q y) 2 * 0 + Q x * HPow.hPow (β := ℕ) (P y) 2 * Q z -
                                HMul.hMul (α := R) 2 0 * P y * Q y * Q z +
                              2 * Q x * P y * Q y * 0 -
                            W'.a₁ * HPow.hPow (α := R) (β := ℕ) 0 2 * Q y * Q z +
                          W'.a₁ * HPow.hPow (β := ℕ) (Q x) 2 * P y * 0 +
                        W'.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 * Q x * Q z -
                      W'.a₂ * 0 * HPow.hPow (β := ℕ) (Q x) 2 * 0 -
                    W'.a₃ * 0 * P y * HPow.hPow (β := ℕ) (Q z) 2 +
                  W'.a₃ * Q x * Q y * HPow.hPow (α := R) (β := ℕ) 0 2 -
                2 * W'.a₃ * 0 * Q y * 0 * Q z +
              2 * W'.a₃ * Q x * P y * 0 * Q z +
            W'.a₄ * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) (Q z) 2 -
          W'.a₄ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
        3 * W'.a₆ * 0 * 0 * HPow.hPow (β := ℕ) (Q z) 2 -
      3 * W'.a₆ * Q x * HPow.hPow (α := R) (β := ℕ) 0 2 * Q z =
    HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x

Tactic:
ring1