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
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x / HPow.hPow (β := ℕ) (P z) 2 = Q x / HPow.hPow (β := ℕ) (Q z) 2
hy :
  ¬P y / HPow.hPow (β := ℕ) (P z) 3 =
      W.toAffine.negY (Q x / HPow.hPow (β := ℕ) (Q z) 2) (Q y / HPow.hPow (β := ℕ) (Q 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.dblU P / W.dblZ P
have rw : (3 * HPow.hPow (β := ℕ) (P x / HPow.hPow (β := ℕ) (P z) 2) 2 + 2 * W.toAffine.a₂ * (P x / HPow.hPow (β := ℕ) (P z) 2) +
        W.toAffine.a₄ -
      W.toAffine.a₁ * (P y / HPow.hPow (β := ℕ) (P z) 3)) /
    (P y / HPow.hPow (β := ℕ) (P z) 3 - W.negY P / HPow.hPow (β := ℕ) (P z) 3) =
  -(W.a₁ * P y * P z -
        (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W.a₄ * HPow.hPow (β := ℕ) (P z) 4)) /
    (P z * (P y - W.negY P))
Tactic: rw [Affine.slope_of_Y_ne hx <| negY_of_Z_ne_zero hQz ▸ hy, ← negY_of_Z_ne_zero hPz, dblU_eq, dblZ]
-- 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'.dblX (u • P) = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 2 * W'.dblX P
have simp : 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: simp only [dblX, dblU_smul, negY_smul, smul_fin3_ext]
-- 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'.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
have 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
Tactic: rw [dblX, dblU_of_Z_eq_zero hPz, negY_of_Z_eq_zero hPz, hPz]
-- 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'.dblX P = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 2
have 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
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
-- 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'.dblX P = HPow.hPow (β := ℕ) (W'.dblU P) 2
have 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
Tactic: rw [dblX, Y_eq_negY_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
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ 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
have 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
Tactic: simp [field]
-- 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.dblX P / HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    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))
have rw : (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) /
    HPow.hPow (β := ℕ) (W.dblZ P) 2 =
  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))
Tactic: rw [dblX, toAffine_slope_of_eq hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_addX_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 :
  (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) /
      HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    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 / HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    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))
have rw₁ : (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) /
    HPow.hPow (β := ℕ) (W.dblZ P) 2 =
  W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2) (-W.dblU P / W.dblZ P)
Tactic: rw [dblX, toAffine_slope_of_eq hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_addX_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 :
  (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) /
      HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    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))
rw₁ :
  (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) /
      HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2) (-W.dblU P / W.dblZ P)
⊢ W.dblX P / HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    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))
have rw₂ : (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) /
    HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 2 =
  W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
    (-W.dblU P / (P z * (P y - W.negY P)))
Tactic: rw [dblX, toAffine_slope_of_eq hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_addX_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 :
  (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) /
      HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    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))
rw₁ :
  (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) /
      HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2) (-W.dblU P / W.dblZ P)
rw₂ :
  (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) /
      HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 2 =
    W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (-W.dblU P / (P z * (P y - W.negY P)))
⊢ W.dblX P / HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    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))
have rw₃ : (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) /
    HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 2 =
  W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (P x / HPow.hPow (β := ℕ) (P z) 2)
    (-W.dblU P / (P z * (P y - W.negY P)))
Tactic: rw [dblX, toAffine_slope_of_eq hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_addX_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 :
  (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) /
      HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    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))
rw₁ :
  (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) /
      HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2) (-W.dblU P / W.dblZ P)
rw₂ :
  (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) /
      HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 2 =
    W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (-W.dblU P / (P z * (P y - W.negY P)))
rw₃ :
  (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) /
      HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 2 =
    W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (P x / HPow.hPow (β := ℕ) (P z) 2)
      (-W.dblU P / (P z * (P y - W.negY P)))
⊢ W.dblX P / HPow.hPow (β := ℕ) (W.dblZ P) 2 =
    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))
have rw₄ : (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) /
    HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 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) /
    HPow.hPow (β := ℕ) (P z * (P y - W.negY P)) 2
Tactic: rw [dblX, toAffine_slope_of_eq hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_addX_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'.negDblY (u • P) = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 4) 3 * W'.negDblY P
have 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)
Tactic: simp only [negDblY, dblU_smul, dblX_smul, negY_smul, smul_fin3_ext]
-- 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'.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
have 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
Tactic: rw [negDblY, dblU_of_Z_eq_zero hPz, dblX_of_Z_eq_zero hP hPz, negY_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
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negDblY P = -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (P x) 2) 3
have 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
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
-- 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'.negDblY P = HPow.hPow (β := ℕ) (-W'.dblU P) 3
have 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
Tactic: rw [negDblY, dblX_of_Y_eq hQz hx hy hy', Y_eq_negY_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
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ 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
have 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
Tactic: rw [Affine.negAddY, toAffine_addX_of_eq hPz hd]
-- 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.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 * (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))
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]