awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -P y * HPow.hPow (β := ℕ) (Q x) 3 * HPow.hPow (β := ℕ) (P z) 3 +
                                              2 * P y * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 3 -
                                            3 * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q y * HPow.hPow (β := ℕ) (P z) 2 *
                                              0 +
                                          3 * P x * P y * HPow.hPow (β := ℕ) (Q x) 2 * P z *
                                            HPow.hPow (α := R) (β := ℕ) 0 2 +
                                        HPow.hPow (β := ℕ) (P x) 3 * Q y * HPow.hPow (α := R) (β := ℕ) 0 3 -
                                      2 * HPow.hPow (β := ℕ) (P y) 2 * Q y * HPow.hPow (α := R) (β := ℕ) 0 3 +
                                    W'.a₁ * P x * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 4 +
                                  W'.a₁ * P y * Q x * Q y * HPow.hPow (β := ℕ) (P z) 3 * 0 -
                                W'.a₁ * P x * P y * Q y * P z * HPow.hPow (α := R) (β := ℕ) 0 3 -
                              W'.a₁ * HPow.hPow (β := ℕ) (P y) 2 * Q x * HPow.hPow (α := R) (β := ℕ) 0 4 -
                            2 * W'.a₂ * P x * Q x * Q y * HPow.hPow (β := ℕ) (P z) 4 * 0 +
                          2 * W'.a₂ * P x * P y * Q x * P z * HPow.hPow (α := R) (β := ℕ) 0 4 +
                        W'.a₃ * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 6 -
                      W'.a₃ * HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (α := R) (β := ℕ) 0 6 -
                    W'.a₄ * Q x * Q y * HPow.hPow (β := ℕ) (P z) 6 * 0 -
                  W'.a₄ * P x * Q y * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (α := R) (β := ℕ) 0 3 +
                W'.a₄ * P y * Q x * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (α := R) (β := ℕ) 0 4 +
              W'.a₄ * P x * P y * P z * HPow.hPow (α := R) (β := ℕ) 0 6 -
            2 * W'.a₆ * Q y * HPow.hPow (β := ℕ) (P z) 6 * HPow.hPow (α := R) (β := ℕ) 0 3 +
          2 * W'.a₆ * P y * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (α := R) (β := ℕ) 0 6 +
        (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) * HPow.hPow (β := ℕ) (P z) 3 *
          HPow.hPow (β := ℕ) (Q x) 3 -
      (HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) +
        (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) * HPow.hPow (β := ℕ) (P z) 3 *
          HPow.hPow (β := ℕ) (Q y) 2) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
a :
  W'.negAddY P Q + (P y - W'.negY P) * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (β := ℕ) (Q x) 3 -
      (HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * W'.negY P +
        (P y - W'.negY P) * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (β := ℕ) (Q y) 2) =
    0
⊢ W'.negAddY P Q = HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * W'.negY P

Tactic:
linear_combination (norm := (rw [negAddY, negY, hQz]; ring1))
    (P y - W'.negY P) * P z ^ 3 * (equation_of_Z_eq_zero hQz).mp hQ

Premises used: WeierstrassCurve.Jacobian.negAddY, WeierstrassCurve.Jacobian.negY, HSub.hSub, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero, Iff.mp, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) *
        (HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 +
                  W'.a₁ * (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) * P z * Q z * 0 -
                W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
              P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
            Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
          P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2) +
      P y * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (α := R) (β := ℕ) 0 3 =
    HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3
⊢ W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 =
    HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3

Tactic:
rw [negAddY_eq', addX_eq' hP hQ, addZ_of_X_eq hx]

Premises used: WeierstrassCurve.Jacobian.addX_eq', WeierstrassCurve.Jacobian.addZ_of_X_eq, WeierstrassCurve.Jacobian.negAddY_eq'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) *
        (HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 +
                  W'.a₁ * (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) * P z * Q z * 0 -
                W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
              P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
            Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
          P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2) +
      P y * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (α := R) (β := ℕ) 0 3 =
    HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian 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 * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) (- -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 3
rw₁ :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 3
rw₂ :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3 /
      HPow.hPow (β := ℕ) (P z * Q z) 3
rw₃ : W.negAddY P Q = W.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / HPow.hPow (β := ℕ) (P z * Q z) 3
rw₄ rw₅ : W.negAddY P Q = W.negAddY P Q
⊢ W.negAddY P Q = HPow.hPow (β := ℕ) (-addU P Q) 3

Tactic:
rw [addU, neg_neg, div_pow, ← negAddY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]

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

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

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

Tactic:
simp [field]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
simp :
  -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.negAddY P Q) -
        W'.a₁ * (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q) *
          (HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q) -
      W'.a₃ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q) 3 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 *
      (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * HPow.hPow (β := ℕ) (addZ P Q) 3)
⊢ W'.addY (u • P) (v • Q) = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q

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

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

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
rw : -0 - W'.a₁ * 0 * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = 0
⊢ W'.addY P P = 0

