ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>W'.Nonsingular P ↔ W'.Equation P ∧ (W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) ≠ 0 ∨ 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3 ≠ 0 ∨ W'.a₁ * P x * P y + 3 * W'.a₃ * P y * P z ^ 2 - (2 * W'.a₂ * P x ^ 2 * P z + 4 * W'.a₄ * P x * P z ^ 3 + 6 * W'.a₆ * P z ^ 5) ≠ 0)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>u : R<VAR>hu : IsUnit u<GOAL>W'.Nonsingular (u • P) ↔ W'.Nonsingular P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>h : P ≈ Q<GOAL>W'.Nonsingular P ↔ W'.Nonsingular Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W'.a₁ * P x * P y ≠ 0)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>Nontrivial R<GOAL>W'.Nonsingular ![1, 1, 0]
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>X Y : R<GOAL>W'.Nonsingular ![X, Y, 1] ↔ W'.toAffine.Nonsingular X Y
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>W.Nonsingular P ↔ W.toAffine.Nonsingular (P x / P z ^ 2) (P y / P z ^ 3)
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>W.Nonsingular P ↔ W.Equation P ∧ ((MvPolynomial.eval P) W.polynomialX ≠ 0 ∨ (MvPolynomial.eval P) W.polynomialY ≠ 0)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P : Fin 3 → R<VAR>hP : W'.Nonsingular P<VAR>hPz : P z = 0<GOAL>P x ≠ 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z = 0<GOAL>IsUnit (P x)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P : Fin 3 → R<VAR>hP : W'.Nonsingular P<VAR>hPz : P z = 0<GOAL>P y ≠ 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z = 0<GOAL>IsUnit (P y)
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hQ : W.Nonsingular Q<VAR>hPz : P z = 0<VAR>hQz : Q z = 0<GOAL>P ≈ Q
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z = 0<GOAL>P ≈ ![1, 1, 0]
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>W'.NonsingularLift ⟦P⟧ ↔ W'.Nonsingular P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>Nontrivial R<GOAL>W'.NonsingularLift ⟦![1, 1, 0]⟧
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>X Y : R<GOAL>W'.NonsingularLift ⟦![X, Y, 1]⟧ ↔ W'.toAffine.Nonsingular X Y
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.negY (u • P) = u ^ 3 * W'.negY P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.negY P = -P y
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<GOAL>W.negY P / P z ^ 3 = W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>(P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) = 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3<GOAL>P y * Q z ^ 3 = W.negY Q * P z ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>P y * Q z ^ 3 = Q y * P z ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<GOAL>P y * Q z ^ 3 = W.negY Q * P z ^ 3 ↔ P y / P z ^ 3 = W.toAffine.negY (Q x / Q z ^ 2) (Q y / Q z ^ 3)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>P y * Q z ^ 3 - Q y * P z ^ 3 + (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) = (P y - W'.negY P) * Q z ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3<GOAL>P y ≠ W'.negY P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W'.negY Q * P z ^ 3<GOAL>P y ≠ W'.negY P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3<GOAL>P y = W'.negY P
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hy : P y = W.negY P<GOAL>W.Nonsingular P ↔ W.Equation P ∧ (MvPolynomial.eval P) W.polynomialX ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>W'.dblU P = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.dblU (u • P) = u ^ 4 * W'.dblU P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.dblU P = -3 * P x ^ 2
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3<GOAL>W.dblU P ≠ 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3<GOAL>IsUnit (W.dblU P)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.dblZ (u • P) = u ^ 4 * W'.dblZ P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.dblZ P = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3<GOAL>W'.dblZ P = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hPz : P z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3<GOAL>W'.dblZ P ≠ 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3<GOAL>IsUnit (W.dblZ P)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hPz : P z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W'.negY Q * P z ^ 3<GOAL>W'.dblZ P ≠ 0
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>IsUnit (W.dblZ P)
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = -W.dblU P / W.dblZ P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.dblX (u • P) = (u ^ 4) ^ 2 * W'.dblX P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.dblX P = (P x ^ 2) ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3<GOAL>W'.dblX P = W'.dblU P ^ 2
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>n d : F<VAR>hPz : P z ≠ 0<VAR>hd : d ≠ 0<GOAL>W.toAffine.addX (P x / P z ^ 2) (P x / P z ^ 2) (-n / (P z * d)) = (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2) / (P z * d) ^ 2
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.dblX P / W.dblZ P ^ 2 = W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.negDblY (u • P) = (u ^ 4) ^ 3 * W'.negDblY P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.negDblY P = -(P x ^ 2) ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3<GOAL>W'.negDblY P = (-W'.dblU P) ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P : Fin 3 → F<VAR>n d : F<VAR>hPz : P z ≠ 0<VAR>hd : d ≠ 0<GOAL>W.toAffine.negAddY (P x / P z ^ 2) (P x / P z ^ 2) (P y / P z ^ 3) (-n / (P z * d)) = (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * d ^ 2 - P x * d ^ 2) + P y * d ^ 3) / (P z * d) ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.negDblY P / W.dblZ P ^ 3 = W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.dblY (u • P) = (u ^ 4) ^ 3 * W'.dblY P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.dblY P = (P x ^ 2) ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3<GOAL>W'.dblY P = W'.dblU P ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.dblY P / W.dblZ P ^ 3 = W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.dblXYZ (u • P) = u ^ 4 • W'.dblXYZ P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.dblXYZ P = P x ^ 2 • ![1, 1, 0]
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>NoZeroDivisors R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3<GOAL>W'.dblXYZ P = ![W'.dblU P ^ 2, W'.dblU P ^ 3, 0]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 = Q y * P z ^ 3<VAR>hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3<GOAL>W.dblXYZ P = W.dblU P • ![1, 1, 0]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<VAR>hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3<GOAL>W.dblXYZ P = W.dblZ P • ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1]
<VAR>F : Type v<VAR>Field F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>u v : F<VAR>hu : u ≠ 0<VAR>hv : v ≠ 0<GOAL>WeierstrassCurve.Jacobian.addU (u • P) (v • Q) = (u * v) ^ 2 * WeierstrassCurve.Jacobian.addU P Q
<VAR>F : Type v<VAR>Field F<VAR>P Q : Fin 3 → F<VAR>hPz : P z = 0<GOAL>WeierstrassCurve.Jacobian.addU P Q = 0
<VAR>F : Type v<VAR>Field F<VAR>P Q : Fin 3 → F<VAR>hQz : Q z = 0<GOAL>WeierstrassCurve.Jacobian.addU P Q = 0
<VAR>F : Type v<VAR>Field F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3<GOAL>WeierstrassCurve.Jacobian.addU P Q ≠ 0
<VAR>F : Type v<VAR>Field F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3<GOAL>IsUnit (WeierstrassCurve.Jacobian.addU P Q)
<VAR>R : Type u<VAR>CommRing R<VAR>P : Fin 3 → R<GOAL>WeierstrassCurve.Jacobian.addZ P P = 0
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>WeierstrassCurve.Jacobian.addZ (u • P) (v • Q) = (u * v) ^ 2 * WeierstrassCurve.Jacobian.addZ P Q
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>hPz : P z = 0<GOAL>WeierstrassCurve.Jacobian.addZ P Q = P x * Q z * Q z
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z = 0<GOAL>WeierstrassCurve.Jacobian.addZ P Q = -(Q x * P z) * P z
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>WeierstrassCurve.Jacobian.addZ P Q = 0
<VAR>R : Type u<VAR>CommRing R<VAR>P Q : Fin 3 → R<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>WeierstrassCurve.Jacobian.addZ P Q ≠ 0
<VAR>F : Type v<VAR>Field F<VAR>P Q : Fin 3 → F<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>IsUnit (WeierstrassCurve.Jacobian.addZ P Q)
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) = (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * WeierstrassCurve.Jacobian.addZ P Q)
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>W'.addX P P = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<GOAL>W'.addX P Q * (P z * Q z) ^ 2 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W'.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * WeierstrassCurve.Jacobian.addZ P Q - W'.a₂ * P z ^ 2 * Q z ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 - P x * Q z ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 - Q x * P z ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<GOAL>W.addX P Q = ((P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * WeierstrassCurve.Jacobian.addZ P Q - W.a₂ * P z ^ 2 * Q z ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 - P x * Q z ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2 - Q x * P z ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2) / (P z * Q z) ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>W'.addX (u • P) (v • Q) = ((u * v) ^ 2) ^ 2 * W'.addX P Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hPz : P z = 0<GOAL>W'.addX P Q = (P x * Q z) ^ 2 * Q x
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hQz : Q z = 0<GOAL>W'.addX P Q = (-(Q x * P z)) ^ 2 * P x
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W'.addX P Q * (P z * Q z) ^ 2 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W.addX P Q = WeierstrassCurve.Jacobian.addU P Q ^ 2
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>n d : F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hd : d ≠ 0<GOAL>W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (n / (P z * Q z * d)) = (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 - Q x * P z ^ 2 * d ^ 2) / (P z * Q z * d) ^ 2
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>W.addX P Q / WeierstrassCurve.Jacobian.addZ P Q ^ 2 = W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<GOAL>W'.negAddY P P = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<GOAL>W'.negAddY P Q * (P z * Q z) ^ 3 = (P y * Q z ^ 3 - Q y * P z ^ 3) * (W'.addX P Q * (P z * Q z) ^ 2 - P x * Q z ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2) + P y * Q z ^ 3 * WeierstrassCurve.Jacobian.addZ P Q ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<GOAL>W.negAddY P Q = ((P y * Q z ^ 3 - Q y * P z ^ 3) * (W.addX P Q * (P z * Q z) ^ 2 - P x * Q z ^ 2 * WeierstrassCurve.Jacobian.addZ P Q ^ 2) + P y * Q z ^ 3 * WeierstrassCurve.Jacobian.addZ P Q ^ 3) / (P z * Q z) ^ 3
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>W'.negAddY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.negAddY P Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.negAddY P Q = (P x * Q z) ^ 3 * W'.negY Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hQ : W'.Equation Q<VAR>hQz : Q z = 0<GOAL>W'.negAddY P Q = (-(Q x * P z)) ^ 3 * W'.negY P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W'.negAddY P Q * (P z * Q z) ^ 3 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W.negAddY P Q = (-WeierstrassCurve.Jacobian.addU P Q) ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>n d : F<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hd : d ≠ 0<GOAL>W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (n / (P z * Q z * d)) = (n * (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 - Q x * P z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2) + P y * Q z ^ 3 * d ^ 3) / (P z * Q z * d) ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>W.negAddY P Q / WeierstrassCurve.Jacobian.addZ P Q ^ 3 = W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>W'.addY P P = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>W'.addY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.addY P Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.addY P Q = (P x * Q z) ^ 3 * Q y
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hQ : W'.Equation Q<VAR>hQz : Q z = 0<GOAL>W'.addY P Q = (-(Q x * P z)) ^ 3 * P y
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W'.addY P Q * (P z * Q z) ^ 3 = (-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W.addY P Q = WeierstrassCurve.Jacobian.addU P Q ^ 3
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>W.addY P Q / WeierstrassCurve.Jacobian.addZ P Q ^ 3 = W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>W'.addXYZ P P = ![0, 0, 0]
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.addXYZ P Q = (P x * Q z) • Q
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P Q : Fin 3 → R<VAR>hQ : W'.Equation Q<VAR>hQz : Q z = 0<GOAL>W'.addXYZ P Q = -(Q x * P z) • P
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W.addXYZ P Q = WeierstrassCurve.Jacobian.addU P Q • ![1, 1, 0]
<VAR>F : Type v<VAR>Field F<VAR>W : WeierstrassCurve.Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2<GOAL>W.addXYZ P Q = WeierstrassCurve.Jacobian.addZ P Q • ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1]
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.neg (u • P) = u • W'.neg P
<VAR>R : Type u<VAR>CommRing R<VAR>W' : WeierstrassCurve.Jacobian R<VAR>P : Fin 3 → R<VAR>u : R<VAR>hu : IsUnit u<GOAL>W'.neg (u • P) ≈ W'.neg P