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
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) (- -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 3
⊢ W.negAddY P Q = HPow.hPow (β := ℕ) (-addU P Q) 3
have rw₁ : W.negAddY P Q =
  HPow.hPow (β := ℕ) ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 3
Tactic: rw [addU, neg_neg, div_pow, ← negAddY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) (- -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 3
rw₁ :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 3
⊢ W.negAddY P Q = HPow.hPow (β := ℕ) (-addU P Q) 3
have rw₂ : W.negAddY P Q =
  HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3 /
    HPow.hPow (β := ℕ) (P z * Q z) 3
Tactic: rw [addU, neg_neg, div_pow, ← negAddY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) (- -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 3
rw₁ :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 3
rw₂ :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3 /
      HPow.hPow (β := ℕ) (P z * Q z) 3
⊢ W.negAddY P Q = HPow.hPow (β := ℕ) (-addU P Q) 3
have rw₃ : W.negAddY P Q = W.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / HPow.hPow (β := ℕ) (P z * Q z) 3
Tactic: rw [addU, neg_neg, div_pow, ← negAddY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) (- -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 3
rw₁ :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 3
rw₂ :
  W.negAddY P Q =
    HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3 /
      HPow.hPow (β := ℕ) (P z * Q z) 3
rw₃ : W.negAddY P Q = W.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / HPow.hPow (β := ℕ) (P z * Q z) 3
⊢ W.negAddY P Q = HPow.hPow (β := ℕ) (-addU P Q) 3
have rw₄ : W.negAddY P Q = W.negAddY P Q
Tactic: rw [addU, neg_neg, div_pow, ← negAddY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.negAddY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
      (P y / HPow.hPow (β := ℕ) (P z) 3) (n / (P z * Q z * d)) =
    (n *
            (HPow.hPow (β := ℕ) n 2 + W.a₁ * n * P z * Q z * d -
                    W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) d 2 -
                  P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) d 2 -
                Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 -
              P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) d 2) +
          P y * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) d 3) /
        HPow.hPow (β := ℕ) (P z * Q z) 3 /
      HPow.hPow (β := ℕ) d 3
have rw : n / (P z * Q z * d) *
      ((HPow.hPow (β := ℕ) n 2 + W.a₁ * n * P z * Q z * d -
                  W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) d 2 -
                P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) d 2 -
              Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2) /
            HPow.hPow (β := ℕ) (P z * Q z) 2 /
          HPow.hPow (β := ℕ) d 2 -
        P x / HPow.hPow (β := ℕ) (P z) 2) +
    P y / HPow.hPow (β := ℕ) (P z) 3 =
  (n *
          (HPow.hPow (β := ℕ) n 2 + W.a₁ * n * P z * Q z * d -
                  W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) d 2 -
                P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) d 2 -
              Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 -
            P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) d 2) +
        P y * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) d 3) /
      HPow.hPow (β := ℕ) (P z * Q z) 3 /
    HPow.hPow (β := ℕ) d 3
Tactic: rw [Affine.negAddY, toAffine_addX_of_ne hPz hQz 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
⊢ W.negAddY P Q / HPow.hPow (β := ℕ) (addZ P Q) 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 : ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) *
          (W.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 -
            P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2) +
        P y * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) (addZ P Q) 3) /
      HPow.hPow (β := ℕ) (P z * Q z) 3 /
    HPow.hPow (β := ℕ) (addZ P Q) 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 [negAddY_eq hPz hQz, addX_eq' hP hQ, toAffine_slope_of_ne hPz hQz hx,
    toAffine_negAddY_of_ne hPz hQz <| addZ_ne_zero_of_X_ne hx]
-- 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
rw :
  ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) *
            (W.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 -
              P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2) +
          P y * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) (addZ P Q) 3) /
        HPow.hPow (β := ℕ) (P z * Q z) 3 /
      HPow.hPow (β := ℕ) (addZ P Q) 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.negAddY P Q / HPow.hPow (β := ℕ) (addZ P Q) 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₁ : ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) *
          (HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 +
                    W.a₁ * (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) * P z * Q z *
                      addZ P Q -
                  W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
                P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
              Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
            P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2) +
        P y * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) (addZ P Q) 3) /
      HPow.hPow (β := ℕ) (P z * Q z) 3 /
    HPow.hPow (β := ℕ) (addZ P Q) 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 [negAddY_eq hPz hQz, addX_eq' hP hQ, toAffine_slope_of_ne hPz hQz hx,
    toAffine_negAddY_of_ne hPz hQz <| addZ_ne_zero_of_X_ne hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ W'.addY (u • P) (v • Q) = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q
have simp : -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.negAddY P Q) -
      W'.a₁ * (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q) *
        (HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q) -
    W'.a₃ * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q) 3 =
  HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 *
    (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * HPow.hPow (β := ℕ) (addZ P Q) 3)
