awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 =
    HMul.hMul (α := R) (-(eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R)
        (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 2 -
                HMul.hMul (β := R) W'.a₁ ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) * 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 * P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
          P x * P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 2) +
      P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 3
have a : W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 +
      -9 *
          (HPow.hPow (β := ℕ) (P y) 2 * P z + 2 * W'.a₁ * P x * P y * P z - 3 * HPow.hPow (β := ℕ) (P x) 3 -
            3 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z) *
        0 -
    (HMul.hMul (α := R) (-(eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R)
          (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 2 -
                  HMul.hMul (β := R) W'.a₁ ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) * 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 * P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
            P x * P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 +
      -9 *
          (HPow.hPow (β := ℕ) (P y) 2 * P z + 2 * W'.a₁ * P x * P y * P z - 3 * HPow.hPow (β := ℕ) (P x) 3 -
            3 * W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z) *
        (HPow.hPow (β := ℕ) (P y) 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 -
          (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P z +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₆ * HPow.hPow (β := ℕ) (P z) 3))) =
  0
Tactic: linear_combination (norm := (rw [negDblY, eval_polynomialX, negY]; ring1))
    -9 * (P y ^ 2 * P z + 2 * W'.a₁ * P x * P y * P z - 3 * P x ^ 3 - 3 * W'.a₂ * P x ^ 2 * P z)
      * (equation_iff _).mp hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
⊢ W.negDblY P =
    (HMul.hMul (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F)
          (HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                  HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * 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 * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (P z) 2
have rw : W.negDblY P = W.negDblY P * HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2
Tactic: rw [← negDblY_eq' hP, mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
rw : W.negDblY P = W.negDblY P * HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2
⊢ W.negDblY P =
    (HMul.hMul (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F)
          (HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                  HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * 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 * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (P z) 2
have rw₁ : W.negDblY P = W.negDblY P
Tactic: rw [← negDblY_eq' hP, mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 =
    -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3
have rw : HMul.hMul (α := R) (-(eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R)
      (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 2 -
              HMul.hMul (β := R) W'.a₁ ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) * 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 * P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2 -
        P x * P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 2) +
    W'.negY P * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 3 =
  -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3
Tactic: rw [negDblY_eq' hP, Y_eq_negY_of_Y_eq hQz hx hy hy']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.negDblY P = -W.dblU P
have rw : W.negDblY P =
  -(HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
      HPow.hPow (β := ℕ) (P z) 2)
Tactic: rw [dblU, ← neg_div, ← negDblY_of_Y_eq' hP hQz hx hy hy',
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
rw :
  W.negDblY P =
    -(HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
        HPow.hPow (β := ℕ) (P z) 2)
⊢ W.negDblY P = -W.dblU P
have rw₁ : W.negDblY P =
  -HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
    HPow.hPow (β := ℕ) (P z) 2
Tactic: rw [dblU, ← neg_div, ← negDblY_of_Y_eq' hP hQz hx hy hy',
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
rw :
  W.negDblY P =
    -(HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
        HPow.hPow (β := ℕ) (P z) 2)
rw₁ :
  W.negDblY P =
    -HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
      HPow.hPow (β := ℕ) (P z) 2
⊢ W.negDblY P = -W.dblU P
have rw₂ : W.negDblY P = W.negDblY P * HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2
Tactic: rw [dblU, ← neg_div, ← negDblY_of_Y_eq' hP hQz hx hy hy',
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
rw :
  W.negDblY P =
    -(HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
        HPow.hPow (β := ℕ) (P z) 2)
rw₁ :
  W.negDblY P =
    -HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
      HPow.hPow (β := ℕ) (P z) 2
rw₂ : W.negDblY P = W.negDblY P * HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2
⊢ W.negDblY P = -W.dblU P
have rw₃ : W.negDblY P = W.negDblY P
Tactic: rw [dblU, ← neg_div, ← negDblY_of_Y_eq' hP hQz hx hy hy',
    mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.negAddY (P x / P z) (P x / P z) (P y / P z) (-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 * P z * HPow.hPow (β := ℕ) d 2 -
              P x * P z * HPow.hPow (β := ℕ) d 2) +
          P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 3) /
        HPow.hPow (β := ℕ) (P z) 2 /
      (P z * HPow.hPow (β := ℕ) 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 * P z * HPow.hPow (β := ℕ) d 2) *
              d /
            P z /
          (P z * HPow.hPow (β := ℕ) d 3) -
        P x / P z) +
    P y / P z =
  (-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 * P z * HPow.hPow (β := ℕ) d 2 -
            P x * P z * HPow.hPow (β := ℕ) d 2) +
        P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 3) /
      HPow.hPow (β := ℕ) (P z) 2 /
    (P z * HPow.hPow (β := ℕ) d 3)
Tactic: rw [Affine.negAddY, toAffine_addX_of_eq hPz hd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.negDblY P / W.dblZ P =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
have rw : (HMul.hMul (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F)
          (HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                  HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * 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 * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (P z) 2 /
    W.dblZ P =
  W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
    (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
Tactic: rw [negDblY_eq hP hPz, dblZ, toAffine_slope_of_eq hPz hQz hx hy, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_negAddY_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hPz hQz hx hy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
rw :
  (HMul.hMul (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F)
            (HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                    HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * 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 * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
              P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
          P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
        HPow.hPow (β := ℕ) (P z) 2 /
      W.dblZ P =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
⊢ W.negDblY P / W.dblZ P =
    W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
have rw₁ : (HMul.hMul (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F)
          (HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 2 -
                  HMul.hMul (β := F) W.a₁ ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) * 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 * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2 -
            P x * P z * HPow.hPow (β := ℕ) (P y - W.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W.negY P) 3) /
      HPow.hPow (β := ℕ) (P z) 2 /
    (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3) =
  W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
    (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
Tactic: rw [negDblY_eq hP hPz, dblZ, toAffine_slope_of_eq hPz hQz hx hy, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_negAddY_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hPz hQz hx hy]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ W'.dblY (u • P) = HPow.hPow (β := ℕ) u 4 * W'.dblY P
have simp : -(HPow.hPow (β := ℕ) u 4 * W'.negDblY P) - W'.a₁ * (HPow.hPow (β := ℕ) u 4 * W'.dblX P) -
    W'.a₃ * (HPow.hPow (β := ℕ) u 4 * W'.dblZ P) =
  HPow.hPow (β := ℕ) u 4 * (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P)
Tactic: simp only [dblY, negY_eq, negDblY_smul, dblX_smul, dblZ_smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblY P = HPow.hPow (β := ℕ) (P y) 4
have rw : - -HPow.hPow (β := ℕ) (P y) 4 - W'.a₁ * 0 - W'.a₃ * 0 = HPow.hPow (β := ℕ) (P y) 4
Tactic: rw [dblY, negY_eq, negDblY_of_Z_eq_zero hP hPz, dblX_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.dblY P * HPow.hPow (β := ℕ) (P z) 2 + W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 -
      (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3 +
        -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3) =
    0
have a : (-W'.negDblY P - W'.a₁ * 0 - W'.a₃ * 0) * HPow.hPow (β := ℕ) (P z) 2 + W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 -
    (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3 +
      -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3) =
  0
Tactic: rw [dblY, negY_eq, dblX_of_Y_eq hP hPz hQz hx hy hy',
    dblZ_of_Y_eq hQz hx hy hy']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W'.negY Q * P z
⊢ W'.dblY P * HPow.hPow (β := ℕ) (P z) 2 =
    HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3
have a : W'.dblY P * HPow.hPow (β := ℕ) (P z) 2 + W'.negDblY P * HPow.hPow (β := ℕ) (P z) 2 -
    (HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3 +
      -HPow.hPow (α := R) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) R) → R) W'.polynomialX : R) 3) =
  0
Tactic: linear_combination (norm := (rw [dblY, negY_eq, dblX_of_Y_eq hP hPz hQz hx hy hy',
    dblZ_of_Y_eq hQz hx hy hy']; ring1)) -negDblY_of_Y_eq' hP hQz hx hy hy'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
⊢ W.dblY P = W.dblU P
have rw : W.dblY P =
  HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
    HPow.hPow (β := ℕ) (P z) 2
Tactic: rw [dblU, ← dblY_of_Y_eq' hP hPz hQz hx hy hy', mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
rw :
  W.dblY P =
    HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
      HPow.hPow (β := ℕ) (P z) 2
⊢ W.dblY P = W.dblU P
have rw₁ : W.dblY P = W.dblY P * HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2
Tactic: rw [dblU, ← dblY_of_Y_eq' hP hPz hQz hx hy hy', mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
rw :
  W.dblY P =
    HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
      HPow.hPow (β := ℕ) (P z) 2
rw₁ : W.dblY P = W.dblY P * HPow.hPow (β := ℕ) (P z) 2 / HPow.hPow (β := ℕ) (P z) 2
⊢ W.dblY P = W.dblU P
have rw₂ : W.dblY P = W.dblY P
Tactic: rw [dblU, ← dblY_of_Y_eq' hP hPz hQz hx hy hy', mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.dblY P / W.dblZ P =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
have erw : W.negY ![W.dblX P, W.negDblY P, W.dblZ P] / W.dblZ P =
  W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
Tactic: erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hQz 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.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
erw :
  W.negY ![W.dblX P, W.negDblY P, W.dblZ P] / W.dblZ P =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
⊢ W.dblY P / W.dblZ P =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
have erw₁ : W.toAffine.negY (![W.dblX P, W.negDblY P, W.dblZ P] x / ![W.dblX P, W.negDblY P, W.dblZ P] z)
    (![W.dblX P, W.negDblY P, W.dblZ P] y / ![W.dblX P, W.negDblY P, W.dblZ P] z) =
  W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
Tactic: erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hQz 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.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
erw :
  W.negY ![W.dblX P, W.negDblY P, W.dblZ P] / W.dblZ P =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
erw₁ :
  W.toAffine.negY (![W.dblX P, W.negDblY P, W.dblZ P] x / ![W.dblX P, W.negDblY P, W.dblZ P] z)
      (![W.dblX P, W.negDblY P, W.dblZ P] y / ![W.dblX P, W.negDblY P, W.dblZ P] z) =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
⊢ W.dblY P / W.dblZ P =
    W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
have erw₂ : W.toAffine.negY
    (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
    (![W.dblX P, W.negDblY P, W.dblZ P] y / ![W.dblX P, W.negDblY P, W.dblZ P] z) =
  W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))
Tactic: erw [dblY, negY_of_Z_ne_zero <| dblZ_ne_zero_of_Y_ne' hP hQ hPz hQz 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]