awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), 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 (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), 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.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), 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 (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, 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.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₂ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, 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 (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * 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.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₂ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₃ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * 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 (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addXYZ P Q x,
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * 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.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₂ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₃ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₄ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
    ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addXYZ P Q x,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * 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 (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * 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.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₂ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₃ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₄ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
    ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addXYZ P Q x,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addXYZ P Q y,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
rw₅ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
    ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * 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 (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * 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.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₂ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₃ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₄ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
    ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addXYZ P Q x,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addXYZ P Q y,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
rw₅ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
    ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addXYZ P Q y,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
rw₆ :
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
    ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
      HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * 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 (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q] =
  ![HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q,
    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 3 * W'.addY P Q, HPow.hPow (β := ℕ) (u * v) 2 * 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.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addXYZ P P = ![0, 0, 0]
have rw : ![W'.addX P P, W'.addY P P, addZ P P] = ![0, 0, 0]
Tactic: rw [addXYZ, addX_self hP, addY_self hP, addZ_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
rw : ![W'.addX P P, W'.addY P P, addZ P P] = ![0, 0, 0]
⊢ W'.addXYZ P P = ![0, 0, 0]
have rw₁ : ![0, W'.addY P P, addZ P P] = ![0, 0, 0]
Tactic: rw [addXYZ, addX_self hP, addY_self hP, addZ_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
rw : ![W'.addX P P, W'.addY P P, addZ P P] = ![0, 0, 0]
rw₁ : ![0, W'.addY P P, addZ P P] = ![0, 0, 0]
⊢ W'.addXYZ P P = ![0, 0, 0]
have rw₂ : ![0, 0, addZ P P] = ![0, 0, 0]
Tactic: rw [addXYZ, addX_self hP, addY_self hP, addZ_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
rw : ![W'.addX P P, W'.addY P P, addZ P P] = ![0, 0, 0]
rw₁ : ![0, W'.addY P P, addZ P P] = ![0, 0, 0]
rw₂ : ![0, 0, 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 hP, addY_self hP, addZ_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.addXYZ P Q = (P x * Q z) • Q
have rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = (P x * Q z) • Q
Tactic: rw [addXYZ, addX_of_Z_eq_zero_left hPz, addY_of_Z_eq_zero_left hP hPz, addZ_of_Z_eq_zero_left hPz,
    smul_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = (P x * Q z) • Q
⊢ W'.addXYZ P Q = (P x * Q z) • Q
have rw₁ : ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, W'.addY P Q, addZ P Q] = (P x * Q z) • Q
Tactic: rw [addXYZ, addX_of_Z_eq_zero_left hPz, addY_of_Z_eq_zero_left hP hPz, addZ_of_Z_eq_zero_left hPz,
    smul_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = (P x * Q z) • Q
rw₁ : ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, W'.addY P Q, addZ P Q] = (P x * Q z) • Q
⊢ W'.addXYZ P Q = (P x * Q z) • Q
have rw₂ : ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y, addZ P Q] = (P x * Q z) • Q
Tactic: rw [addXYZ, addX_of_Z_eq_zero_left hPz, addY_of_Z_eq_zero_left hP hPz, addZ_of_Z_eq_zero_left hPz,
    smul_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = (P x * Q z) • Q
rw₁ : ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, W'.addY P Q, addZ P Q] = (P x * Q z) • Q
rw₂ : ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y, addZ P Q] = (P x * Q z) • Q
⊢ W'.addXYZ P Q = (P x * Q z) • Q
have rw₃ : ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y, P x * Q z * Q z] = (P x * Q z) • Q
Tactic: rw [addXYZ, addX_of_Z_eq_zero_left hPz, addY_of_Z_eq_zero_left hP hPz, addZ_of_Z_eq_zero_left hPz,
    smul_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = (P x * Q z) • Q
rw₁ : ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, W'.addY P Q, addZ P Q] = (P x * Q z) • Q
rw₂ : ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y, addZ P Q] = (P x * Q z) • Q
rw₃ :
  ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y, P x * Q z * Q z] = (P x * Q z) • Q
⊢ W'.addXYZ P Q = (P x * Q z) • Q
have rw₄ : ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y, P x * Q z * Q z] =
  ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y, P x * Q z * Q z]
Tactic: rw [addXYZ, addX_of_Z_eq_zero_left hPz, addY_of_Z_eq_zero_left hP hPz, addZ_of_Z_eq_zero_left hPz,
    smul_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addXYZ P Q = -(Q x * P z) • P
have rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = -(Q x * P z) • P
Tactic: rw [addXYZ, addX_of_Z_eq_zero_right hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQz, smul_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = -(Q x * P z) • P
⊢ W'.addXYZ P Q = -(Q x * P z) • P
have rw₁ : ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, W'.addY P Q, addZ P Q] = -(Q x * P z) • P
Tactic: rw [addXYZ, addX_of_Z_eq_zero_right hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQz, smul_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = -(Q x * P z) • P
rw₁ : ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, W'.addY P Q, addZ P Q] = -(Q x * P z) • P
⊢ W'.addXYZ P Q = -(Q x * P z) • P
have rw₂ : ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y, addZ P Q] = -(Q x * P z) • P
Tactic: rw [addXYZ, addX_of_Z_eq_zero_right hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQz, smul_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = -(Q x * P z) • P
rw₁ : ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, W'.addY P Q, addZ P Q] = -(Q x * P z) • P
rw₂ :
  ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y, addZ P Q] = -(Q x * P z) • P
⊢ W'.addXYZ P Q = -(Q x * P z) • P
have rw₃ : ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y, -(Q x * P z) * P z] =
  -(Q x * P z) • P
Tactic: rw [addXYZ, addX_of_Z_eq_zero_right hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQz, smul_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = -(Q x * P z) • P
rw₁ : ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, W'.addY P Q, addZ P Q] = -(Q x * P z) • P
rw₂ :
  ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y, addZ P Q] = -(Q x * P z) • P
rw₃ :
  ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y, -(Q x * P z) * P z] =
    -(Q x * P z) • P
⊢ W'.addXYZ P Q = -(Q x * P z) • P
have rw₄ : ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y, -(Q x * P z) * P z] =
  ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y, -(Q x * P z) * P z]
Tactic: rw [addXYZ, addX_of_Z_eq_zero_right hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQz, smul_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (hypothesis)
Goal:
F : Type u
inst : Field F
W : Jacobian 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 * HPow.hPow (β := ℕ) (Q z) 2 ≠ Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ W.addXYZ P Q =
    addZ P Q •
      ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        1]
have hZ : ∀ {n : ℕ}, IsUnit (addZ P Q ^ n)
Tactic: have hZ {n : ℕ} : IsUnit <| addZ P Q ^ n := (isUnit_addZ_of_X_ne hx).pow n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian 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 * HPow.hPow (β := ℕ) (Q z) 2 ≠ Q x * HPow.hPow (β := ℕ) (P z) 2
hZ : ∀ {n : ℕ}, IsUnit (addZ P Q ^ n)
⊢ W.addXYZ P Q =
    addZ P Q •
      ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        1]
have erw : ![W.addX P Q, W.addY P Q, addZ P Q] =
  addZ P Q •
    ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
      W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
        (P y / HPow.hPow (β := ℕ) (P z) 3)
        (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
      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.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian 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 * ((⇑f : (a : R) → S) ∘ P) z -
    (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 3 =
  (f : (a : R) → S) (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)
Tactic: simp only [negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).dblU ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.dblU P)
have simp : (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) y * ((⇑f : (a : R) → S) ∘ P) z -
    (3 * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) x) 2 +
        2 * (W'.map f).a₂ * ((⇑f : (a : R) → S) ∘ P) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 +
      (W'.map f).a₄ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 4) =
  (f : (a : R) → S)
    (W'.a₁ * P y * P z -
      (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
        W'.a₄ * HPow.hPow (β := ℕ) (P z) 4))
Tactic: simp only [dblU_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian 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 *
    (((⇑f : (a : R) → S) ∘ P) y -
      (-((⇑f : (a : R) → S) ∘ P) y - (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) x * ((⇑f : (a : R) → S) ∘ P) z -
        (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 3)) =
  (f : (a : R) → S) (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)))
Tactic: simp only [dblZ, negY]