Tactic: simp only [addY, negY_eq, negAddY_smul, addX_smul, addZ_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
⊢ W'.addY P P = 0
have rw : -0 - W'.a₁ * 0 * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = 0
Tactic: rw [addY, negY_eq, addX_self hP, negAddY_self, addZ_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addY P Q = HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y
have rw : -(HPow.hPow (β := ℕ) (P x * Q z) 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * HPow.hPow (β := ℕ) (Q z) 3)) -
      W'.a₁ * (HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x) * (P x * Q z * Q z) -
    W'.a₃ * HPow.hPow (β := ℕ) (P x * Q z * Q z) 3 =
  HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y
Tactic: rw [addY, negY_eq, negAddY_of_Z_eq_zero_left hP hPz, negY, addX_of_Z_eq_zero_left hPz,
    addZ_of_Z_eq_zero_left hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addY P Q = HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y
have rw : -(HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) -
      W'.a₁ * (HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x) * (-(Q x * P z) * P z) -
    W'.a₃ * HPow.hPow (β := ℕ) (-(Q x * P z) * P z) 3 =
  HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y
Tactic: rw [addY, negY_eq, negAddY_of_Z_eq_zero_right hQ hQz, negY, addX_of_Z_eq_zero_right hQz,
    addZ_of_Z_eq_zero_right hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ W'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 + W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 -
      (HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3 +
        HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3) =
    0
have a : (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3) *
        HPow.hPow (β := ℕ) (P z * Q z) 3 +
      W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 -
    (HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3 +
      HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3) =
  0
Tactic: rw [addY, negY_eq, addZ_of_X_eq hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ W'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 =
    HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3
have a : W'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 + W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 -
    (HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3 +
      HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3) =
  0
Tactic: linear_combination (norm := (rw [addY, negY_eq, addZ_of_X_eq hx]; ring1))
    -negAddY_of_X_eq' hP hQ hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ W.addY P Q = HPow.hPow (β := ℕ) (addU P Q) 3
have rw : W.addY P Q =
  HPow.hPow (β := ℕ) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 3
Tactic: rw [addU, ← neg_div, div_pow, ← addY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 3
⊢ W.addY P Q = HPow.hPow (β := ℕ) (addU P Q) 3
have rw₁ : W.addY P Q = HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 3
Tactic: rw [addU, ← neg_div, div_pow, ← addY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 3
rw₁ :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 3
⊢ W.addY P Q = HPow.hPow (β := ℕ) (addU P Q) 3
have rw₂ : W.addY P Q =
  HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3 /
    HPow.hPow (β := ℕ) (P z * Q z) 3
Tactic: rw [addU, ← neg_div, div_pow, ← addY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 3
rw₁ :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 3
rw₂ :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3 /
      HPow.hPow (β := ℕ) (P z * Q z) 3
⊢ W.addY P Q = HPow.hPow (β := ℕ) (addU P Q) 3
have rw₃ : W.addY P Q = W.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / HPow.hPow (β := ℕ) (P z * Q z) 3
Tactic: rw [addU, ← neg_div, div_pow, ← addY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 3
rw₁ :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 3
rw₂ :
  W.addY P Q =
    HPow.hPow (β := ℕ) (-(P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3)) 3 /
      HPow.hPow (β := ℕ) (P z * Q z) 3
rw₃ : W.addY P Q = W.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / HPow.hPow (β := ℕ) (P z * Q z) 3
⊢ W.addY P Q = HPow.hPow (β := ℕ) (addU P Q) 3
have rw₄ : W.addY P Q = W.addY P Q
Tactic: rw [addU, ← neg_div, div_pow, ← addY_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]
-- 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
⊢ W.addY P Q / HPow.hPow (β := ℕ) (addZ P Q) 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.addX P Q, W.negAddY P Q, addZ P Q] / HPow.hPow (β := ℕ) (addZ P Q) 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 [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
    negAddY_of_Z_ne_zero hP hQ hPz hQz hx, 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
erw :
  W.negY ![W.addX P Q, W.negAddY P Q, addZ P Q] / HPow.hPow (β := ℕ) (addZ P Q) 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.addY P Q / HPow.hPow (β := ℕ) (addZ P Q) 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.addX P Q, W.negAddY P Q, addZ P Q] x / HPow.hPow (β := ℕ) (![W.addX P Q, W.negAddY P Q, addZ P Q] z) 2)
    (![W.addX P Q, W.negAddY P Q, addZ P Q] y / HPow.hPow (β := ℕ) (![W.addX P Q, W.negAddY P Q, addZ P Q] 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 [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
    negAddY_of_Z_ne_zero hP hQ hPz hQz hx, 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
erw :
  W.negY ![W.addX P Q, W.negAddY P Q, addZ P Q] / HPow.hPow (β := ℕ) (addZ P Q) 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.addX P Q, W.negAddY P Q, addZ P Q] x / HPow.hPow (β := ℕ) (![W.addX P Q, W.negAddY P Q, addZ P Q] z) 2)
      (![W.addX P Q, W.negAddY P Q, addZ P Q] y / HPow.hPow (β := ℕ) (![W.addX P Q, W.negAddY P Q, addZ P Q] 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.addY P Q / HPow.hPow (β := ℕ) (addZ P Q) 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.addX P Q, W.negAddY P Q, addZ P Q] y / HPow.hPow (β := ℕ) (![W.addX P Q, W.negAddY P Q, addZ P Q] 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 [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
    negAddY_of_Z_ne_zero hP hQ hPz hQz hx, Affine.addY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
have rw : ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
Tactic: rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]