awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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 * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw :
  (-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) /
      HPow.hPow (β := ℕ) (W.dblZ P) 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)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
⊢ W.negDblY P / HPow.hPow (β := ℕ) (W.dblZ P) 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)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
have rw₁ : (-W.dblU P *
        (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 -
          P x * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
      P y * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
    HPow.hPow (β := ℕ) (W.dblZ P) 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)
    (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
Tactic: rw [negDblY, dblX, toAffine_slope_of_eq hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_negAddY_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hx hy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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 * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw :
  (-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) /
      HPow.hPow (β := ℕ) (W.dblZ P) 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)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
rw₁ :
  (-W.dblU P *
          (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 -
            P x * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (W.dblZ P) 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)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
⊢ W.negDblY P / HPow.hPow (β := ℕ) (W.dblZ P) 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)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
have rw₂ : (-W.dblU P *
        (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 -
          P x * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
      P y * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
    HPow.hPow (β := ℕ) (W.dblZ P) 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) (-W.dblU P / W.dblZ P)
Tactic: rw [negDblY, dblX, toAffine_slope_of_eq hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_negAddY_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hx hy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblY (u • P) = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.dblY P
have 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)
Tactic: simp only [dblY, negY_eq, negDblY_smul, dblX_smul, dblZ_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblY P = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 3
have 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
Tactic: rw [dblY, negY_eq, negDblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
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'.dblY P = HPow.hPow (β := ℕ) (W'.dblU P) 3
have 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
Tactic: rw [dblY, negY_eq, negDblY_of_Y_eq hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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 * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ W.dblY P / HPow.hPow (β := ℕ) (W.dblZ P) 3 =
    W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
have erw : W.negY ![W.dblX P, W.negDblY P, W.dblZ P] / HPow.hPow (β := ℕ) (W.dblZ P) 3 =
  W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
    (P y / HPow.hPow (β := ℕ) (P z) 3)
    (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
Tactic: erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hx hy,
    dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, negDblY_of_Z_ne_zero hP hQ hPz hQz hx hy, Affine.addY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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 * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W.negY Q * HPow.hPow (β := ℕ) (P z) 3
erw :
  W.negY ![W.dblX P, W.negDblY P, W.dblZ P] / HPow.hPow (β := ℕ) (W.dblZ P) 3 =
    W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
⊢ W.dblY P / HPow.hPow (β := ℕ) (W.dblZ P) 3 =
    W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
have erw₁ : W.toAffine.negY (![W.dblX P, W.negDblY P, W.dblZ P] x / HPow.hPow (β := ℕ) (![W.dblX P, W.negDblY P, W.dblZ P] z) 2)
    (![W.dblX P, W.negDblY P, W.dblZ P] y / HPow.hPow (β := ℕ) (![W.dblX P, W.negDblY P, W.dblZ P] z) 3) =
  W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
    (P y / HPow.hPow (β := ℕ) (P z) 3)
    (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
Tactic: erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hx hy,
    dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, negDblY_of_Z_ne_zero hP hQ hPz hQz hx hy, Affine.addY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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 * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W.negY Q * HPow.hPow (β := ℕ) (P z) 3
erw :
  W.negY ![W.dblX P, W.negDblY P, W.dblZ P] / HPow.hPow (β := ℕ) (W.dblZ P) 3 =
    W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
erw₁ :
  W.toAffine.negY (![W.dblX P, W.negDblY P, W.dblZ P] x / HPow.hPow (β := ℕ) (![W.dblX P, W.negDblY P, W.dblZ P] z) 2)
      (![W.dblX P, W.negDblY P, W.dblZ P] y / HPow.hPow (β := ℕ) (![W.dblX P, W.negDblY P, W.dblZ P] z) 3) =
    W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
⊢ W.dblY P / HPow.hPow (β := ℕ) (W.dblZ P) 3 =
    W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
have erw₂ : W.toAffine.negY
    (W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)))
    (![W.dblX P, W.negDblY P, W.dblZ P] y / HPow.hPow (β := ℕ) (![W.dblX P, W.negDblY P, W.dblZ P] z) 3) =
  W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
    (P y / HPow.hPow (β := ℕ) (P z) 3)
    (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3))
Tactic: erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hx hy,
    dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, negDblY_of_Z_ne_zero hP hQ hPz hQz hx hy, Affine.addY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have rw : ![W'.dblX (u • P), W'.dblY (u • P), W'.dblZ (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
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
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have 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
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
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
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have 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
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
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
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have 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
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
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
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have 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]
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
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]
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have 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]
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
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]
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have 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]
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
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]
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have 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]
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
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'.dblXYZ P = ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
have rw : ![W'.dblX P, W'.dblY P, W'.dblZ 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']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
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]
⊢ W'.dblXYZ P = ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
have 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]
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']