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 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
erw : ![W.dblX P, W.dblY P, W.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₁ : ![0, W.dblY P, W.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₂ : ![0, W.dblU P, W.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₃ : ![0, W.dblU P, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₄ : ![0, W.dblU P, 0] = ![W.dblU P * ![0, 1, 0] x, W.dblU P * ![0, 1, 0] y, W.dblU P * ![0, 1, 0] z]
⊢ W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
have erw₅ : ![0, W.dblU P, 0] = ![0, W.dblU P * ![0, 1, 0] y, 0]
Tactic: erw [dblXYZ, dblX_of_Y_eq hP hPz hQz hx hy hy', dblY_of_Y_eq hP hPz hQz hx hy hy',
    dblZ_of_Y_eq hQz hx hy hy', smul_fin3, mul_zero, mul_one]
-- 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
erw : ![W.dblX P, W.dblY P, W.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₁ : ![0, W.dblY P, W.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₂ : ![0, W.dblU P, W.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₃ : ![0, W.dblU P, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
erw₄ : ![0, W.dblU P, 0] = ![W.dblU P * ![0, 1, 0] x, W.dblU P * ![0, 1, 0] y, W.dblU P * ![0, 1, 0] z]
erw₅ : ![0, W.dblU P, 0] = ![0, W.dblU P * ![0, 1, 0] y, 0]
⊢ W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
have erw₆ : ![0, W.dblU P, 0] = ![0, W.dblU P, 0]
Tactic: erw [dblXYZ, dblX_of_Y_eq hP hPz hQz hx hy hy', dblY_of_Y_eq hP hPz hQz hx hy hy',
    dblZ_of_Y_eq hQz hx hy hy', smul_fin3, mul_zero, mul_one]
-- 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
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.dblXYZ 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)),
        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)),
        1]
have hZ : IsUnit (W.dblZ P)
Tactic: have hZ : IsUnit <| W.dblZ P := isUnit_dblZ_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
hZ : IsUnit (W.dblZ P)
⊢ W.dblXYZ 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)),
        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)),
        1]
have erw : ![W.dblX P, W.dblY P, W.dblZ 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)),
      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)),
      1]
Tactic: erw [dblXYZ, smul_fin3, ← dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel,
    ← dblY_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel, mul_one]
-- 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
hZ : IsUnit (W.dblZ P)
erw :
  ![W.dblX P, W.dblY P, W.dblZ 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)),
        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)),
        1]
⊢ W.dblXYZ 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)),
        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)),
        1]
have erw₁ : ![W.dblX P, W.dblY P, W.dblZ 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)),
          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)),
          1]
        x,
    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.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)),
          1]
        y,
    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.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)),
          1]
        z]
Tactic: erw [dblXYZ, smul_fin3, ← dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel,
    ← dblY_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel, mul_one]
-- 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
hZ : IsUnit (W.dblZ P)
erw :
  ![W.dblX P, W.dblY P, W.dblZ 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)),
        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)),
        1]
erw₁ :
  ![W.dblX P, W.dblY P, W.dblZ 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)),
            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)),
            1]
          x,
      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.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)),
            1]
          y,
      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.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)),
            1]
          z]
⊢ W.dblXYZ 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)),
        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)),
        1]
have erw₂ : ![W.dblX P, W.dblY P, W.dblZ P] =
  ![W.dblZ P *
      ![W.dblX 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)),
          1]
        x,
    W.dblZ P *
      ![W.dblX 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)),
          1]
        y,
    W.dblZ P *
      ![W.dblX 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)),
          1]
        z]
