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
⊢ -3 * HPow.hPow (α := R) (β := ℕ) 0 2 * Q x * Q y + HMul.hMul (α := R) 3 0 * HPow.hPow (β := ℕ) (Q x) 2 * P y -
                                    HPow.hPow (β := ℕ) (P y) 2 * Q y * Q z +
                                  P y * HPow.hPow (β := ℕ) (Q y) 2 * 0 +
                                W'.a₁ * 0 * HPow.hPow (β := ℕ) (Q y) 2 * 0 -
                              W'.a₁ * Q x * HPow.hPow (β := ℕ) (P y) 2 * Q z -
                            W'.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 * Q y * Q z +
                          W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * P y * 0 +
                        2 * W'.a₂ * 0 * Q x * P y * Q z -
                      2 * W'.a₂ * 0 * Q x * Q y * 0 -
                    W'.a₃ * HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                  W'.a₃ * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
                W'.a₄ * 0 * P y * HPow.hPow (β := ℕ) (Q z) 2 -
              2 * W'.a₄ * 0 * Q y * 0 * Q z +
            2 * W'.a₄ * Q x * P y * 0 * Q z -
          W'.a₄ * Q x * Q y * HPow.hPow (α := R) (β := ℕ) 0 2 +
        3 * W'.a₆ * P y * 0 * HPow.hPow (β := ℕ) (Q z) 2 -
      3 * W'.a₆ * Q y * HPow.hPow (α := R) (β := ℕ) 0 2 * Q z =
    HPow.hPow (β := ℕ) (P y) 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * 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 * Q y + 3 * P x * HPow.hPow (α := R) (β := ℕ) 0 2 * P y -
                                    HPow.hPow (β := ℕ) (P y) 2 * Q y * 0 +
                                  P y * HPow.hPow (β := ℕ) (Q y) 2 * P z +
                                W'.a₁ * P x * HPow.hPow (β := ℕ) (Q y) 2 * P z -
                              W'.a₁ * 0 * HPow.hPow (β := ℕ) (P y) 2 * 0 -
                            W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * Q y * 0 +
                          W'.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 * P y * P z +
                        2 * W'.a₂ * P x * 0 * P y * 0 -
                      2 * W'.a₂ * P x * 0 * Q y * P z -
                    W'.a₃ * HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
                  W'.a₃ * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₄ * P x * P y * HPow.hPow (α := R) (β := ℕ) 0 2 -
              2 * W'.a₄ * P x * Q y * P z * 0 +
            2 * W'.a₄ * 0 * P y * P z * 0 -
          W'.a₄ * 0 * Q y * HPow.hPow (β := ℕ) (P z) 2 +
        3 * W'.a₆ * P y * P z * HPow.hPow (α := R) (β := ℕ) 0 2 -
      3 * W'.a₆ * Q y * HPow.hPow (β := ℕ) (P z) 2 * 0 =
    -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)
⊢ W'.negAddY P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * W'.negY P

Tactic:
rw [negAddY, hQz, X_eq_zero_of_Z_eq_zero hQ hQz, negY]

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

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
hx : P x * Q z = Q x * P z
rw :
  (P y * Q z - Q y * P z) *
        (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 * (Q x * P z - Q x * P z) -
                W'.a₂ * P z * Q z * HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 2 -
              Q x * P z * HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 2 -
            Q x * P z * HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 2 -
          Q x * P z * HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 2) +
      P y * Q z * HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 3 =
    HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * (P z * Q z)
⊢ W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 = HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * (P z * Q z)

Tactic:
rw [negAddY_eq' hP hQ, hx]

Premises used: WeierstrassCurve.Projective.negAddY_eq'
-- 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
hx : P x * Q z = Q x * P z
⊢ (P y * Q z - Q y * P z) *
        (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 * (Q x * P z - Q x * P z) -
                W'.a₂ * P z * Q z * HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 2 -
              Q x * P z * HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 2 -
            Q x * P z * HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 2 -
          Q x * P z * HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 2) +
      P y * Q z * HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 3 =
    HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * (P z * Q z)

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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
rw : W.negAddY P Q = -(-HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z))
rw₁ : W.negAddY P Q = - -(HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z))
rw₂ : W.negAddY P Q = HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z)
rw₃ : W.negAddY P Q = HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * (P z * Q z) / (P z * Q z * (P z * Q z))
rw₄ : W.negAddY P Q = W.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 / (P z * Q z * (P z * Q z))
rw₅ : W.negAddY P Q = W.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 / HPow.hPow (β := ℕ) (P z * Q z) 2
rw₆ rw₇ : W.negAddY P Q = W.negAddY P Q
⊢ W.negAddY P Q = -addU P Q

