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
rw : ![W'.addX P P, W'.addY P P, W'.addZ P P] = ![0, 0, 0]
rw₁ : ![0, W'.addY P P, W'.addZ P P] = ![0, 0, 0]
⊢ W'.addXYZ P P = ![0, 0, 0]
have rw₂ : ![0, 0, W'.addZ P P] = ![0, 0, 0]
Tactic: rw [addXYZ, addX_self, addY_self, addZ_self]
-- 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
rw : ![W'.addX P P, W'.addY P P, W'.addZ P P] = ![0, 0, 0]
rw₁ : ![0, W'.addY P P, W'.addZ P P] = ![0, 0, 0]
rw₂ : ![0, 0, W'.addZ P P] = ![0, 0, 0]
⊢ W'.addXYZ P P = ![0, 0, 0]
have rw₃ : Eq.{r + 1} (α := Fin 3 → R) ![0, 0, 0] ![0, 0, 0]
Tactic: rw [addXYZ, addX_self, addY_self, addZ_self]
-- 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'.addXYZ P Q = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
have rw : ![W'.addX P Q, W'.addY P Q, W'.addZ P Q] = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
Tactic: rw [addXYZ, addX_of_Z_eq_zero_left hP hPz, addY_of_Z_eq_zero_left hP hPz,
    addZ_of_Z_eq_zero_left hP hPz, smul_fin3]
-- 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
rw : ![W'.addX P Q, W'.addY P Q, W'.addZ P Q] = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
⊢ W'.addXYZ P Q = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
have rw₁ : ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, W'.addY P Q, W'.addZ P Q] = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
Tactic: rw [addXYZ, addX_of_Z_eq_zero_left hP hPz, addY_of_Z_eq_zero_left hP hPz,
    addZ_of_Z_eq_zero_left hP hPz, smul_fin3]
-- 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
rw : ![W'.addX P Q, W'.addY P Q, W'.addZ P Q] = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
rw₁ : ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, W'.addY P Q, W'.addZ P Q] = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
⊢ W'.addXYZ P Q = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
have rw₂ : ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y, W'.addZ P Q] =
  (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
Tactic: rw [addXYZ, addX_of_Z_eq_zero_left hP hPz, addY_of_Z_eq_zero_left hP hPz,
    addZ_of_Z_eq_zero_left hP hPz, smul_fin3]
-- 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
rw : ![W'.addX P Q, W'.addY P Q, W'.addZ P Q] = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
rw₁ : ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, W'.addY P Q, W'.addZ P Q] = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
rw₂ :
  ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y, W'.addZ P Q] =
    (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
⊢ W'.addXYZ P Q = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
have rw₃ : ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y,
    HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z] =
  (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
Tactic: rw [addXYZ, addX_of_Z_eq_zero_left hP hPz, addY_of_Z_eq_zero_left hP hPz,
    addZ_of_Z_eq_zero_left hP hPz, smul_fin3]
-- 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
rw : ![W'.addX P Q, W'.addY P Q, W'.addZ P Q] = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
rw₁ : ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, W'.addY P Q, W'.addZ P Q] = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
rw₂ :
  ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y, W'.addZ P Q] =
    (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
rw₃ :
  ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y,
      HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z] =
    (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
⊢ W'.addXYZ P Q = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
have rw₄ : ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y,
    HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z] =
  ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y,
    HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z]
Tactic: rw [addXYZ, addX_of_Z_eq_zero_left hP hPz, addY_of_Z_eq_zero_left hP hPz,
    addZ_of_Z_eq_zero_left hP hPz, smul_fin3]
-- 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'.addXYZ P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
have rw : ![W'.addX P Q, W'.addY P Q, W'.addZ P Q] = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
Tactic: rw [addXYZ, addX_of_Z_eq_zero_right hQ hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQ hQz, smul_fin3]
-- 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
rw : ![W'.addX P Q, W'.addY P Q, W'.addZ P Q] = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
⊢ W'.addXYZ P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
have rw₁ : ![-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x, W'.addY P Q, W'.addZ P Q] = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
Tactic: rw [addXYZ, addX_of_Z_eq_zero_right hQ hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQ hQz, smul_fin3]
-- 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
rw : ![W'.addX P Q, W'.addY P Q, W'.addZ P Q] = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
rw₁ : ![-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x, W'.addY P Q, W'.addZ P Q] = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
⊢ W'.addXYZ P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
have rw₂ : ![-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x, -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P y, W'.addZ P Q] =
  -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
Tactic: rw [addXYZ, addX_of_Z_eq_zero_right hQ hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQ hQz, smul_fin3]
-- 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
rw : ![W'.addX P Q, W'.addY P Q, W'.addZ P Q] = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
rw₁ : ![-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x, W'.addY P Q, W'.addZ P Q] = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
rw₂ :
  ![-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x, -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P y, W'.addZ P Q] =
    -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
⊢ W'.addXYZ P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
have rw₃ : ![-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x, -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P y,
    -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P z] =
  -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
Tactic: rw [addXYZ, addX_of_Z_eq_zero_right hQ hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQ hQz, smul_fin3]
-- 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
rw : ![W'.addX P Q, W'.addY P Q, W'.addZ P Q] = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
rw₁ : ![-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x, W'.addY P Q, W'.addZ P Q] = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
rw₂ :
  ![-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x, -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P y, W'.addZ P Q] =
    -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
rw₃ :
  ![-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x, -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P y,
      -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P z] =
    -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
⊢ W'.addXYZ P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
have rw₄ : ![-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x, -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P y,
    -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P z] =
  ![-(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P x, -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P y,
    -(HPow.hPow (β := ℕ) (Q y) 2 * P z) * P z]
Tactic: rw [addXYZ, addX_of_Z_eq_zero_right hQ hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQ hQz, smul_fin3]
-- 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
hx : P x * Q z = Q x * P z
⊢ W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
have erw : ![W.addX P Q, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
Tactic: erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx, 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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
erw : ![W.addX P Q, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
⊢ W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
have erw₁ : ![0, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
Tactic: erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx, 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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
erw : ![W.addX P Q, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₁ : ![0, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
⊢ W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
have erw₂ : ![0, addU P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
Tactic: erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx, 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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
erw : ![W.addX P Q, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₁ : ![0, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₂ : ![0, addU P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
⊢ W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
have erw₃ : ![0, addU P Q, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
Tactic: erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx, 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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
erw : ![W.addX P Q, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₁ : ![0, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₂ : ![0, addU P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₃ : ![0, addU P Q, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
⊢ W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
have erw₄ : ![0, addU P Q, 0] = ![addU P Q * ![0, 1, 0] x, addU P Q * ![0, 1, 0] y, addU P Q * ![0, 1, 0] z]
Tactic: erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx, 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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
erw : ![W.addX P Q, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₁ : ![0, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₂ : ![0, addU P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₃ : ![0, addU P Q, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₄ : ![0, addU P Q, 0] = ![addU P Q * ![0, 1, 0] x, addU P Q * ![0, 1, 0] y, addU P Q * ![0, 1, 0] z]
⊢ W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
have erw₅ : ![0, addU P Q, 0] = ![0, addU P Q * ![0, 1, 0] y, 0]
Tactic: erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx, 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
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
erw : ![W.addX P Q, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₁ : ![0, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₂ : ![0, addU P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₃ : ![0, addU P Q, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₄ : ![0, addU P Q, 0] = ![addU P Q * ![0, 1, 0] x, addU P Q * ![0, 1, 0] y, addU P Q * ![0, 1, 0] z]
erw₅ : ![0, addU P Q, 0] = ![0, addU P Q * ![0, 1, 0] y, 0]
⊢ W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
have erw₆ : ![0, addU P Q, 0] = ![0, addU P Q, 0]
Tactic: erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx, 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
⊢ W.addXYZ P Q =
    W.addZ P Q •
      ![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.addZ P Q)
Tactic: have hZ : IsUnit <| W.addZ P Q := isUnit_addZ_of_X_ne hP hQ hx
-- 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
hZ : IsUnit (W.addZ P Q)
⊢ W.addXYZ P Q =
    W.addZ P Q •
      ![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.addX P Q, W.addY P Q, W.addZ P Q] =
  W.addZ P Q •
    ![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 [addXYZ, smul_fin3, ← addX_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel,
    ← addY_of_Z_ne_zero hP hQ hPz hQz hx, 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
hZ : IsUnit (W.addZ P Q)
erw :
  ![W.addX P Q, W.addY P Q, W.addZ P Q] =
    W.addZ P Q •
      ![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.addXYZ P Q =
    W.addZ P Q •
      ![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.addX P Q, W.addY P Q, W.addZ P Q] =
  ![W.addZ P Q *
      ![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.addZ P Q *
      ![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.addZ P Q *
      ![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 [addXYZ, smul_fin3, ← addX_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel,
    ← addY_of_Z_ne_zero hP hQ hPz hQz hx, 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
hZ : IsUnit (W.addZ P Q)
erw :
  ![W.addX P Q, W.addY P Q, W.addZ P Q] =
    W.addZ P Q •
      ![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.addX P Q, W.addY P Q, W.addZ P Q] =
    ![W.addZ P Q *
        ![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.addZ P Q *
        ![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.addZ P Q *
        ![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.addXYZ P Q =
    W.addZ P Q •
      ![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.addX P Q, W.addY P Q, W.addZ P Q] =
  ![W.addZ P Q *
      ![W.addX P Q / W.addZ P Q,
          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.addZ P Q *
      ![W.addX P Q / W.addZ P Q,
          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.addZ P Q *
      ![W.addX P Q / W.addZ P Q,
          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 [addXYZ, smul_fin3, ← addX_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel,
    ← addY_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).negY ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.negY P)
have simp : -((⇑f : (a : R) → S) ∘ P) y - (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) x - (W'.map f).a₃ * ((⇑f : (a : R) → S) ∘ P) z =
  (f : (a : R) → S) (-P y - W'.a₁ * P x - W'.a₃ * P z)
Tactic: simp only [negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Projective F
f : F →+* K
P : Fin 3 → F
⊢ (W.map f).dblU ((⇑f : (a : F) → K) ∘ P) = (f : (a : F) → K) (W.dblU P)
have simp : HPow.hPow (β := ℕ)
      ((W.map f).a₁ * ((⇑f : (a : F) → K) ∘ P) y * ((⇑f : (a : F) → K) ∘ P) z -
        (3 * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) x) 2 +
            2 * (W.map f).a₂ * ((⇑f : (a : F) → K) ∘ P) x * ((⇑f : (a : F) → K) ∘ P) z +
          (W.map f).a₄ * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) z) 2))
      3 /
    HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) z) 2 =
  (f : (a : F) → K)
    (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: simp only [dblU_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).dblZ ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.dblZ P)
have simp : ((⇑f : (a : R) → S) ∘ P) z *
    HPow.hPow (β := ℕ)
      (((⇑f : (a : R) → S) ∘ P) y -
        (-((⇑f : (a : R) → S) ∘ P) y - (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) x -
          (W'.map f).a₃ * ((⇑f : (a : R) → S) ∘ P) z))
      3 =
  (f : (a : R) → S) (P z * HPow.hPow (β := ℕ) (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) 3)
Tactic: simp only [dblZ, negY]