awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw :
  HPow.hPow (α := F) (β := ℕ) ((eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) 3 /
      HPow.hPow (β := ℕ) (P z) 2 =
    HPow.hPow (β := ℕ)
        (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
        3 /
      HPow.hPow (β := ℕ) (P z) 2
⊢ W.dblU P =
    HPow.hPow (β := ℕ)
        (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
        3 /
      HPow.hPow (β := ℕ) (P z) 2
have rw₁ : HPow.hPow (β := ℕ)
      (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
      3 /
    HPow.hPow (β := ℕ) (P z) 2 =
  HPow.hPow (β := ℕ)
      (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
      3 /
    HPow.hPow (β := ℕ) (P z) 2
Tactic: rw [dblU, eval_polynomialX]
-- 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
⊢ W.dblU P = 0
have rw : HPow.hPow (β := ℕ)
      (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
      3 /
    HPow.hPow (β := ℕ) (P z) 2 =
  0
Tactic: rw [dblU_eq, hPz, zero_pow two_ne_zero, div_zero]
-- 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
rw :
  HPow.hPow (β := ℕ)
        (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
        3 /
      HPow.hPow (β := ℕ) (P z) 2 =
    0
⊢ W.dblU P = 0
have rw₁ : HPow.hPow (β := ℕ)
      (W.a₁ * P y * 0 - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * 0 + W.a₄ * HPow.hPow (α := F) (β := ℕ) 0 2))
      3 /
    HPow.hPow (α := F) (β := ℕ) 0 2 =
  0
Tactic: rw [dblU_eq, hPz, zero_pow two_ne_zero, div_zero]
-- 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
rw :
  HPow.hPow (β := ℕ)
        (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
        3 /
      HPow.hPow (β := ℕ) (P z) 2 =
    0
rw₁ :
  HPow.hPow (β := ℕ)
        (W.a₁ * P y * 0 -
          (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * 0 + W.a₄ * HPow.hPow (α := F) (β := ℕ) 0 2))
        3 /
      HPow.hPow (α := F) (β := ℕ) 0 2 =
    0
⊢ W.dblU P = 0
have rw₂ : HPow.hPow (β := ℕ) (W.a₁ * P y * 0 - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * 0 + W.a₄ * 0)) 3 / 0 = 0
Tactic: rw [dblU_eq, hPz, zero_pow two_ne_zero, div_zero]
-- 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
rw :
  HPow.hPow (β := ℕ)
        (W.a₁ * P y * P z - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
        3 /
      HPow.hPow (β := ℕ) (P z) 2 =
    0
rw₁ :
  HPow.hPow (β := ℕ)
        (W.a₁ * P y * 0 -
          (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * 0 + W.a₄ * HPow.hPow (α := F) (β := ℕ) 0 2))
        3 /
      HPow.hPow (α := F) (β := ℕ) 0 2 =
    0
rw₂ : HPow.hPow (β := ℕ) (W.a₁ * P y * 0 - (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * 0 + W.a₄ * 0)) 3 / 0 = 0
⊢ W.dblU P = 0
have rw₃ : Eq.{u + 1} (α := F) 0 0
Tactic: rw [dblU_eq, hPz, zero_pow two_ne_zero, div_zero]
-- 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'.dblZ (u • P) = HPow.hPow (β := ℕ) u 4 * W'.dblZ P
have simp : u * P z * HPow.hPow (β := ℕ) (u * P y - u * W'.negY P) 3 =
  HPow.hPow (β := ℕ) u 4 * (P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3)
Tactic: simp only [dblZ, negY_smul, smul_fin3_ext]
-- 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
hPz : P z = 0
⊢ W'.dblZ P = 0
have rw : P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
Tactic: rw [dblZ, hPz, zero_mul]
-- 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
hPz : P z = 0
rw : P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
⊢ W'.dblZ P = 0
have rw₁ : 0 * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
Tactic: rw [dblZ, hPz, zero_mul]
-- 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
hPz : P z = 0
rw : P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
rw₁ : 0 * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
⊢ W'.dblZ P = 0
have rw₂ : Eq.{r + 1} (α := R) 0 0
Tactic: rw [dblZ, hPz, zero_mul]
-- 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
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'.dblZ P = 0
have rw : P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
Tactic: rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, zero_pow three_ne_zero, mul_zero]
-- 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
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 : P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
⊢ W'.dblZ P = 0
have rw₁ : P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 3 = 0
Tactic: rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, zero_pow three_ne_zero, mul_zero]
-- 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
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 : P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
rw₁ : P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 3 = 0
⊢ W'.dblZ P = 0
have rw₂ : P z * HPow.hPow (α := R) (β := ℕ) 0 3 = 0
Tactic: rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, zero_pow three_ne_zero, mul_zero]
-- 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
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 : P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
rw₁ : P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 3 = 0
rw₂ : P z * HPow.hPow (α := R) (β := ℕ) 0 3 = 0
⊢ W'.dblZ P = 0
have rw₃ : P z * 0 = 0
Tactic: rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, zero_pow three_ne_zero, mul_zero]
-- 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
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 : P z * HPow.hPow (β := ℕ) (P y - W'.negY P) 3 = 0
rw₁ : P z * HPow.hPow (β := ℕ) (W'.negY P - W'.negY P) 3 = 0
rw₂ : P z * HPow.hPow (α := R) (β := ℕ) 0 3 = 0
rw₃ : P z * 0 = 0
⊢ W'.dblZ P = 0
have rw₄ : Eq.{r + 1} (α := R) 0 0
Tactic: rw [dblZ, Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, zero_pow three_ne_zero, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (hypothesis)
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
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.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) =
    HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (P z) / (P y - W.negY P)
have hx₁ : P x / P z = Q x / Q z
Tactic: simp only [X_eq_iff hPz hQz, ne_eq, Y_eq_iff' hPz hQz] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (hypothesis)
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
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
hx₁ : 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) =
    HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (P z) / (P y - W.negY P)
have hy₁ : ¬P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z)
Tactic: simp only [X_eq_iff hPz hQz, ne_eq, Y_eq_iff' hPz hQz] at hx hy
Cleared hypotheses: 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
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x / P z = Q x / Q z
hy : ¬P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z)
⊢ W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) =
    HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (P z) / (P y - W.negY P)
have rw : (3 * HPow.hPow (β := ℕ) (P x / P z) 2 + 2 * W.toAffine.a₂ * (P x / P z) + W.toAffine.a₄ - W.toAffine.a₁ * (P y / P z)) /
    (P y / P z - W.negY P / P z) =
  HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (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]
-- 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'.dblX P * P z =
    (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 y - W'.negY P)
have a : W'.dblX P * P z + 9 * (W'.a₁ * HPow.hPow (β := ℕ) (P x) 2 + 2 * P x * P y) * 0 -
    ((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 y - W'.negY P) +
      9 * (W'.a₁ * HPow.hPow (β := ℕ) (P x) 2 + 2 * P x * P y) *
        (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 [dblX, eval_polynomialX, negY]; ring1))
    9 * (W'.a₁ * P x ^ 2 + 2 * P x * P y) * (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.dblX P =
    (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 y - W.negY P) /
      P z
have rw : W.dblX P = W.dblX P * P z / P z
Tactic: rw [← dblX_eq' hP, mul_div_cancel_right₀ _ 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.dblX P = W.dblX P * P z / P z
⊢ W.dblX P =
    (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 y - W.negY P) /
      P z
have rw₁ : W.dblX P = W.dblX P
Tactic: rw [← dblX_eq' hP, mul_div_cancel_right₀ _ 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'.dblX P = 0
have apply : W'.dblX P * P z = 0
Tactic: apply eq_zero_of_ne_zero_of_mul_right_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'.dblX P * P z = 0
have rw : (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) *
    (W'.negY P - W'.negY P) =
  0
Tactic: rw [dblX_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 : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.addX (P x / P z) (P x / P z) (-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)
have simp : n * (n + -(P z * d * W.toAffine.a₁)) - HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) d 2 * W.toAffine.a₂ -
      P z * HPow.hPow (β := ℕ) d 2 * P x -
    P z * 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₂ -
    P z * HPow.hPow (β := ℕ) d 2 * P x * 2
Tactic: simp [field]
-- 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.dblX P / W.dblZ P =
    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))
have rw : (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 y - W.negY P) /
      P z /
    W.dblZ P =
  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))
Tactic: rw [dblX_eq hP hPz, dblZ, toAffine_slope_of_eq hPz hQz hx hy, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_addX_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 :
  (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 y - W.negY P) /
        P z /
      W.dblZ P =
    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.dblZ P =
    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))
have rw₁ : (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 y - W.negY P) /
      P z /
    (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3) =
  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))
Tactic: rw [dblX_eq hP hPz, dblZ, toAffine_slope_of_eq hPz hQz hx hy, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_addX_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 :
  (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 y - W.negY P) /
        P z /
      W.dblZ P =
    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))