Tactic: erw [dblXYZ, smul_fin3, ← dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel,
    ← dblY_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z = 0
⊢ addU P Q = 0
have rw : -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z) = 0
Tactic: rw [addU, hPz, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z = 0
rw : -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z) = 0
⊢ addU P Q = 0
have rw₁ : -HPow.hPow (β := ℕ) (P y * Q z - Q y * 0) 3 / (0 * Q z) = 0
Tactic: rw [addU, hPz, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z = 0
rw : -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z) = 0
rw₁ : -HPow.hPow (β := ℕ) (P y * Q z - Q y * 0) 3 / (0 * Q z) = 0
⊢ addU P Q = 0
have rw₂ : -HPow.hPow (β := ℕ) (P y * Q z - Q y * 0) 3 / 0 = 0
Tactic: rw [addU, hPz, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z = 0
rw : -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z) = 0
rw₁ : -HPow.hPow (β := ℕ) (P y * Q z - Q y * 0) 3 / (0 * Q z) = 0
rw₂ : -HPow.hPow (β := ℕ) (P y * Q z - Q y * 0) 3 / 0 = 0
⊢ addU P Q = 0
have rw₃ : Eq.{u + 1} (α := F) 0 0
Tactic: rw [addU, hPz, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ addU P Q = 0
have rw : -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z) = 0
Tactic: rw [addU, hQz, mul_zero <| P z, div_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hQz : Q z = 0
rw : -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z) = 0
⊢ addU P Q = 0
have rw₁ : -HPow.hPow (β := ℕ) (P y * 0 - Q y * P z) 3 / (P z * 0) = 0
Tactic: rw [addU, hQz, mul_zero <| P z, div_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hQz : Q z = 0
rw : -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z) = 0
rw₁ : -HPow.hPow (β := ℕ) (P y * 0 - Q y * P z) 3 / (P z * 0) = 0
⊢ addU P Q = 0
have rw₂ : -HPow.hPow (β := ℕ) (P y * 0 - Q y * P z) 3 / 0 = 0
Tactic: rw [addU, hQz, mul_zero <| P z, div_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hQz : Q z = 0
rw : -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z) = 0
rw₁ : -HPow.hPow (β := ℕ) (P y * 0 - Q y * P z) 3 / (P z * 0) = 0
rw₂ : -HPow.hPow (β := ℕ) (P y * 0 - Q y * P z) 3 / 0 = 0
⊢ addU P Q = 0
have rw₃ : Eq.{u + 1} (α := F) 0 0
Tactic: rw [addU, hQz, mul_zero <| P z, div_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ W'.addZ P Q * (P z * Q z) +
        (HPow.hPow (β := ℕ) (Q z) 3 * 0 +
          HPow.hPow (β := ℕ) (P z) 3 *
            (HPow.hPow (β := ℕ) (Q y) 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * HPow.hPow (β := ℕ) (Q z) 2 -
              (HPow.hPow (β := ℕ) (Q x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * Q z +
                  W'.a₄ * Q x * HPow.hPow (β := ℕ) (Q z) 2 +
                W'.a₆ * HPow.hPow (β := ℕ) (Q z) 3))) -
      (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 +
        (HPow.hPow (β := ℕ) (Q z) 3 *
            (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)) +
          HPow.hPow (β := ℕ) (P z) 3 * 0)) =
    0
have a : (-3 * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q z + 3 * P x * HPow.hPow (β := ℕ) (Q x) 2 * P z +
                            HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
                          HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                        W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (Q z) 2 -
                      W'.a₁ * Q x * Q y * HPow.hPow (β := ℕ) (P z) 2 -
                    W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                  W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (Q z) 2 -
              W'.a₃ * Q y * HPow.hPow (β := ℕ) (P z) 2 * Q z -
            W'.a₄ * P x * P z * HPow.hPow (β := ℕ) (Q z) 2 +
          W'.a₄ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z) *
        (P z * Q z) +
      (HPow.hPow (β := ℕ) (Q z) 3 * 0 +
        HPow.hPow (β := ℕ) (P z) 3 *
          (HPow.hPow (β := ℕ) (Q y) 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * HPow.hPow (β := ℕ) (Q z) 2 -
            (HPow.hPow (β := ℕ) (Q x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * Q z +
                W'.a₄ * Q x * HPow.hPow (β := ℕ) (Q z) 2 +
              W'.a₆ * HPow.hPow (β := ℕ) (Q z) 3))) -
    (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 +
      (HPow.hPow (β := ℕ) (Q z) 3 *
          (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)) +
        HPow.hPow (β := ℕ) (P z) 3 * 0)) =
  0
Tactic: rw [addZ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ W'.addZ P Q * (P z * Q z) = HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3
have a : W'.addZ P Q * (P z * Q z) +
      (HPow.hPow (β := ℕ) (Q z) 3 * 0 +
        HPow.hPow (β := ℕ) (P z) 3 *
          (HPow.hPow (β := ℕ) (Q y) 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * HPow.hPow (β := ℕ) (Q z) 2 -
            (HPow.hPow (β := ℕ) (Q x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * Q z +
                W'.a₄ * Q x * HPow.hPow (β := ℕ) (Q z) 2 +
              W'.a₆ * HPow.hPow (β := ℕ) (Q z) 3))) -
    (HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 +
      (HPow.hPow (β := ℕ) (Q z) 3 *
          (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)) +
        HPow.hPow (β := ℕ) (P z) 3 * 0)) =
  0
Tactic: linear_combination (norm := (rw [addZ]; ring1))
    Q z ^ 3 * (equation_iff _).mp hP - P z ^ 3 * (equation_iff _).mp hQ
-- 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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addZ P Q = HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 / (P z * Q z)
have rw : W.addZ P Q = W.addZ P Q * (P z * Q z) / (P z * Q z)
Tactic: rw [← addZ_eq' hP hQ, mul_div_cancel_right₀ _ <| mul_ne_zero hPz hQz]
-- 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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
rw : W.addZ P Q = W.addZ P Q * (P z * Q z) / (P z * Q z)
⊢ W.addZ P Q = HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 / (P z * Q z)
have rw₁ : W.addZ P Q = W.addZ P Q
Tactic: rw [← addZ_eq' hP hQ, mul_div_cancel_right₀ _ <| mul_ne_zero hPz hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ W'.addZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q
have simp : -3 * HPow.hPow (β := ℕ) (u * P x) 2 * (v * Q x) * (v * Q z) +
                        3 * (u * P x) * HPow.hPow (β := ℕ) (v * Q x) 2 * (u * P z) +
                      HPow.hPow (β := ℕ) (u * P y) 2 * HPow.hPow (β := ℕ) (v * Q z) 2 -
                    HPow.hPow (β := ℕ) (v * Q y) 2 * HPow.hPow (β := ℕ) (u * P z) 2 +
                  W'.a₁ * (u * P x) * (u * P y) * HPow.hPow (β := ℕ) (v * Q z) 2 -
                W'.a₁ * (v * Q x) * (v * Q y) * HPow.hPow (β := ℕ) (u * P z) 2 -
              W'.a₂ * HPow.hPow (β := ℕ) (u * P x) 2 * HPow.hPow (β := ℕ) (v * Q z) 2 +
            W'.a₂ * HPow.hPow (β := ℕ) (v * Q x) 2 * HPow.hPow (β := ℕ) (u * P z) 2 +
          W'.a₃ * (u * P y) * (u * P z) * HPow.hPow (β := ℕ) (v * Q z) 2 -
        W'.a₃ * (v * Q y) * HPow.hPow (β := ℕ) (u * P z) 2 * (v * Q z) -
      W'.a₄ * (u * P x) * (u * P z) * HPow.hPow (β := ℕ) (v * Q z) 2 +
    W'.a₄ * (v * Q x) * HPow.hPow (β := ℕ) (u * P z) 2 * (v * Q z) =
  HPow.hPow (β := ℕ) (u * v) 2 *
    (-3 * HPow.hPow (β := ℕ) (P x) 2 * Q x * Q z + 3 * P x * HPow.hPow (β := ℕ) (Q x) 2 * P z +
                        HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
                      HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                    W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (Q z) 2 -
                  W'.a₁ * Q x * Q y * HPow.hPow (β := ℕ) (P z) 2 -
                W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
              W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (Q z) 2 -
          W'.a₃ * Q y * HPow.hPow (β := ℕ) (P z) 2 * Q z -
        W'.a₄ * P x * P z * HPow.hPow (β := ℕ) (Q z) 2 +
      W'.a₄ * Q x * HPow.hPow (β := ℕ) (P z) 2 * Q z)
Tactic: simp only [addZ, 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
⊢ W'.addZ P P = 0
have rw : -3 * HPow.hPow (β := ℕ) (P x) 2 * P x * P z + 3 * P x * HPow.hPow (β := ℕ) (P x) 2 * P z +
                      HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                    HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                  W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 -
                W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 -
              W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (P z) 2 -
        W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 2 * P z -
      W'.a₄ * P x * P z * HPow.hPow (β := ℕ) (P z) 2 +
    W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * P z =
  0
Tactic: rw [addZ]
-- 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
⊢ W'.addZ P Q = HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z
have rw : -3 * HPow.hPow (α := R) (β := ℕ) 0 2 * Q x * Q z + HMul.hMul (α := R) 3 0 * HPow.hPow (β := ℕ) (Q x) 2 * 0 +
                      HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
                    HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
                  W'.a₁ * 0 * P y * HPow.hPow (β := ℕ) (Q z) 2 -
                W'.a₁ * Q x * Q y * HPow.hPow (α := R) (β := ℕ) 0 2 -
              W'.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) (Q z) 2 +
            W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
          W'.a₃ * P y * 0 * HPow.hPow (β := ℕ) (Q z) 2 -
        W'.a₃ * Q y * HPow.hPow (α := R) (β := ℕ) 0 2 * Q z -
      W'.a₄ * 0 * 0 * HPow.hPow (β := ℕ) (Q z) 2 +
    W'.a₄ * Q x * HPow.hPow (α := R) (β := ℕ) 0 2 * Q z =
  HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z
Tactic: rw [addZ, hPz, X_eq_zero_of_Z_eq_zero hP 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
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addZ P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P z
have rw : -3 * HPow.hPow (β := ℕ) (P x) 2 * 0 * 0 + 3 * P x * HPow.hPow (α := R) (β := ℕ) 0 2 * P z +
                      HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 -
                    HPow.hPow (β := ℕ) (Q y) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                  W'.a₁ * P x * P y * HPow.hPow (α := R) (β := ℕ) 0 2 -
                W'.a₁ * 0 * Q y * HPow.hPow (β := ℕ) (P z) 2 -
              W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (α := R) (β := ℕ) 0 2 +
            W'.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₃ * P y * P z * HPow.hPow (α := R) (β := ℕ) 0 2 -
        W'.a₃ * Q y * HPow.hPow (β := ℕ) (P z) 2 * 0 -
      W'.a₄ * P x * P z * HPow.hPow (α := R) (β := ℕ) 0 2 +
    W'.a₄ * 0 * HPow.hPow (β := ℕ) (P z) 2 * 0 =
  -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P z
Tactic: rw [addZ, hQz, X_eq_zero_of_Z_eq_zero hQ hQz]
-- 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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addZ P Q = 0
have apply : W'.addZ P Q * (P z * Q z) = 0
Tactic: apply eq_zero_of_ne_zero_of_mul_right_eq_zero <| mul_ne_zero hPz hQz
-- 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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addZ P Q * (P z * Q z) = 0
have rw : HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 = 0
Tactic: rw [addZ_eq' hP hQ, hx, sub_self, zero_pow three_ne_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
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
rw : HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 = 0
⊢ W'.addZ P Q * (P z * Q z) = 0
have rw₁ : HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 3 = 0
Tactic: rw [addZ_eq' hP hQ, hx, sub_self, zero_pow three_ne_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
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
rw : HPow.hPow (β := ℕ) (P x * Q z - Q x * P z) 3 = 0
rw₁ : HPow.hPow (β := ℕ) (Q x * P z - Q x * P z) 3 = 0
⊢ W'.addZ P Q * (P z * Q z) = 0
have rw₂ : HPow.hPow (α := R) (β := ℕ) 0 3 = 0
Tactic: rw [addZ_eq' hP hQ, hx, sub_self, zero_pow three_ne_zero]