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
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))
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))
⊢ 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.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.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))
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))
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.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.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.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.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.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: 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:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have rw : ![W'.dblX (u • P), W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- 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
rw : ![W'.dblX (u • P), W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have rw₁ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- 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
rw : ![W'.dblX (u • P), W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₁ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have rw₂ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, W'.dblZ (u • P)] =
  HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- 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
rw : ![W'.dblX (u • P), W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₁ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₂ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, W'.dblZ (u • P)] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have rw₃ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
  HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- 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
rw : ![W'.dblX (u • P), W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₁ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₂ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, W'.dblZ (u • P)] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₃ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have rw₄ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
  ![HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P x, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P y,
    HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- 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
rw : ![W'.dblX (u • P), W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₁ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₂ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, W'.dblZ (u • P)] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₃ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₄ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P x, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P y,
      HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have rw₅ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P y, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- 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
rw : ![W'.dblX (u • P), W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₁ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₂ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, W'.dblZ (u • P)] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₃ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₄ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P x, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P y,
      HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
rw₅ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P y,
      HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have rw₆ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- 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
rw : ![W'.dblX (u • P), W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₁ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, W'.dblY (u • P), W'.dblZ (u • P)] = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₂ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, W'.dblZ (u • P)] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₃ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
rw₄ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P x, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P y,
      HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
rw₅ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P y,
      HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
rw₆ :
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
    ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblXYZ P z]
⊢ W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
have rw₇ : ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P] =
  ![HPow.hPow (β := ℕ) u 4 * W'.dblX P, HPow.hPow (β := ℕ) u 4 * W'.dblY P, HPow.hPow (β := ℕ) u 4 * W'.dblZ P]
Tactic: rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]
-- 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'.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
have erw : ![W'.dblX P, W'.dblY P, W'.dblZ P] =
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
Tactic: erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, smul_fin3,
    mul_zero, mul_one]
-- 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
erw :
  ![W'.dblX P, W'.dblY P, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
⊢ W'.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
have erw₁ : ![0, W'.dblY P, W'.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
Tactic: erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, smul_fin3,
    mul_zero, mul_one]
-- 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
erw :
  ![W'.dblX P, W'.dblY P, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₁ :
  ![0, W'.dblY P, W'.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
⊢ W'.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
have erw₂ : ![0, HPow.hPow (β := ℕ) (P y) 4, W'.dblZ P] =
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
Tactic: erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, smul_fin3,
    mul_zero, mul_one]
-- 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
erw :
  ![W'.dblX P, W'.dblY P, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₁ :
  ![0, W'.dblY P, W'.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₂ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
⊢ W'.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
have erw₃ : ![0, HPow.hPow (β := ℕ) (P y) 4, 0] =
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
Tactic: erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, smul_fin3,
    mul_zero, mul_one]
-- 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
erw :
  ![W'.dblX P, W'.dblY P, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₁ :
  ![0, W'.dblY P, W'.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₂ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₃ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, 0] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
⊢ W'.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
have erw₄ : ![0, HPow.hPow (β := ℕ) (P y) 4, 0] =
  ![HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] x, HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] y,
    HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] z]
Tactic: erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, smul_fin3,
    mul_zero, mul_one]
-- 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
erw :
  ![W'.dblX P, W'.dblY P, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₁ :
  ![0, W'.dblY P, W'.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₂ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₃ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, 0] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₄ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, 0] =
    ![HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] x, HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] y,
      HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] z]
⊢ W'.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
have erw₅ : ![0, HPow.hPow (β := ℕ) (P y) 4, 0] = ![0, HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] y, 0]
Tactic: erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, smul_fin3,
    mul_zero, mul_one]
-- 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
erw :
  ![W'.dblX P, W'.dblY P, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₁ :
  ![0, W'.dblY P, W'.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₂ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, W'.dblZ P] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₃ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, 0] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
erw₄ :
  ![0, HPow.hPow (β := ℕ) (P y) 4, 0] =
    ![HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] x, HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] y,
      HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] z]
erw₅ : ![0, HPow.hPow (β := ℕ) (P y) 4, 0] = ![0, HPow.hPow (β := ℕ) (P y) 4 * ![0, 1, 0] y, 0]
⊢ W'.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
have erw₆ : ![0, HPow.hPow (β := ℕ) (P y) 4, 0] = ![0, HPow.hPow (β := ℕ) (P y) 4, 0]
Tactic: erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, 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
⊢ W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
have 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]
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]
⊢ W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
have erw₁ : ![0, W.dblY P, W.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 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]
⊢ W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
have erw₂ : ![0, W.dblU P, W.dblZ P] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 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]
⊢ 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] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 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]
⊢ 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] = ![W.dblU P * ![0, 1, 0] x, W.dblU P * ![0, 1, 0] y, W.dblU P * ![0, 1, 0] z]
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]