rw₁ :
  (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 y - W.negY P) /
        P z /
      (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3) =
    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.dblZ P =
    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))
have rw₂ : (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 y - W.negY P) /
      P z /
    (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3) =
  W.toAffine.addX (P x / P z) (Q x / Q z)
    (HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (P z) / (P y - W.negY P))
Tactic: rw [dblX_eq hP hPz, dblZ, toAffine_slope_of_eq hPz hQz hx hy, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_addX_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 :
  (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 y - W.negY P) /
        P z /
      W.dblZ P =
    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))
rw₁ :
  (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 y - W.negY P) /
        P z /
      (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3) =
    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))
rw₂ :
  (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 y - W.negY P) /
        P z /
      (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3) =
    W.toAffine.addX (P x / P z) (Q x / Q z)
      (HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (P z) / (P y - W.negY P))
⊢ W.dblX P / W.dblZ P =
    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))
have rw₃ : (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 y - W.negY P) /
      P z /
    (P z * HPow.hPow (β := ℕ) (P y - W.negY P) 3) =
  W.toAffine.addX (P x / P z) (P x / P z)
    (HDiv.hDiv (α := F) (-(eval P : (a : MvPolynomial (Fin 3) F) → F) W.polynomialX : F) (P z) / (P y - W.negY P))
Tactic: rw [dblX_eq hP hPz, dblZ, toAffine_slope_of_eq hPz hQz hx hy, ← (X_eq_iff hPz hQz).mp hx,
    toAffine_addX_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hPz hQz hx hy]