awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hPz : P z = 0
⊢ W'.addX P Q = HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x
have rw : P x * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 - 2 * P y * Q y * 0 * Q z +
                    HPow.hPow (β := ℕ) (P x) 2 * Q x * HPow.hPow (β := ℕ) (Q z) 2 -
                  W'.a₁ * P x * Q y * HPow.hPow (α := R) (β := ℕ) 0 2 * Q z -
                W'.a₁ * P y * Q x * 0 * HPow.hPow (β := ℕ) (Q z) 2 +
              2 * W'.a₂ * P x * Q x * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) (Q z) 2 -
            W'.a₃ * Q y * HPow.hPow (α := R) (β := ℕ) 0 4 * Q z -
          W'.a₃ * P y * 0 * HPow.hPow (β := ℕ) (Q z) 4 +
        W'.a₄ * Q x * HPow.hPow (α := R) (β := ℕ) 0 4 * HPow.hPow (β := ℕ) (Q z) 2 +
      W'.a₄ * P x * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) (Q z) 4 +
    2 * W'.a₆ * HPow.hPow (α := R) (β := ℕ) 0 4 * HPow.hPow (β := ℕ) (Q z) 4 =
  HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x
Tactic: rw [addX, 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
hQz : Q z = 0
⊢ W'.addX P Q = HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x
have rw : P x * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 - 2 * P y * Q y * P z * 0 +
                    HPow.hPow (β := ℕ) (P x) 2 * Q x * HPow.hPow (α := R) (β := ℕ) 0 2 -
                  W'.a₁ * P x * Q y * HPow.hPow (β := ℕ) (P z) 2 * 0 -
                W'.a₁ * P y * Q x * P z * HPow.hPow (α := R) (β := ℕ) 0 2 +
              2 * W'.a₂ * P x * Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
            W'.a₃ * Q y * HPow.hPow (β := ℕ) (P z) 4 * 0 -
          W'.a₃ * P y * P z * HPow.hPow (α := R) (β := ℕ) 0 4 +
        W'.a₄ * Q x * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (α := R) (β := ℕ) 0 2 +
      W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (α := R) (β := ℕ) 0 4 +
    2 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (α := R) (β := ℕ) 0 4 =
  HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x
Tactic: rw [addX, 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'.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 =
    HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2
have rw : 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 * 0 -
        W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
      P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
    Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 =
  HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2
Tactic: rw [addX_eq' hP hQ, addZ_of_X_eq 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.addX P Q = HPow.hPow (β := ℕ) (addU P Q) 2
have rw : W.addX P Q =
  HPow.hPow (β := ℕ) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 2
Tactic: rw [addU, neg_sq, div_pow, ← addX_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| 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.addX P Q =
    HPow.hPow (β := ℕ) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 2
⊢ W.addX P Q = HPow.hPow (β := ℕ) (addU P Q) 2
have rw₁ : W.addX P Q = HPow.hPow (β := ℕ) ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 2
Tactic: rw [addU, neg_sq, div_pow, ← addX_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| 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.addX P Q =
    HPow.hPow (β := ℕ) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 2
rw₁ :
  W.addX P Q =
    HPow.hPow (β := ℕ) ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 2
⊢ W.addX P Q = HPow.hPow (β := ℕ) (addU P Q) 2
have rw₂ : W.addX P Q =
  HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 /
    HPow.hPow (β := ℕ) (P z * Q z) 2
Tactic: rw [addU, neg_sq, div_pow, ← addX_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| 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.addX P Q =
    HPow.hPow (β := ℕ) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 2
rw₁ :
  W.addX P Q =
    HPow.hPow (β := ℕ) ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 2
rw₂ :
  W.addX P Q =
    HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 /
      HPow.hPow (β := ℕ) (P z * Q z) 2
⊢ W.addX P Q = HPow.hPow (β := ℕ) (addU P Q) 2
have rw₃ : W.addX P Q = W.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 / HPow.hPow (β := ℕ) (P z * Q z) 2
Tactic: rw [addU, neg_sq, div_pow, ← addX_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| 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.addX P Q =
    HPow.hPow (β := ℕ) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z))) 2
rw₁ :
  W.addX P Q =
    HPow.hPow (β := ℕ) ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) 2
rw₂ :
  W.addX P Q =
    HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 /
      HPow.hPow (β := ℕ) (P z * Q z) 2
rw₃ : W.addX P Q = W.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 / HPow.hPow (β := ℕ) (P z * Q z) 2
⊢ W.addX P Q = HPow.hPow (β := ℕ) (addU P Q) 2
have rw₄ : W.addX P Q = W.addX P Q
Tactic: rw [addU, neg_sq, div_pow, ← addX_of_X_eq' hP hQ hx,
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| 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.addX P Q / HPow.hPow (β := ℕ) (addZ P Q) 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 (β := ℕ) (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) /
      HPow.hPow (β := ℕ) (P z * Q z) 2 /
    HPow.hPow (β := ℕ) (addZ P Q) 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 [addX_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
    toAffine_addX_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 :
  (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) /
        HPow.hPow (β := ℕ) (P z * Q z) 2 /
      HPow.hPow (β := ℕ) (addZ P Q) 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.addX P Q / HPow.hPow (β := ℕ) (addZ P Q) 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 (β := ℕ) (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) /
      HPow.hPow (β := ℕ) (P z * Q z) 2 /
    HPow.hPow (β := ℕ) (addZ P Q) 2 =
  W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
    ((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z * addZ P Q))
Tactic: rw [addX_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
    toAffine_addX_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
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.negAddY P Q =
    ((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
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 [← negAddY_eq', 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
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 =
    ((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
have rw₁ : W.negAddY P Q = W.negAddY P Q
Tactic: rw [← negAddY_eq', 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:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.negAddY P P = 0
have rw : -P y * HPow.hPow (β := ℕ) (P x) 3 * HPow.hPow (β := ℕ) (P z) 3 +
                                        2 * P y * HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 3 -
                                      3 * HPow.hPow (β := ℕ) (P x) 2 * P x * P y * HPow.hPow (β := ℕ) (P z) 2 * P z +
                                    3 * P x * P y * HPow.hPow (β := ℕ) (P x) 2 * P z * HPow.hPow (β := ℕ) (P z) 2 +
                                  HPow.hPow (β := ℕ) (P x) 3 * P y * HPow.hPow (β := ℕ) (P z) 3 -
                                2 * HPow.hPow (β := ℕ) (P y) 2 * P y * HPow.hPow (β := ℕ) (P z) 3 +
                              W'.a₁ * P x * HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 4 +
                            W'.a₁ * P y * P x * P y * HPow.hPow (β := ℕ) (P z) 3 * P z -
                          W'.a₁ * P x * P y * P y * P z * HPow.hPow (β := ℕ) (P z) 3 -
                        W'.a₁ * HPow.hPow (β := ℕ) (P y) 2 * P x * HPow.hPow (β := ℕ) (P z) 4 -
                      2 * W'.a₂ * P x * P x * P y * HPow.hPow (β := ℕ) (P z) 4 * P z +
                    2 * W'.a₂ * P x * P y * P x * P z * HPow.hPow (β := ℕ) (P z) 4 +
                  W'.a₃ * HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 6 -
                W'.a₃ * HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 6 -
              W'.a₄ * P x * P y * HPow.hPow (β := ℕ) (P z) 6 * P z -
            W'.a₄ * P x * P y * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (P z) 3 +
          W'.a₄ * P y * P x * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (β := ℕ) (P z) 4 +
        W'.a₄ * P x * P y * P z * HPow.hPow (β := ℕ) (P z) 6 -
      2 * W'.a₆ * P y * HPow.hPow (β := ℕ) (P z) 6 * HPow.hPow (β := ℕ) (P z) 3 +
    2 * W'.a₆ * P y * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (β := ℕ) (P z) 6 =
  0
Tactic: rw [negAddY]
-- 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'.negAddY P Q + (W'.negY Q - Q y) * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) (P x) 3 -
      (HPow.hPow (β := ℕ) (P x * Q z) 3 * W'.negY Q +
        (W'.negY Q - Q y) * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) (P y) 2) =
    0
have a : -P y * HPow.hPow (β := ℕ) (Q x) 3 * HPow.hPow (α := R) (β := ℕ) 0 3 +
                                            2 * P y * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (α := R) (β := ℕ) 0 3 -
                                          3 * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q y * HPow.hPow (α := R) (β := ℕ) 0 2 *
                                            Q z +
                                        3 * P x * P y * HPow.hPow (β := ℕ) (Q x) 2 * 0 * HPow.hPow (β := ℕ) (Q z) 2 +
                                      HPow.hPow (β := ℕ) (P x) 3 * Q y * HPow.hPow (β := ℕ) (Q z) 3 -
                                    2 * HPow.hPow (β := ℕ) (P y) 2 * Q y * HPow.hPow (β := ℕ) (Q z) 3 +
                                  W'.a₁ * P x * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (α := R) (β := ℕ) 0 4 +
                                W'.a₁ * P y * Q x * Q y * HPow.hPow (α := R) (β := ℕ) 0 3 * Q z -
                              W'.a₁ * P x * P y * Q y * 0 * HPow.hPow (β := ℕ) (Q z) 3 -
                            W'.a₁ * HPow.hPow (β := ℕ) (P y) 2 * Q x * HPow.hPow (β := ℕ) (Q z) 4 -
                          2 * W'.a₂ * P x * Q x * Q y * HPow.hPow (α := R) (β := ℕ) 0 4 * Q z +
                        2 * W'.a₂ * P x * P y * Q x * 0 * HPow.hPow (β := ℕ) (Q z) 4 +
                      W'.a₃ * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (α := R) (β := ℕ) 0 6 -
                    W'.a₃ * HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (Q z) 6 -
                  W'.a₄ * Q x * Q y * HPow.hPow (α := R) (β := ℕ) 0 6 * Q z -
                W'.a₄ * P x * Q y * HPow.hPow (α := R) (β := ℕ) 0 4 * HPow.hPow (β := ℕ) (Q z) 3 +
              W'.a₄ * P y * Q x * HPow.hPow (α := R) (β := ℕ) 0 3 * HPow.hPow (β := ℕ) (Q z) 4 +
            W'.a₄ * P x * P y * 0 * HPow.hPow (β := ℕ) (Q z) 6 -
          2 * W'.a₆ * Q y * HPow.hPow (α := R) (β := ℕ) 0 6 * HPow.hPow (β := ℕ) (Q z) 3 +
        2 * W'.a₆ * P y * HPow.hPow (α := R) (β := ℕ) 0 3 * HPow.hPow (β := ℕ) (Q z) 6 +
      (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * HPow.hPow (β := ℕ) (Q z) 3 - Q y) * HPow.hPow (β := ℕ) (Q z) 3 *
        HPow.hPow (β := ℕ) (P x) 3 -
    (HPow.hPow (β := ℕ) (P x * Q z) 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * HPow.hPow (β := ℕ) (Q z) 3) +
      (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * HPow.hPow (β := ℕ) (Q z) 3 - Q y) * HPow.hPow (β := ℕ) (Q z) 3 *
        HPow.hPow (β := ℕ) (P y) 2) =
  0
Tactic: rw [negAddY, negY, 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
hP : W'.Equation P
hPz : P z = 0
⊢ W'.negAddY P Q = HPow.hPow (β := ℕ) (P x * Q z) 3 * W'.negY Q
have a : W'.negAddY P Q + (W'.negY Q - Q y) * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) (P x) 3 -
    (HPow.hPow (β := ℕ) (P x * Q z) 3 * W'.negY Q +
      (W'.negY Q - Q y) * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (β := ℕ) (P y) 2) =
  0
Tactic: linear_combination (norm := (rw [negAddY, negY, hPz]; ring1))
    (W'.negY Q - Q y) * Q z ^ 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
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.negAddY P Q + (P y - W'.negY P) * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (β := ℕ) (Q x) 3 -
      (HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * W'.negY P +
        (P y - W'.negY P) * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (β := ℕ) (Q y) 2) =
    0
have a : -P y * HPow.hPow (β := ℕ) (Q x) 3 * HPow.hPow (β := ℕ) (P z) 3 +
                                            2 * P y * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 3 -
                                          3 * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q y * HPow.hPow (β := ℕ) (P z) 2 * 0 +
                                        3 * P x * P y * HPow.hPow (β := ℕ) (Q x) 2 * P z *
                                          HPow.hPow (α := R) (β := ℕ) 0 2 +
                                      HPow.hPow (β := ℕ) (P x) 3 * Q y * HPow.hPow (α := R) (β := ℕ) 0 3 -
                                    2 * HPow.hPow (β := ℕ) (P y) 2 * Q y * HPow.hPow (α := R) (β := ℕ) 0 3 +
                                  W'.a₁ * P x * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 4 +
                                W'.a₁ * P y * Q x * Q y * HPow.hPow (β := ℕ) (P z) 3 * 0 -
                              W'.a₁ * P x * P y * Q y * P z * HPow.hPow (α := R) (β := ℕ) 0 3 -
                            W'.a₁ * HPow.hPow (β := ℕ) (P y) 2 * Q x * HPow.hPow (α := R) (β := ℕ) 0 4 -
                          2 * W'.a₂ * P x * Q x * Q y * HPow.hPow (β := ℕ) (P z) 4 * 0 +
                        2 * W'.a₂ * P x * P y * Q x * P z * HPow.hPow (α := R) (β := ℕ) 0 4 +
                      W'.a₃ * HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 6 -
                    W'.a₃ * HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (α := R) (β := ℕ) 0 6 -
                  W'.a₄ * Q x * Q y * HPow.hPow (β := ℕ) (P z) 6 * 0 -
                W'.a₄ * P x * Q y * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (α := R) (β := ℕ) 0 3 +
              W'.a₄ * P y * Q x * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (α := R) (β := ℕ) 0 4 +
            W'.a₄ * P x * P y * P z * HPow.hPow (α := R) (β := ℕ) 0 6 -
          2 * W'.a₆ * Q y * HPow.hPow (β := ℕ) (P z) 6 * HPow.hPow (α := R) (β := ℕ) 0 3 +
        2 * W'.a₆ * P y * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (α := R) (β := ℕ) 0 6 +
      (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) * HPow.hPow (β := ℕ) (P z) 3 *
        HPow.hPow (β := ℕ) (Q x) 3 -
    (HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) +
      (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) * HPow.hPow (β := ℕ) (P z) 3 *
        HPow.hPow (β := ℕ) (Q y) 2) =
  0
Tactic: rw [negAddY, negY, 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
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.negAddY P Q = HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * W'.negY P
have a : W'.negAddY P Q + (P y - W'.negY P) * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (β := ℕ) (Q x) 3 -
    (HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * W'.negY P +
      (P y - W'.negY P) * HPow.hPow (β := ℕ) (P z) 3 * HPow.hPow (β := ℕ) (Q y) 2) =
  0
Tactic: linear_combination (norm := (rw [negAddY, negY, hQz]; ring1))
    (P y - W'.negY P) * P z ^ 3 * (equation_of_Z_eq_zero hQz).mp hQ
-- 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'.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
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 * 0 -
              W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
            P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
          Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
        P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (α := R) (β := ℕ) 0 2) +
    P y * HPow.hPow (β := ℕ) (Q z) 3 * HPow.hPow (α := R) (β := ℕ) 0 3 =
  HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 3
Tactic: rw [negAddY_eq', addX_eq' hP hQ, addZ_of_X_eq 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.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]