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
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw : ![W'.dblX P, W'.dblY P, W'.dblZ P] = ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
rw₁ :
  ![HPow.hPow (β := ℕ) (W'.dblU P) 2, W'.dblY P, W'.dblZ P] =
    ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
⊢ W'.dblXYZ P = ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
have rw₂ : ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, W'.dblZ P] =
  ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
Tactic: rw [dblXYZ, dblX_of_Y_eq hQz hx hy hy', dblY_of_Y_eq hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw : ![W'.dblX P, W'.dblY P, W'.dblZ P] = ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
rw₁ :
  ![HPow.hPow (β := ℕ) (W'.dblU P) 2, W'.dblY P, W'.dblZ P] =
    ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
rw₂ :
  ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, W'.dblZ P] =
    ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
⊢ W'.dblXYZ P = ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
have rw₃ : ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0] =
  ![HPow.hPow (β := ℕ) (W'.dblU P) 2, HPow.hPow (β := ℕ) (W'.dblU P) 3, 0]
Tactic: rw [dblXYZ, dblX_of_Y_eq hQz hx hy hy', dblY_of_Y_eq hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy']
-- 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
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ W.dblXYZ P =
    W.dblZ P •
      ![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 (W.dblZ P ^ n)
Tactic: have hZ {n : ℕ} : IsUnit <| W.dblZ P ^ n := (isUnit_dblZ_of_Y_ne' hP hQ hPz hx hy).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
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W.negY Q * HPow.hPow (β := ℕ) (P z) 3
hZ : ∀ {n : ℕ}, IsUnit (W.dblZ P ^ n)
⊢ W.dblXYZ P =
    W.dblZ P •
      ![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.dblX P, W.dblY P, W.dblZ P] =
  W.dblZ P •
    ![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 [dblXYZ, smul_fin3, ← dblX_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel,
    ← dblY_of_Z_ne_zero hP hQ hPz hQz hx hy, hZ.mul_div_cancel, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z = 0
⊢ addU P Q = 0
have rw : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) = 0
Tactic: rw [addU, hPz, zero_mul, div_zero, neg_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z = 0
rw : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) = 0
⊢ addU P Q = 0
have rw₁ : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (α := F) (β := ℕ) 0 3) / (0 * Q z)) = 0
Tactic: rw [addU, hPz, zero_mul, div_zero, neg_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z = 0
rw : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) = 0
rw₁ : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (α := F) (β := ℕ) 0 3) / (0 * Q z)) = 0
⊢ addU P Q = 0
have rw₂ : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (α := F) (β := ℕ) 0 3) / 0) = 0
Tactic: rw [addU, hPz, zero_mul, div_zero, neg_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z = 0
rw : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) = 0
rw₁ : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (α := F) (β := ℕ) 0 3) / (0 * Q z)) = 0
rw₂ : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (α := F) (β := ℕ) 0 3) / 0) = 0
⊢ addU P Q = 0
have rw₃ : Eq.{u + 1} (α := F) (-0) 0
Tactic: rw [addU, hPz, zero_mul, div_zero, neg_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hPz : P z = 0
rw : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) = 0
rw₁ : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (α := F) (β := ℕ) 0 3) / (0 * Q z)) = 0
rw₂ : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (α := F) (β := ℕ) 0 3) / 0) = 0
rw₃ : Eq.{u + 1} (α := F) (-0) 0
⊢ addU P Q = 0
have rw₄ : Eq.{u + 1} (α := F) 0 0
Tactic: rw [addU, hPz, zero_mul, div_zero, neg_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hQz : Q z = 0
⊢ addU P Q = 0
have rw : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) = 0
Tactic: rw [addU, hQz, mul_zero, div_zero, neg_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hQz : Q z = 0
rw : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) = 0
⊢ addU P Q = 0
have rw₁ : -((P y * HPow.hPow (α := F) (β := ℕ) 0 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * 0)) = 0
Tactic: rw [addU, hQz, mul_zero, div_zero, neg_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hQz : Q z = 0
rw : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) = 0
rw₁ : -((P y * HPow.hPow (α := F) (β := ℕ) 0 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * 0)) = 0
⊢ addU P Q = 0
have rw₂ : -((P y * HPow.hPow (α := F) (β := ℕ) 0 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / 0) = 0
Tactic: rw [addU, hQz, mul_zero, div_zero, neg_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hQz : Q z = 0
rw : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) = 0
rw₁ : -((P y * HPow.hPow (α := F) (β := ℕ) 0 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * 0)) = 0
rw₂ : -((P y * HPow.hPow (α := F) (β := ℕ) 0 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / 0) = 0
⊢ addU P Q = 0
have rw₃ : Eq.{u + 1} (α := F) (-0) 0
Tactic: rw [addU, hQz, mul_zero, div_zero, neg_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
P Q : Fin 3 → F
hQz : Q z = 0
rw : -((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)) = 0
rw₁ : -((P y * HPow.hPow (α := F) (β := ℕ) 0 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * 0)) = 0
rw₂ : -((P y * HPow.hPow (α := F) (β := ℕ) 0 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / 0) = 0
rw₃ : Eq.{u + 1} (α := F) (-0) 0
⊢ addU P Q = 0
have rw₄ : Eq.{u + 1} (α := F) 0 0
Tactic: rw [addU, hQz, mul_zero, div_zero, neg_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
u v : R
⊢ addZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 * addZ P Q
have simp : HPow.hPow (β := ℕ) u 2 * P x * HPow.hPow (β := ℕ) (v * Q z) 2 -
    HPow.hPow (β := ℕ) v 2 * Q x * HPow.hPow (β := ℕ) (u * P z) 2 =
  HPow.hPow (β := ℕ) (u * v) 2 * (P x * HPow.hPow (β := ℕ) (Q z) 2 - Q x * HPow.hPow (β := ℕ) (P z) 2)
Tactic: simp only [addZ, smul_fin3_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
⊢ addZ P Q = P x * Q z * Q z
have rw : P x * HPow.hPow (β := ℕ) (Q z) 2 - Q x * HPow.hPow (α := R) (β := ℕ) 0 2 = P x * Q z * Q z
Tactic: rw [addZ, hPz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hQz : Q z = 0
⊢ addZ P Q = -(Q x * P z) * P z
have rw : P x * HPow.hPow (α := R) (β := ℕ) 0 2 - Q x * HPow.hPow (β := ℕ) (P z) 2 = -(Q x * P z) * P z
Tactic: rw [addZ, hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ addZ P Q = 0
have rw : P x * HPow.hPow (β := ℕ) (Q z) 2 - Q x * HPow.hPow (β := ℕ) (P z) 2 = 0
Tactic: rw [addZ, hx, sub_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw : P x * HPow.hPow (β := ℕ) (Q z) 2 - Q x * HPow.hPow (β := ℕ) (P z) 2 = 0
⊢ addZ P Q = 0
have rw₁ : Q x * HPow.hPow (β := ℕ) (P z) 2 - Q x * HPow.hPow (β := ℕ) (P z) 2 = 0
Tactic: rw [addZ, hx, sub_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
R : Type r
inst : CommRing R
P Q : Fin 3 → R
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
rw : P x * HPow.hPow (β := ℕ) (Q z) 2 - Q x * HPow.hPow (β := ℕ) (P z) 2 = 0
rw₁ : Q x * HPow.hPow (β := ℕ) (P z) 2 - Q x * HPow.hPow (β := ℕ) (P z) 2 = 0
⊢ addZ P Q = 0
have rw₂ : Eq.{r + 1} (α := R) 0 0
Tactic: rw [addZ, hx, sub_self]
-- 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
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 ≠ Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ P x / HPow.hPow (β := ℕ) (P z) 2 ≠ Q x / HPow.hPow (β := ℕ) (Q z) 2
have rwa : ¬P x / HPow.hPow (β := ℕ) (P z) 2 = Q x / HPow.hPow (β := ℕ) (Q z) 2
Tactic: rwa [ne_eq, ← X_eq_iff hPz hQz]
-- 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
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 ≠ Q x * HPow.hPow (β := ℕ) (P z) 2
rwa : ¬P x / HPow.hPow (β := ℕ) (P z) 2 = Q x / HPow.hPow (β := ℕ) (Q z) 2
⊢ P x / HPow.hPow (β := ℕ) (P z) 2 ≠ Q x / HPow.hPow (β := ℕ) (Q z) 2
have rwa₁ : ¬P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
Tactic: rwa [ne_eq, ← X_eq_iff hPz hQz]
-- 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
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 ≠ Q x * HPow.hPow (β := ℕ) (P 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) =
    (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z * addZ P Q)
have rw : (P y / HPow.hPow (β := ℕ) (P z) 3 - Q y / HPow.hPow (β := ℕ) (Q z) 3) /
    ((P x * HPow.hPow (β := ℕ) (Q z) 2 - Q x * HPow.hPow (β := ℕ) (P z) 2) /
      (HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2)) =
  (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) /
    (P z * Q z * (P x * HPow.hPow (β := ℕ) (Q z) 2 - Q x * HPow.hPow (β := ℕ) (P z) 2))
Tactic: rw [Affine.slope_of_X_ne <| by rwa [ne_eq, ← X_eq_iff hPz hQz],
    div_sub_div _ _ (pow_ne_zero 2 hPz) (pow_ne_zero 2 hQz), mul_comm <| _ ^ 2, addZ]
-- 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
hQ : W'.Equation Q
⊢ W'.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 =
    HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 +
            W'.a₁ * (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) * P z * Q z * addZ P Q -
          W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
        P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
      Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2
have a : W'.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 +
      (-HPow.hPow (β := ℕ) (Q z) 6 * 0 +
        HPow.hPow (β := ℕ) (P z) 6 *
          (HPow.hPow (β := ℕ) (Q y) 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * HPow.hPow (β := ℕ) (Q z) 3 -
            (HPow.hPow (β := ℕ) (Q x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                W'.a₄ * Q x * HPow.hPow (β := ℕ) (Q z) 4 +
              W'.a₆ * HPow.hPow (β := ℕ) (Q z) 6))) -
    (HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 +
              W'.a₁ * (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) * P z * Q z * addZ P Q -
            W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
          P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
        Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 +
      (-HPow.hPow (β := ℕ) (Q z) 6 *
          (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 6)) +
        HPow.hPow (β := ℕ) (P z) 6 * 0)) =
  0
Tactic: linear_combination (norm := (rw [addX, addZ]; ring1)) -Q z ^ 6 * (equation_iff P).mp hP
    - P z ^ 6 * (equation_iff Q).mp hQ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addX P Q =
    (HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 +
              W.a₁ * (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) * P z * Q z * addZ P Q -
            W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
          P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
        Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2) /
      HPow.hPow (β := ℕ) (P z * Q z) 2
have rw : W.addX P Q = W.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 / HPow.hPow (β := ℕ) (P z * Q z) 2
Tactic: rw [← addX_eq' hP hQ, mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
rw : W.addX P Q = W.addX P Q * HPow.hPow (β := ℕ) (P z * Q z) 2 / HPow.hPow (β := ℕ) (P z * Q z) 2
⊢ W.addX P Q =
    (HPow.hPow (β := ℕ) (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) 2 +
              W.a₁ * (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) * P z * Q z * addZ P Q -
            W.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
          P x * HPow.hPow (β := ℕ) (Q z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2 -
        Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (addZ P Q) 2) /
      HPow.hPow (β := ℕ) (P z * Q z) 2
have rw₁ : W.addX P Q = W.addX P Q
Tactic: rw [← addX_eq' hP hQ, mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]
-- 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
⊢ W'.addX (u • P) (v • Q) = HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 * W'.addX P Q
have simp : HPow.hPow (β := ℕ) u 2 * P x * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) v 2 * Q x) 2 * HPow.hPow (β := ℕ) (u * P z) 2 -
                      2 * (HPow.hPow (β := ℕ) u 3 * P y) * (HPow.hPow (β := ℕ) v 3 * Q y) * (u * P z) * (v * Q z) +
                    HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) u 2 * P x) 2 * (HPow.hPow (β := ℕ) v 2 * Q x) *
                      HPow.hPow (β := ℕ) (v * Q z) 2 -
                  W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) v 3 * Q y) *
                      HPow.hPow (β := ℕ) (u * P z) 2 *
                    (v * Q z) -
                W'.a₁ * (HPow.hPow (β := ℕ) u 3 * P y) * (HPow.hPow (β := ℕ) v 2 * Q x) * (u * P z) *
                  HPow.hPow (β := ℕ) (v * Q z) 2 +
              2 * W'.a₂ * (HPow.hPow (β := ℕ) u 2 * P x) * (HPow.hPow (β := ℕ) v 2 * Q x) *
                  HPow.hPow (β := ℕ) (u * P z) 2 *
                HPow.hPow (β := ℕ) (v * Q z) 2 -
            W'.a₃ * (HPow.hPow (β := ℕ) v 3 * Q y) * HPow.hPow (β := ℕ) (u * P z) 4 * (v * Q z) -
          W'.a₃ * (HPow.hPow (β := ℕ) u 3 * P y) * (u * P z) * HPow.hPow (β := ℕ) (v * Q z) 4 +
        W'.a₄ * (HPow.hPow (β := ℕ) v 2 * Q x) * HPow.hPow (β := ℕ) (u * P z) 4 * HPow.hPow (β := ℕ) (v * Q z) 2 +
      W'.a₄ * (HPow.hPow (β := ℕ) u 2 * P x) * HPow.hPow (β := ℕ) (u * P z) 2 * HPow.hPow (β := ℕ) (v * Q z) 4 +
    2 * W'.a₆ * HPow.hPow (β := ℕ) (u * P z) 4 * HPow.hPow (β := ℕ) (v * Q z) 4 =
  HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (u * v) 2) 2 *
    (P x * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 - 2 * P y * Q y * P z * Q z +
                      HPow.hPow (β := ℕ) (P x) 2 * Q x * HPow.hPow (β := ℕ) (Q z) 2 -
                    W'.a₁ * P x * Q y * HPow.hPow (β := ℕ) (P z) 2 * Q z -
                  W'.a₁ * P y * Q x * P z * HPow.hPow (β := ℕ) (Q z) 2 +
                2 * W'.a₂ * P x * Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
              W'.a₃ * Q y * HPow.hPow (β := ℕ) (P z) 4 * Q z -
            W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (Q z) 4 +
          W'.a₄ * Q x * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 2 +
        W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 4 +
      2 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 4)
Tactic: simp only [addX, smul_fin3_ext]
-- 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'.addX P P + -2 * HPow.hPow (β := ℕ) (P z) 2 * 0 -
      (0 +
        -2 * HPow.hPow (β := ℕ) (P z) 2 *
          (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 6))) =
    0
have a : P x * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 - 2 * P y * P y * P z * P z +
                        HPow.hPow (β := ℕ) (P x) 2 * P x * HPow.hPow (β := ℕ) (P z) 2 -
                      W'.a₁ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 * P z -
                    W'.a₁ * P y * P x * P z * HPow.hPow (β := ℕ) (P z) 2 +
                  2 * W'.a₂ * P x * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 4 * P z -
              W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (P z) 4 +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P z) 4 +
        2 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (P z) 4 +
      -2 * HPow.hPow (β := ℕ) (P z) 2 * 0 -
    (0 +
      -2 * HPow.hPow (β := ℕ) (P z) 2 *
        (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
          (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
            W'.a₆ * HPow.hPow (β := ℕ) (P z) 6))) =
  0
Tactic: rw [addX]
-- 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'.addX P P = 0
have a : W'.addX P P + -2 * HPow.hPow (β := ℕ) (P z) 2 * 0 -
    (0 +
      -2 * HPow.hPow (β := ℕ) (P z) 2 *
        (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
          (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
            W'.a₆ * HPow.hPow (β := ℕ) (P z) 6))) =
  0
Tactic: linear_combination (norm := (rw [addX]; ring1)) -2 * P z ^ 2 * (equation_iff _).mp hP