awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₄ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₅ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₆ :
  ![P x, -P y, 0] =
    ![P x * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₇ : ![P x, -P y, 0] = ![P x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₈ : ![P x, -P y, 0] = ![P x, -HPow.hPow (β := ℕ) (P y / P x) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₉ : ![P x, -P y, 0] =
  ![P x, -(HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₄ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₅ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₆ :
  ![P x, -P y, 0] =
    ![P x * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₇ : ![P x, -P y, 0] = ![P x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₈ : ![P x, -P y, 0] = ![P x, -HPow.hPow (β := ℕ) (P y / P x) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₉ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₁₀ : ![P x, -P y, 0] =
  ![P x, -(HPow.hPow (β := ℕ) (P y) 2 * P y / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₄ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₅ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₆ :
  ![P x, -P y, 0] =
    ![P x * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₇ : ![P x, -P y, 0] = ![P x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₈ : ![P x, -P y, 0] = ![P x, -HPow.hPow (β := ℕ) (P y / P x) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₉ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₀ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P y) 2 * P y / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₁₁ : ![P x, -P y, 0] =
  ![P x, -(HPow.hPow (β := ℕ) (P x) 3 * P y / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₄ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₅ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₆ :
  ![P x, -P y, 0] =
    ![P x * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₇ : ![P x, -P y, 0] = ![P x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₈ : ![P x, -P y, 0] = ![P x, -HPow.hPow (β := ℕ) (P y / P x) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₉ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₀ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P y) 2 * P y / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₁ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P x) 3 * P y / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₁₂ : ![P x, -P y, 0] = ![P x, -P y * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₄ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₅ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₆ :
  ![P x, -P y, 0] =
    ![P x * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₇ : ![P x, -P y, 0] = ![P x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₈ : ![P x, -P y, 0] = ![P x, -HPow.hPow (β := ℕ) (P y / P x) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₉ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₀ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P y) 2 * P y / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₁ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P x) 3 * P y / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₂ : ![P x, -P y, 0] = ![P x, -P y * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₁₃ : ![P x, -P y, 0] = ![P x, -P y, -(P y / P x) * ![1, 1, 0] z]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₄ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₅ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₆ :
  ![P x, -P y, 0] =
    ![P x * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₇ : ![P x, -P y, 0] = ![P x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₈ : ![P x, -P y, 0] = ![P x, -HPow.hPow (β := ℕ) (P y / P x) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₉ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₀ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P y) 2 * P y / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₁ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P x) 3 * P y / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₂ : ![P x, -P y, 0] = ![P x, -P y * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₃ : ![P x, -P y, 0] = ![P x, -P y, -(P y / P x) * ![1, 1, 0] z]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
have erw₁₄ : ![P x, -P y, 0] = ![P x, -P y, 0]
Tactic: erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ W.neg P =
    P z •
      ![P x / HPow.hPow (β := ℕ) (P z) 2,
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]
have rw : ![P x, W.negY P, P z] =
  ![HPow.hPow (β := ℕ) (P z) 2 *
      ![P x / HPow.hPow (β := ℕ) (P z) 2,
          W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]
        x,
    HPow.hPow (β := ℕ) (P z) 3 *
      ![P x / HPow.hPow (β := ℕ) (P z) 2,
          W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]
        y,
    P z *
      ![P x / HPow.hPow (β := ℕ) (P z) 2,
          W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]
        z]
Tactic: rw [neg, smul_fin3]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] =
    ![HPow.hPow (β := ℕ) (P z) 2 *
        ![P x / HPow.hPow (β := ℕ) (P z) 2,
            W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]
          x,
      HPow.hPow (β := ℕ) (P z) 3 *
        ![P x / HPow.hPow (β := ℕ) (P z) 2,
            W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]
          y,
      P z *
        ![P x / HPow.hPow (β := ℕ) (P z) 2,
            W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3), 1]
          z]
have simp : ![P x, W.negY P, P z] =
  ![HPow.hPow (β := ℕ) (P z) 2 * (P x / HPow.hPow (β := ℕ) (P z) 2),
    HPow.hPow (β := ℕ) (P z) 3 * W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
    P z * 1]
Tactic: simp only [fin3_def_ext]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ ![P x, W.negY P, P z] =
    ![HPow.hPow (β := ℕ) (P z) 2 * (P x / HPow.hPow (β := ℕ) (P z) 2),
      HPow.hPow (β := ℕ) (P z) 3 *
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
      P z * 1]
have rw : ![P x, W.negY P, P z] =
  ![P x,
    HPow.hPow (β := ℕ) (P z) 3 * W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
    P z * 1]
Tactic: rw [mul_div_cancel₀ _ <| pow_ne_zero 2 hPz, ← negY_of_Z_ne_zero hPz,
    mul_div_cancel₀ _ <| pow_ne_zero 3 hPz, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
rw :
  ![P x, W.negY P, P z] =
    ![P x,
      HPow.hPow (β := ℕ) (P z) 3 *
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
      P z * 1]
⊢ ![P x, W.negY P, P z] =
    ![HPow.hPow (β := ℕ) (P z) 2 * (P x / HPow.hPow (β := ℕ) (P z) 2),
      HPow.hPow (β := ℕ) (P z) 3 *
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
      P z * 1]
have rw₁ : ![P x, W.negY P, P z] = ![P x, HPow.hPow (β := ℕ) (P z) 3 * (W.negY P / HPow.hPow (β := ℕ) (P z) 3), P z * 1]
Tactic: rw [mul_div_cancel₀ _ <| pow_ne_zero 2 hPz, ← negY_of_Z_ne_zero hPz,
    mul_div_cancel₀ _ <| pow_ne_zero 3 hPz, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
rw :
  ![P x, W.negY P, P z] =
    ![P x,
      HPow.hPow (β := ℕ) (P z) 3 *
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
      P z * 1]
rw₁ : ![P x, W.negY P, P z] = ![P x, HPow.hPow (β := ℕ) (P z) 3 * (W.negY P / HPow.hPow (β := ℕ) (P z) 3), P z * 1]
⊢ ![P x, W.negY P, P z] =
    ![HPow.hPow (β := ℕ) (P z) 2 * (P x / HPow.hPow (β := ℕ) (P z) 2),
      HPow.hPow (β := ℕ) (P z) 3 *
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
      P z * 1]
have rw₂ : ![P x, W.negY P, P z] = ![P x, W.negY P, P z * 1]
Tactic: rw [mul_div_cancel₀ _ <| pow_ne_zero 2 hPz, ← negY_of_Z_ne_zero hPz,
    mul_div_cancel₀ _ <| pow_ne_zero 3 hPz, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
rw :
  ![P x, W.negY P, P z] =
    ![P x,
      HPow.hPow (β := ℕ) (P z) 3 *
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
      P z * 1]
rw₁ : ![P x, W.negY P, P z] = ![P x, HPow.hPow (β := ℕ) (P z) 3 * (W.negY P / HPow.hPow (β := ℕ) (P z) 3), P z * 1]
rw₂ : ![P x, W.negY P, P z] = ![P x, W.negY P, P z * 1]
⊢ ![P x, W.negY P, P z] =
    ![HPow.hPow (β := ℕ) (P z) 2 * (P x / HPow.hPow (β := ℕ) (P z) 2),
      HPow.hPow (β := ℕ) (P z) 3 *
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
      P z * 1]
have rw₃ : ![P x, W.negY P, P z] = ![P x, W.negY P, P z]
Tactic: rw [mul_div_cancel₀ _ <| pow_ne_zero 2 hPz, ← negY_of_Z_ne_zero hPz,
    mul_div_cancel₀ _ <| pow_ne_zero 3 hPz, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
⊢ W.Nonsingular (W.neg P)
have pos : ∀ (hPz : P z = 0), W.Nonsingular (W.neg P)
Tactic: by_cases hPz : P z = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
pos : ∀ (hPz : P z = 0), W.Nonsingular (W.neg P)
⊢ W.Nonsingular (W.neg P)
have neg : ∀ (hPz : ¬P z = 0), W.Nonsingular (W.neg P)
Tactic: by_cases hPz : P z = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addX P (W'.neg P) + -2 * HPow.hPow (β := ℕ) (P z) 2 * 0 -
      (HPow.hPow (β := ℕ) (W'.dblZ P) 2 +
        -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 - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) * P z * P z +
                        HPow.hPow (β := ℕ) (P x) 2 * P x * HPow.hPow (β := ℕ) (P z) 2 -
                      W'.a₁ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) *
                          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 - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) * 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 -
    (HPow.hPow (β := ℕ) (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3))) 2 +
      -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, neg_X, neg_Y, neg_Z, dblZ, negY]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addX P (W'.neg P) = HPow.hPow (β := ℕ) (W'.dblZ P) 2
have a : W'.addX P (W'.neg P) + -2 * HPow.hPow (β := ℕ) (P z) 2 * 0 -
    (HPow.hPow (β := ℕ) (W'.dblZ P) 2 +
      -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, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1))
    -2 * P z ^ 2 * (equation_iff _).mp hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negAddY P (W'.neg P) = HPow.hPow (β := ℕ) (W'.dblZ P) 3
have a : W'.negAddY P (W'.neg P) + -2 * HPow.hPow (β := ℕ) (P z) 3 * (P y - W'.negY P) * 0 -
    (HPow.hPow (β := ℕ) (W'.dblZ P) 3 +
      -2 * HPow.hPow (β := ℕ) (P z) 3 * (P y - W'.negY P) *
        (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 [negAddY, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1))
    -2 * P z ^ 3 * (P y - W'.negY P) * (equation_iff _).mp hP