awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4 * W'.dblU P) 2 -
          W'.a₁ * (HPow.hPow (β := ℕ) u 4 * W'.dblU P) * (u * P z) *
            (HPow.hPow (β := ℕ) u 3 * P y - HPow.hPow (β := ℕ) u 3 * W'.negY P) -
        W'.a₂ * HPow.hPow (β := ℕ) (u * P z) 2 *
          HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y - HPow.hPow (β := ℕ) u 3 * W'.negY P) 2 -
      2 * (HPow.hPow (β := ℕ) u 2 * P x) *
        HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y - HPow.hPow (β := ℕ) u 3 * W'.negY P) 2 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 *
      (HPow.hPow (β := ℕ) (W'.dblU P) 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) -
          W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
        2 * P x * HPow.hPow (β := ℕ) (P y - W'.negY P) 2)

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
hPz : P z = 0
a :
  HPow.hPow (β := ℕ) (-3 * HPow.hPow (β := ℕ) (P x) 2) 2 -
              W'.a₁ * (-3 * HPow.hPow (β := ℕ) (P x) 2) * 0 * (P y - -P y) -
            W'.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) (P y - -P y) 2 -
          2 * P x * HPow.hPow (β := ℕ) (P y - -P y) 2 +
        -8 * P x * HPow.hPow (β := ℕ) (P x) 3 -
      (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 2 + -8 * P x * HPow.hPow (β := ℕ) (P y) 2) =
    0
⊢ W'.dblX P + -8 * P x * HPow.hPow (β := ℕ) (P x) 3 -
      (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 2 + -8 * P x * HPow.hPow (β := ℕ) (P y) 2) =
    0

Tactic:
rw [dblX, dblU_of_Z_eq_zero hPz, negY_of_Z_eq_zero hPz, hPz]

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

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
hPz : P z = 0
a :
  W'.dblX P + -8 * P x * HPow.hPow (β := ℕ) (P x) 3 -
      (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 2 + -8 * P x * HPow.hPow (β := ℕ) (P y) 2) =
    0
⊢ W'.dblX P = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 2

Tactic:
linear_combination (norm := (rw [dblX, dblU_of_Z_eq_zero hPz, negY_of_Z_eq_zero hPz, hPz]; ring1))
    -8 * P x * (equation_of_Z_eq_zero hPz).mp hP

Premises used: WeierstrassCurve.Jacobian.dblX, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero, Iff.mp, WeierstrassCurve.Jacobian.dblU_of_Z_eq_zero, OfNat.ofNat, WeierstrassCurve.Jacobian.negY_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw :
  HPow.hPow (β := ℕ) (W'.dblU P) 2 - W'.a₁ * W'.dblU P * P z * (W'.negY P - W'.negY P) -
        W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2 -
      2 * P x * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2 =
    HPow.hPow (β := ℕ) (W'.dblU P) 2
⊢ W'.dblX P = HPow.hPow (β := ℕ) (W'.dblU P) 2

Tactic:
rw [dblX, Y_eq_negY_of_Y_eq hQz hx hy hy']

Premises used: WeierstrassCurve.Jacobian.dblX, WeierstrassCurve.Jacobian.Y_eq_negY_of_Y_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ HPow.hPow (β := ℕ) (W'.dblU P) 2 - W'.a₁ * W'.dblU P * P z * (W'.negY P - W'.negY P) -
        W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2 -
      2 * P x * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2 =
    HPow.hPow (β := ℕ) (W'.dblU P) 2

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

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

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
simp :
  -(HPow.hPow (β := ℕ) u 4 * W'.dblU P) *
        (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P -
          HPow.hPow (β := ℕ) u 2 * P x *
            HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y - HPow.hPow (β := ℕ) u 3 * W'.negY P) 2) +
      HPow.hPow (β := ℕ) u 3 * P y *
        HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y - HPow.hPow (β := ℕ) u 3 * W'.negY P) 3 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 *
      (-W'.dblU P * (W'.dblX P - P x * HPow.hPow (β := ℕ) (P y - W'.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P y - W'.negY P) 3)
⊢ W'.negDblY (u • P) = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.negDblY P

Tactic:
simp only [negDblY, dblU_smul, dblX_smul, negY_smul, smul_fin3_ext]

Premises used: WeierstrassCurve.Jacobian.dblX_smul, WeierstrassCurve.Jacobian.dblU_smul, WeierstrassCurve.Jacobian.negY_smul, WeierstrassCurve.Jacobian.smul_fin3_ext, WeierstrassCurve.Jacobian.negDblY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ -(HPow.hPow (β := ℕ) u 4 * W'.dblU P) *
        (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P -
          HPow.hPow (β := ℕ) u 2 * P x *
            HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y - HPow.hPow (β := ℕ) u 3 * W'.negY P) 2) +
      HPow.hPow (β := ℕ) u 3 * P y *
        HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 3 * P y - HPow.hPow (β := ℕ) u 3 * W'.negY P) 3 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 *
      (-W'.dblU P * (W'.dblX P - P x * HPow.hPow (β := ℕ) (P y - W'.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P y - W'.negY P) 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
hPz : P z = 0
a :
  -(-3 * HPow.hPow (β := ℕ) (P x) 2) *
            (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 2 - P x * HPow.hPow (β := ℕ) (P y - -P y) 2) +
          P y * HPow.hPow (β := ℕ) (P y - -P y) 3 +
        (8 * HPow.hPow (β := ℕ) (P y) 2 - 4 * HPow.hPow (β := ℕ) (P x) 3) * HPow.hPow (β := ℕ) (P x) 3 -
      (-HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 3 +
        (8 * HPow.hPow (β := ℕ) (P y) 2 - 4 * HPow.hPow (β := ℕ) (P x) 3) * HPow.hPow (β := ℕ) (P y) 2) =
    0
⊢ W'.negDblY P + (8 * HPow.hPow (β := ℕ) (P y) 2 - 4 * HPow.hPow (β := ℕ) (P x) 3) * HPow.hPow (β := ℕ) (P x) 3 -
      (-HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 3 +
        (8 * HPow.hPow (β := ℕ) (P y) 2 - 4 * HPow.hPow (β := ℕ) (P x) 3) * HPow.hPow (β := ℕ) (P y) 2) =
    0

Tactic:
rw [negDblY, dblU_of_Z_eq_zero hPz, dblX_of_Z_eq_zero hP hPz, negY_of_Z_eq_zero hPz]

Premises used: WeierstrassCurve.Jacobian.dblX_of_Z_eq_zero, WeierstrassCurve.Jacobian.dblU_of_Z_eq_zero, WeierstrassCurve.Jacobian.negDblY, WeierstrassCurve.Jacobian.negY_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -(-3 * HPow.hPow (β := ℕ) (P x) 2) *
            (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 2 - P x * HPow.hPow (β := ℕ) (P y - -P y) 2) +
          P y * HPow.hPow (β := ℕ) (P y - -P y) 3 +
        (8 * HPow.hPow (β := ℕ) (P y) 2 - 4 * HPow.hPow (β := ℕ) (P x) 3) * HPow.hPow (β := ℕ) (P x) 3 -
      (-HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 3 +
        (8 * HPow.hPow (β := ℕ) (P y) 2 - 4 * HPow.hPow (β := ℕ) (P x) 3) * HPow.hPow (β := ℕ) (P y) 2) =
    0

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
hPz : P z = 0
a :
  W'.negDblY P + (8 * HPow.hPow (β := ℕ) (P y) 2 - 4 * HPow.hPow (β := ℕ) (P x) 3) * HPow.hPow (β := ℕ) (P x) 3 -
      (-HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 3 +
        (8 * HPow.hPow (β := ℕ) (P y) 2 - 4 * HPow.hPow (β := ℕ) (P x) 3) * HPow.hPow (β := ℕ) (P y) 2) =
    0
⊢ W'.negDblY P = -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 3

Tactic:
linear_combination (norm :=
      (rw [negDblY, dblU_of_Z_eq_zero hPz, dblX_of_Z_eq_zero hP hPz, negY_of_Z_eq_zero hPz]; ring1))
    (8 * P y ^ 2 - 4 * P x ^ 3) * (equation_of_Z_eq_zero hPz).mp hP

Premises used: HMul.hMul, HSub.hSub, HPow.hPow, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero, WeierstrassCurve.Jacobian.dblX_of_Z_eq_zero, Iff.mp, WeierstrassCurve.Jacobian.dblU_of_Z_eq_zero, WeierstrassCurve.Jacobian.negDblY, OfNat.ofNat, WeierstrassCurve.Jacobian.negY_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw :
  -W'.dblU P * (HPow.hPow (β := ℕ) (W'.dblU P) 2 - P x * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2) +
      W'.negY P * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 3 =
    HPow.hPow (β := ℕ) (-W'.dblU P) 3
⊢ W'.negDblY P = HPow.hPow (β := ℕ) (-W'.dblU P) 3

Tactic:
rw [negDblY, dblX_of_Y_eq hQz hx hy hy', Y_eq_negY_of_Y_eq hQz hx hy hy']

Premises used: WeierstrassCurve.Jacobian.dblX_of_Y_eq, WeierstrassCurve.Jacobian.Y_eq_negY_of_Y_eq, WeierstrassCurve.Jacobian.negDblY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ -W'.dblU P * (HPow.hPow (β := ℕ) (W'.dblU P) 2 - P x * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2) +
      W'.negY P * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 3 =
    HPow.hPow (β := ℕ) (-W'.dblU P) 3

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
rw :
  -n / (P z * d) *
        ((HPow.hPow (β := ℕ) n 2 - W.a₁ * n * P z * d - W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 -
              2 * P x * HPow.hPow (β := ℕ) d 2) /
            HPow.hPow (β := ℕ) (P z * 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 * d - W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 -
              2 * P x * HPow.hPow (β := ℕ) d 2 -
            P x * HPow.hPow (β := ℕ) d 2) +
        P y * HPow.hPow (β := ℕ) d 3) /
      HPow.hPow (β := ℕ) (P z * d) 3
⊢ W.toAffine.negAddY (P x / HPow.hPow (β := ℕ) (P z) 2) (P x / HPow.hPow (β := ℕ) (P z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3) (-n / (P z * d)) =
    (-n *
          (HPow.hPow (β := ℕ) n 2 - W.a₁ * n * P z * d - W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 -
              2 * P x * HPow.hPow (β := ℕ) d 2 -
            P x * HPow.hPow (β := ℕ) d 2) +
        P y * HPow.hPow (β := ℕ) d 3) /
      HPow.hPow (β := ℕ) (P z * d) 3

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

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

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

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

Premises used: WeierstrassCurve.Jacobian.negY_eq, WeierstrassCurve.Jacobian.dblZ_smul, WeierstrassCurve.Jacobian.dblX_smul, WeierstrassCurve.Jacobian.negDblY_smul, WeierstrassCurve.Jacobian.dblY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.negDblY P) -
        W'.a₁ * (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P) * (HPow.hPow (β := ℕ) u 4 * W'.dblZ P) -
      W'.a₃ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4 * W'.dblZ P) 3 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 *
      (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * HPow.hPow (β := ℕ) (W'.dblZ P) 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
hPz : P z = 0
rw :
  - -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 3 - W'.a₁ * W'.dblX P * 0 -
      W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 =
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 3
⊢ W'.dblY P = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 3

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

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

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw :
  -HPow.hPow (β := ℕ) (-W'.dblU P) 3 - W'.a₁ * W'.dblX P * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 =
    HPow.hPow (β := ℕ) (W'.dblU P) 3
⊢ W'.dblY P = HPow.hPow (β := ℕ) (W'.dblU P) 3

Tactic:
rw [dblY, negY_eq, negDblY_of_Y_eq hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy']

Premises used: WeierstrassCurve.Jacobian.negY_eq, WeierstrassCurve.Jacobian.negDblY_of_Y_eq, WeierstrassCurve.Jacobian.dblZ_of_Y_eq, WeierstrassCurve.Jacobian.dblY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ -HPow.hPow (β := ℕ) (-W'.dblU P) 3 - W'.a₁ * W'.dblX P * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 =
    HPow.hPow (β := ℕ) (W'.dblU P) 3

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.dblXYZ P x = W'.dblX P

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: Eq.mpr, WeierstrassCurve.Jacobian.dblXYZ, Fin.cons, Fin.induction.go, WeierstrassCurve.Jacobian.dblZ, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian 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 (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P, W'.dblY (u • P), W'.dblZ (u • P)] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₂ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.dblY P, W'.dblZ (u • P)] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₃ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₄ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblXYZ P x,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.dblXYZ P y, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
rw₅ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.dblXYZ P y, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
rw₆ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
rw₇ rw₈ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * 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.Jacobian.dblXYZ_Z, WeierstrassCurve.Jacobian.dblXYZ_X, WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.dblXYZ, WeierstrassCurve.Jacobian.dblZ_smul, WeierstrassCurve.Jacobian.dblY_smul, WeierstrassCurve.Jacobian.dblX_smul, WeierstrassCurve.Jacobian.dblXYZ_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
hPz : P z = 0
⊢ W'.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0]

Tactic:
simp [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz,
    smul_fin3]

Premises used: WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.dblXYZ, WeierstrassCurve.Jacobian.dblY_of_Z_eq_zero, WeierstrassCurve.Jacobian.dblZ_of_Z_eq_zero, WeierstrassCurve.Jacobian.dblX_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw : ![W'.dblX P, W'.dblY P, W'.dblZ P] = ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
rw₁ :
  ![HPow.hPow (β := ℕ) (W'.dblU P) 2, W'.dblY P, W'.dblZ P] =
    ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
rw₂ :
  ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, W'.dblZ P] =
    ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
rw₃ rw₄ :
  ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0] =
    ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
⊢ W'.dblXYZ P = ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]

Tactic:
rw [dblXYZ, dblX_of_Y_eq hQz hx hy hy', dblY_of_Y_eq hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy']

Premises used: WeierstrassCurve.Jacobian.dblX_of_Y_eq, WeierstrassCurve.Jacobian.dblXYZ, WeierstrassCurve.Jacobian.dblY_of_Y_eq, WeierstrassCurve.Jacobian.dblZ_of_Y_eq