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
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'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 +
        -(P z * Q z) * (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * (P z * Q z)) -
      (-HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 +
        -(P z * Q z) * (W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 2)) =
    0
have a : (-W'.negAddY P Q - W'.a₁ * 0 - W'.a₃ * 0) * HPow.hPow (β := ℕ) (P z * Q z) 3 +
      -(P z * Q z) * (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * (P z * Q z)) -
    (-HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 +
      -(P z * Q z) * (W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 2)) =
  0
Tactic: rw [addY, negY_eq, addX_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx]
-- 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'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 =
    -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2
have a : W'.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 +
      -(P z * Q z) * (HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * (P z * Q z)) -
    (-HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 +
      -(P z * Q z) * (W'.negAddY P Q * HPow.hPow (β := ℕ) (P z * Q z) 2)) =
  0
Tactic: linear_combination (norm := (rw [addY, negY_eq, addX_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx]; ring1)) -(P z * Q z) * negAddY_of_X_eq' hP hQ hx
-- 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.addY P Q = addU P Q
have rw : W.addY P Q = -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z)
Tactic: rw [addU, ← mul_div_mul_right _ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz,
    ← addY_of_X_eq' hP hQ hPz hQz hx, ← pow_succ',
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| 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
hx : P x * Q z = Q x * P z
rw : W.addY P Q = -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z)
⊢ W.addY P Q = addU P Q
have rw₁ : W.addY P Q =
  -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 /
    (P z * Q z * HPow.hPow (β := ℕ) (P z * Q z) 2)
Tactic: rw [addU, ← mul_div_mul_right _ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz,
    ← addY_of_X_eq' hP hQ hPz hQz hx, ← pow_succ',
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| 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
hx : P x * Q z = Q x * P z
rw : W.addY P Q = -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z)
rw₁ :
  W.addY P Q =
    -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (P z * Q z * HPow.hPow (β := ℕ) (P z * Q z) 2)
⊢ W.addY P Q = addU P Q
have rw₂ : W.addY P Q = W.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / (P z * Q z * HPow.hPow (β := ℕ) (P z * Q z) 2)
Tactic: rw [addU, ← mul_div_mul_right _ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz,
    ← addY_of_X_eq' hP hQ hPz hQz hx, ← pow_succ',
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| 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
hx : P x * Q z = Q x * P z
rw : W.addY P Q = -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z)
rw₁ :
  W.addY P Q =
    -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (P z * Q z * HPow.hPow (β := ℕ) (P z * Q z) 2)
rw₂ : W.addY P Q = W.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / (P z * Q z * HPow.hPow (β := ℕ) (P z * Q z) 2)
⊢ W.addY P Q = addU P Q
have rw₃ : W.addY P Q = W.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / (P z * Q z) ^ HAdd.hAdd (α := ℕ) 2 1
Tactic: rw [addU, ← mul_div_mul_right _ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz,
    ← addY_of_X_eq' hP hQ hPz hQz hx, ← pow_succ',
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| 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
hx : P x * Q z = Q x * P z
rw : W.addY P Q = -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z)
rw₁ :
  W.addY P Q =
    -HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 * HPow.hPow (β := ℕ) (P z * Q z) 2 /
      (P z * Q z * HPow.hPow (β := ℕ) (P z * Q z) 2)
rw₂ : W.addY P Q = W.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / (P z * Q z * HPow.hPow (β := ℕ) (P z * Q z) 2)
rw₃ : W.addY P Q = W.addY P Q * HPow.hPow (β := ℕ) (P z * Q z) 3 / (P z * Q z) ^ HAdd.hAdd (α := ℕ) 2 1
⊢ W.addY P Q = addU P Q
have rw₄ : W.addY P Q = W.addY P Q
Tactic: rw [addU, ← mul_div_mul_right _ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz,
    ← addY_of_X_eq' hP hQ hPz hQz hx, ← pow_succ',
    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| 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
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.addY 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))
have erw : W.negY ![W.addX P Q, W.negAddY P Q, W.addZ 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))
Tactic: erw [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hP hQ hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
    negAddY_of_Z_ne_zero hP hQ hPz hQz hx, 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
erw :
  W.negY ![W.addX P Q, W.negAddY P Q, W.addZ 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))