Tactic:
rw [addY, negY_eq, addX_self hP, negAddY_self, addZ_self]

Premises used: WeierstrassCurve.Jacobian.addY, WeierstrassCurve.Jacobian.negY_eq, WeierstrassCurve.Jacobian.negAddY_self, WeierstrassCurve.Jacobian.addX_self, WeierstrassCurve.Jacobian.addZ_self
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -0 - W'.a₁ * 0 * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = 0

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

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

Premises used: WeierstrassCurve.Jacobian.negAddY_of_Z_eq_zero_left, WeierstrassCurve.Jacobian.addY, WeierstrassCurve.Jacobian.negY_eq, WeierstrassCurve.Jacobian.negY, WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_left, WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(HPow.hPow (β := ℕ) (P x * Q z) 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * HPow.hPow (β := ℕ) (Q z) 3)) -
        W'.a₁ * (HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x) * (P x * Q z * Q z) -
      W'.a₃ * HPow.hPow (β := ℕ) (P x * Q z * Q z) 3 =
    HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
rw :
  -(HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) -
        W'.a₁ * (HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x) * (-(Q x * P z) * P z) -
      W'.a₃ * HPow.hPow (β := ℕ) (-(Q x * P z) * P z) 3 =
    HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y
⊢ W'.addY P Q = HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y

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

Premises used: WeierstrassCurve.Jacobian.addY, WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_right, WeierstrassCurve.Jacobian.negY_eq, WeierstrassCurve.Jacobian.negAddY_of_Z_eq_zero_right, WeierstrassCurve.Jacobian.negY, WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -(HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) -
        W'.a₁ * (HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x) * (-(Q x * P z) * P z) -
      W'.a₃ * HPow.hPow (β := ℕ) (-(Q x * P z) * P z) 3 =
    HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
a :
  (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3) *
          HPow.hPow (β := ℕ) (P z * Q z) 3 +
        W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 -
      (HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3 +
        HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3) =
    0
⊢ W'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 + W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 -
      (HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3 +
        HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3) =
    0

Tactic:
rw [addY, negY_eq, addZ_of_X_eq hx]

Premises used: WeierstrassCurve.Jacobian.addY, WeierstrassCurve.Jacobian.negY_eq, WeierstrassCurve.Jacobian.addZ_of_X_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3) *
          HPow.hPow (β := ℕ) (P z * Q z) 3 +
        W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 -
      (HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3 +
        HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
a :
  W'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 + W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 -
      (HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3 +
        HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3) =
    0
⊢ W'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 =
    HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3

Tactic:
linear_combination (norm := (rw [addY, negY_eq, addZ_of_X_eq hx]; ring1))
    -negAddY_of_X_eq' hP hQ hx

Premises used: WeierstrassCurve.Jacobian.addY, WeierstrassCurve.Jacobian.negY_eq, WeierstrassCurve.Jacobian.negAddY_of_X_eq', WeierstrassCurve.Jacobian.addZ_of_X_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian 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 * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 3
rw₁ :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 3
rw₂ :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3 /
      HPow.hPow (β := ℕ) (P z * Q z) 3
rw₃ : W.addY P Q = W.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / HPow.hPow (β := ℕ) (P z * Q z) 3
rw₄ rw₅ : W.addY P Q = W.addY P Q
⊢ W.addY P Q = HPow.hPow (β := ℕ) (addU P Q) 3

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

Premises used: neg_div, pow_ne_zero, WeierstrassCurve.Jacobian.addU, mul_div_cancel_right₀, div_pow, WeierstrassCurve.Jacobian.addY_of_X_eq', mul_ne_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
⊢ W'.addXYZ P Q x = W'.addX P Q

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]

Premises used: WeierstrassCurve.Jacobian.addXYZ_X, WeierstrassCurve.Jacobian.addXYZ_Z, WeierstrassCurve.Jacobian.addZ_smul, WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.addY_smul, WeierstrassCurve.Jacobian.addXYZ, WeierstrassCurve.Jacobian.addX_smul, WeierstrassCurve.Jacobian.addXYZ_Y
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
rw : ![W'.addX P P, W'.addY P P, addZ P P] = ![0, 0, 0]
rw₁ : ![0, W'.addY P P, addZ P P] = ![0, 0, 0]
rw₂ : ![0, 0, addZ P P] = ![0, 0, 0]
rw₃ rw₄ : Eq.{r + 1} (α := Fin 3 → R) ![0, 0, 0] ![0, 0, 0]
⊢ W'.addXYZ P P = ![0, 0, 0]

Tactic:
rw [addXYZ, addX_self hP, addY_self hP, addZ_self]

Premises used: WeierstrassCurve.Jacobian.addXYZ, WeierstrassCurve.Jacobian.addX_self, WeierstrassCurve.Jacobian.addZ_self, WeierstrassCurve.Jacobian.addY_self