Tactic:
rw [addU, neg_div, neg_neg, ← mul_div_mul_right _ _ <| mul_ne_zero hPz hQz,
    ← negAddY_of_X_eq' hP hQ hx, ← sq,
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]

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

Tactic:
rw [Affine.negAddY, toAffine_addX_of_ne hPz hQz hd]

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

Tactic:
simp [field]
-- 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 :
  -(HPow.hPow (β := ℕ) (u * v) 2 * W'.negAddY P Q) - W'.a₁ * (HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q) -
      W'.a₃ * (HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q) =
    HPow.hPow (β := ℕ) (u * v) 2 * (-W'.negAddY P Q - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q)
⊢ W'.addY (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q

Tactic:
simp only [addY, negY_eq, negAddY_smul, addX_smul, addZ_smul]

Premises used: WeierstrassCurve.Projective.negY_eq, WeierstrassCurve.Projective.addX_smul, WeierstrassCurve.Projective.negAddY_smul, WeierstrassCurve.Projective.addZ_smul, WeierstrassCurve.Projective.addY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ -(HPow.hPow (β := ℕ) (u * v) 2 * W'.negAddY P Q) - W'.a₁ * (HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q) -
      W'.a₃ * (HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q) =
    HPow.hPow (β := ℕ) (u * v) 2 * (-W'.negAddY P Q - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.addY P P = 0

Tactic:
simp only [addY, negY_eq, negAddY_self, addX_self, addZ_self, neg_zero, mul_zero, sub_zero]

Premises used: WeierstrassCurve.Projective.negY_eq, WeierstrassCurve.Projective.negAddY_self, sub_zero, MulZeroClass.mul_zero, WeierstrassCurve.Projective.addZ_self, WeierstrassCurve.Projective.addY, neg_zero, WeierstrassCurve.Projective.addX_self
-- 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 :
  -(HPow.hPow (β := ℕ) (P y) 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)) -
        W'.a₁ * (HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x) -
      W'.a₃ * (HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z) =
    HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y
⊢ W'.addY P Q = HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y

Tactic:
rw [addY, negY_eq, negAddY_of_Z_eq_zero_left hP hPz, negY, addX_of_Z_eq_zero_left hP hPz,
    addZ_of_Z_eq_zero_left hP hPz]

Premises used: WeierstrassCurve.Projective.negY, WeierstrassCurve.Projective.negY_eq, WeierstrassCurve.Projective.addX_of_Z_eq_zero_left, WeierstrassCurve.Projective.addZ_of_Z_eq_zero_left, WeierstrassCurve.Projective.addY, WeierstrassCurve.Projective.negAddY_of_Z_eq_zero_left
-- 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
⊢ -(HPow.hPow (β := ℕ) (P y) 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)) -
        W'.a₁ * (HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x) -
      W'.a₃ * (HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z) =
    HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y

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 :
  -(-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)) -
        W'.a₁ * (-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x) -
      W'.a₃ * (-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P z) =
    -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P y
⊢ W'.addY P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P y

Tactic:
rw [addY, negY_eq, negAddY_of_Z_eq_zero_right hQ hQz, negY, addX_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQ hQz]

Premises used: WeierstrassCurve.Projective.negY, WeierstrassCurve.Projective.negY_eq, WeierstrassCurve.Projective.addZ_of_Z_eq_zero_right, WeierstrassCurve.Projective.negAddY_of_Z_eq_zero_right, WeierstrassCurve.Projective.addY, WeierstrassCurve.Projective.addX_of_Z_eq_zero_right
-- 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
⊢ -(-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)) -
        W'.a₁ * (-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x) -
      W'.a₃ * (-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P z) =
    -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P y

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
a :
  (-W'.negAddY P Q - W'.a₁ * 0 - W'.a₃ * 0) * HPow.hPow (β := ℕ) (P z * Q z) 3 +
        -(P z * Q z) * (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * (P z * Q z)) -
      (-HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 +
        -(P z * Q z) * (W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 2)) =
    0
⊢ W'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 +
        -(P z * Q z) * (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * (P z * Q z)) -
      (-HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 +
        -(P z * Q z) * (W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 2)) =
    0

Tactic:
rw [addY, negY_eq, addX_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx]

Premises used: WeierstrassCurve.Projective.negY_eq, WeierstrassCurve.Projective.addX_of_X_eq, WeierstrassCurve.Projective.addY, WeierstrassCurve.Projective.addZ_of_X_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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ (-W'.negAddY P Q - W'.a₁ * 0 - W'.a₃ * 0) * HPow.hPow (β := ℕ) (P z * Q z) 3 +
        -(P z * Q z) * (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * (P z * Q z)) -
      (-HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 +
        -(P z * Q z) * (W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 2)) =
    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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
a :
  W'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 +
        -(P z * Q z) * (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * (P z * Q z)) -
      (-HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 +
        -(P z * Q z) * (W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 2)) =
    0
⊢ W'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 =
    -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2

Tactic:
linear_combination (norm := (rw [addY, negY_eq, addX_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx]; ring1)) -(P z * Q z) * negAddY_of_X_eq' hP hQ hx

Premises used: WeierstrassCurve.Projective.negY_eq, HMul.hMul, WeierstrassCurve.Projective.addX_of_X_eq, WeierstrassCurve.Projective.negAddY_of_X_eq', OfNat.ofNat, WeierstrassCurve.Projective.addY, WeierstrassCurve.Projective.addZ_of_X_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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
rw : W.addY P Q = -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z)
rw₁ :
  W.addY P Q =
    -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (P z * Q z * HPow.hPow (β := ℕ) (P z * Q z) 2)
rw₂ : W.addY P Q = W.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / (P z * Q z * HPow.hPow (β := ℕ) (P z * Q z) 2)
rw₃ : W.addY P Q = W.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / (P z * Q z) ^ HAdd.hAdd (α := ℕ) 2 1
rw₄ rw₅ : W.addY P Q = W.addY P Q
⊢ W.addY P Q = addU P Q

Tactic:
rw [addU, ← mul_div_mul_right _ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz,
    ← addY_of_X_eq' hP hQ hPz hQz hx, ← pow_succ',
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]

Premises used: mul_div_mul_right, WeierstrassCurve.Projective.addY_of_X_eq', pow_ne_zero, mul_div_cancel_right₀, WeierstrassCurve.Projective.addU, mul_ne_zero, OfNat.ofNat, pow_succ'
-- 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
erw :
  W.negY ![W.addX P Q, W.negAddY P Q, W.addZ P Q] / W.addZ P Q =
    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.addX P Q, W.negAddY P Q, W.addZ P Q] x / ![W.addX P Q, W.negAddY P Q, W.addZ P Q] z)
      (![W.addX P Q, W.negAddY P Q, W.addZ P Q] y / ![W.addX P Q, W.negAddY P Q, W.addZ P 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₂ :
  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.addX P Q, W.negAddY P Q, W.addZ P Q] y / ![W.addX P Q, W.negAddY P Q, W.addZ P 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₃ :
  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.addY P Q / W.addZ P Q =
    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 [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hP hQ hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
    negAddY_of_Z_ne_zero hP hQ hPz hQz hx, Affine.addY]

Premises used: WeierstrassCurve.Projective.addZ_ne_zero_of_X_ne, WeierstrassCurve.Projective.negY_of_Z_ne_zero, WeierstrassCurve.Affine.addY, WeierstrassCurve.Projective.addX_of_Z_ne_zero, WeierstrassCurve.Projective.addY, WeierstrassCurve.Projective.negAddY_of_Z_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
⊢ W'.addXYZ P Q x = W'.addX P Q

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, WeierstrassCurve.Projective.addZ, Fin.induction, Fin.cases, WeierstrassCurve.Projective.addXYZ, Matrix.vecCons, rfl