⊢ W.addY 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))
have erw₁ : W.toAffine.negY (![W.addX P Q, W.negAddY P Q, W.addZ P Q] x / ![W.addX P Q, W.negAddY P Q, W.addZ P Q] z)
    (![W.addX P Q, W.negAddY P Q, W.addZ P Q] y / ![W.addX P Q, W.negAddY P Q, W.addZ P 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 [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hP hQ hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
    negAddY_of_Z_ne_zero hP hQ hPz hQz hx, 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
erw :
  W.negY ![W.addX P Q, W.negAddY P Q, W.addZ 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))
erw₁ :
  W.toAffine.negY (![W.addX P Q, W.negAddY P Q, W.addZ P Q] x / ![W.addX P Q, W.negAddY P Q, W.addZ P Q] z)
      (![W.addX P Q, W.negAddY P Q, W.addZ P Q] y / ![W.addX P Q, W.negAddY P Q, W.addZ P 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.addY 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))
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.addX P Q, W.negAddY P Q, W.addZ P Q] y / ![W.addX P Q, W.negAddY P Q, W.addZ P 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 [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hP hQ hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
    negAddY_of_Z_ne_zero hP hQ hPz hQz hx, 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
erw :
  W.negY ![W.addX P Q, W.negAddY P Q, W.addZ 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))
erw₁ :
  W.toAffine.negY (![W.addX P Q, W.negAddY P Q, W.addZ P Q] x / ![W.addX P Q, W.negAddY P Q, W.addZ P Q] z)
      (![W.addX P Q, W.negAddY P Q, W.addZ P Q] y / ![W.addX P Q, W.negAddY P Q, W.addZ P 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))
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.addX P Q, W.negAddY P Q, W.addZ P Q] y / ![W.addX P Q, W.negAddY P Q, W.addZ P 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.addY 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))
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 [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hP hQ hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
    negAddY_of_Z_ne_zero hP hQ hPz hQz hx, 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
erw :
  W.negY ![W.addX P Q, W.negAddY P Q, W.addZ 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))
erw₁ :
  W.toAffine.negY (![W.addX P Q, W.negAddY P Q, W.addZ P Q] x / ![W.addX P Q, W.negAddY P Q, W.addZ P Q] z)
      (![W.addX P Q, W.negAddY P Q, W.addZ P Q] y / ![W.addX P Q, W.negAddY P Q, W.addZ P 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))
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.addX P Q, W.negAddY P Q, W.addZ P Q] y / ![W.addX P Q, W.negAddY P Q, W.addZ P 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))
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.addY 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))
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 [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hP hQ hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
    negAddY_of_Z_ne_zero hP hQ hPz hQz hx, Affine.addY]
-- 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'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
have rw : ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
  HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
Tactic: rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]
-- 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
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
⊢ W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
have rw₁ : ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
  HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
Tactic: rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]
-- 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
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
⊢ W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
have rw₂ : ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q, W'.addZ (u • P) (v • Q)] =
  HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
Tactic: rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]
-- 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
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₂ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q, W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
⊢ W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
have rw₃ : ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
    HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
  HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
Tactic: rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]
-- 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
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₂ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q, W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₃ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
⊢ W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
have rw₄ : ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
    HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q x, HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q y,
    HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
Tactic: rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]
-- 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
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₂ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q, W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₃ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₄ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q x, HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q y,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
⊢ W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
have rw₅ : ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
    HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q y,
    HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
Tactic: rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]
-- 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
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₂ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q, W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₃ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₄ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q x, HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q y,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
rw₅ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q y,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
⊢ W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
have rw₆ : ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
    HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
    HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
Tactic: rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]
-- 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
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₂ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q, W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₃ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₄ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q x, HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q y,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
rw₅ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q y,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
rw₆ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
⊢ W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
have rw₇ : ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
    HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
    HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q]
Tactic: rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_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
⊢ W'.addXYZ P P = ![0, 0, 0]
have rw : ![W'.addX P P, W'.addY P P, 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]
⊢ W'.addXYZ P P = ![0, 0, 0]
have rw₁ : ![0, W'.addY P P, W'.addZ P P] = ![0, 0, 0]
Tactic: rw [addXYZ, addX_self, addY_self, addZ_self]