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
⊢ Eq (α := W.toAffine.Point) (toAffine W P) 0
have rw : Eq.{u + 1} (α := W.toAffine.Point)
  (if hP : W.Nonsingular P ∧ P z ≠ 0 then
    Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) sorry
  else 0)
  0
Tactic: rw [toAffine, dif_neg <| not_and_of_not_left _ hP]
-- 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
rw :
  Eq.{u + 1} (α := W.toAffine.Point)
    (if hP : W.Nonsingular P ∧ P z ≠ 0 then
      Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯
    else 0)
    0
⊢ Eq (α := W.toAffine.Point) (toAffine W P) 0
have rw₁ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [toAffine, dif_neg <| not_and_of_not_left _ hP]
-- 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
⊢ Eq (α := W.toAffine.Point) (toAffine W P) 0
have rw : Eq.{u + 1} (α := W.toAffine.Point)
  (if hP : W.Nonsingular P ∧ P z ≠ 0 then
    Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) sorry
  else 0)
  0
Tactic: rw [toAffine, dif_neg <| not_and_not_right.mpr fun _ => hPz]
-- 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 :
  Eq.{u + 1} (α := W.toAffine.Point)
    (if hP : W.Nonsingular P ∧ P z ≠ 0 then
      Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯
    else 0)
    0
⊢ Eq (α := W.toAffine.Point) (toAffine W P) 0
have rw₁ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [toAffine, dif_neg <| not_and_not_right.mpr fun _ => hPz]
-- 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
⊢ toAffine W P = Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯
have rw : (if hP : W.Nonsingular P ∧ P z ≠ 0 then
    Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) sorry
  else 0) =
  Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) sorry
Tactic: rw [toAffine, dif_pos ⟨hP, hPz⟩]
-- 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
rw :
  (if hP : W.Nonsingular P ∧ P z ≠ 0 then
      Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯
    else 0) =
    Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯
⊢ toAffine W P = Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯
have rw₁ : Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) sorry =
  Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) sorry
Tactic: rw [toAffine, dif_pos ⟨hP, hPz⟩]
-- 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
u : F
hu : IsUnit u
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have pos : ∀ (hP : W.Nonsingular P), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
Tactic: by_cases hP : W.Nonsingular P
-- 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
u : F
hu : IsUnit u
pos : ∀ (hP : W.Nonsingular P), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have neg : ∀ (hP : ¬W.Nonsingular P), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
Tactic: by_cases hP : W.Nonsingular P
-- 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
u : F
hu : IsUnit u
hP : W.Nonsingular P
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have pos : ∀ (hPz : P z = 0), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W 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
u : F
hu : IsUnit u
hP : W.Nonsingular P
pos : ∀ (hPz : P z = 0), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have neg : ∀ (hPz : ¬P z = 0), Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W 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
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have pos : Eq (α := W.toAffine.Point) 0 (toAffine W P)
Tactic: rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero hPz]
-- 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
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : P z = 0
pos : Eq (α := W.toAffine.Point) 0 (toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have pos₁ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero hPz]
-- 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
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have neg : (u • P) x / HPow.hPow (β := ℕ) ((u • P) z) 2 = P x / HPow.hPow (β := ℕ) (P z) 2 ∧
  (u • P) y / HPow.hPow (β := ℕ) ((u • P) z) 3 = P y / HPow.hPow (β := ℕ) (P z) 3
Tactic: rw [toAffine_of_Z_ne_zero ((nonsingular_smul P hu).mpr hP) <| mul_ne_zero hu.ne_zero hPz,
        toAffine_of_Z_ne_zero hP hPz, Affine.Point.some.injEq]
-- 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
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have neg : Eq (α := W.toAffine.Point) 0 (toAffine W P)
Tactic: rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]
-- 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
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
neg : Eq (α := W.toAffine.Point) 0 (toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)
have neg₁ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
h : P ≈ Q
⊢ Eq (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have rcases : ∀ (u : Fˣ), Eq (α := W.toAffine.Point) (toAffine W ((fun (m : Fˣ) ↦ m • Q) u)) (toAffine W Q)
Tactic: rcases h with ⟨u, rfl⟩
Cleared hypotheses: P, h
-- 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
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos : ∀ (hPz : P z = 0), Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W 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), Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have neg : ∀ (hPz : ¬P z = 0), Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W 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
hPz : P z = 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos : Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]))
  (-toAffine W P)
Tactic: rw [neg_of_Z_eq_zero hP hPz,
      toAffine_smul _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_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
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]))
    (-toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![1, 1, 0]) (-toAffine W P)
Tactic: rw [neg_of_Z_eq_zero hP hPz,
      toAffine_smul _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_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
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]))
    (-toAffine W P)
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![1, 1, 0]) (-toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos₂ : Eq (α := W.toAffine.Point) 0 (-toAffine W P)
Tactic: rw [neg_of_Z_eq_zero hP hPz,
      toAffine_smul _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_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
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]))
    (-toAffine W P)
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![1, 1, 0]) (-toAffine W P)
pos₂ : Eq (α := W.toAffine.Point) 0 (-toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos₃ : Eq.{u + 1} (α := W.toAffine.Point) 0 (-0)
Tactic: rw [neg_of_Z_eq_zero hP hPz,
      toAffine_smul _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_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
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]))
    (-toAffine W P)
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![1, 1, 0]) (-toAffine W P)
pos₂ : Eq (α := W.toAffine.Point) 0 (-toAffine W P)
pos₃ : Eq.{u + 1} (α := W.toAffine.Point) 0 (-0)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have pos₄ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [neg_of_Z_eq_zero hP hPz,
      toAffine_smul _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_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
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have neg : Eq (α := W.toAffine.Point)
  (toAffine W
    (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]))
  (-toAffine W P)
Tactic: rw [neg_of_Z_ne_zero hPz, toAffine_smul _ <| Ne.isUnit hPz, toAffine_some <|
        (nonsingular_smul _ <| Ne.isUnit hPz).mp <| neg_of_Z_ne_zero hPz ▸ nonsingular_neg hP,
      toAffine_of_Z_ne_zero hP hPz, Affine.Point.neg_some]
-- 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
neg :
  Eq (α := W.toAffine.Point)
    (toAffine W
      (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]))
    (-toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have neg₁ : Eq (α := W.toAffine.Point)
  (toAffine W
    ![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])
  (-toAffine W P)
Tactic: rw [neg_of_Z_ne_zero hPz, toAffine_smul _ <| Ne.isUnit hPz, toAffine_some <|
        (nonsingular_smul _ <| Ne.isUnit hPz).mp <| neg_of_Z_ne_zero hPz ▸ nonsingular_neg hP,
      toAffine_of_Z_ne_zero hP hPz, Affine.Point.neg_some]
-- 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
neg :
  Eq (α := W.toAffine.Point)
    (toAffine W
      (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]))
    (-toAffine W P)
neg₁ :
  Eq (α := W.toAffine.Point)
    (toAffine W
      ![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])
    (-toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have neg₂ : Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2)
    (W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)) sorry =
  -toAffine W P
Tactic: rw [neg_of_Z_ne_zero hPz, toAffine_smul _ <| Ne.isUnit hPz, toAffine_some <|
        (nonsingular_smul _ <| Ne.isUnit hPz).mp <| neg_of_Z_ne_zero hPz ▸ nonsingular_neg hP,
      toAffine_of_Z_ne_zero hP hPz, Affine.Point.neg_some]
-- 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
neg :
  Eq (α := W.toAffine.Point)
    (toAffine W
      (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]))
    (-toAffine W P)
neg₁ :
  Eq (α := W.toAffine.Point)
    (toAffine W
      ![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])
    (-toAffine W P)
neg₂ :
  Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2)
      (W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)) ⋯ =
    -toAffine W P
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have neg₃ : Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2)
    (W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)) sorry =
  -Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) sorry
Tactic: rw [neg_of_Z_ne_zero hPz, toAffine_smul _ <| Ne.isUnit hPz, toAffine_some <|
        (nonsingular_smul _ <| Ne.isUnit hPz).mp <| neg_of_Z_ne_zero hPz ▸ nonsingular_neg hP,
      toAffine_of_Z_ne_zero hP hPz, Affine.Point.neg_some]
-- 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
neg :
  Eq (α := W.toAffine.Point)
    (toAffine W
      (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]))
    (-toAffine W P)
neg₁ :
  Eq (α := W.toAffine.Point)
    (toAffine W
      ![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])
    (-toAffine W P)
neg₂ :
  Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2)
      (W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)) ⋯ =
    -toAffine W P
neg₃ :
  Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2)
      (W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)) ⋯ =
    -Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have neg₄ : Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2)
    (W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)) sorry =
  Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2)
    (W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)) sorry
Tactic: rw [neg_of_Z_ne_zero hPz, toAffine_smul _ <| Ne.isUnit hPz, toAffine_some <|
        (nonsingular_smul _ <| Ne.isUnit hPz).mp <| neg_of_Z_ne_zero hPz ▸ nonsingular_neg hP,
      toAffine_of_Z_ne_zero hP hPz, Affine.Point.neg_some]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy :
  ¬(P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
      P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3)
⊢ toAffine W
      ![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] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have rw : Affine.Point.some
    (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)))
    sorry =
  HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
Tactic: rw [toAffine_some <| nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy, toAffine_of_Z_ne_zero hP hPz,
    toAffine_of_Z_ne_zero hQ hQz,
    Affine.Point.add_some <| by rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy :
  ¬(P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
      P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3)
rw :
  Affine.Point.some
      (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)))
      ⋯ =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
⊢ toAffine W
      ![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] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have rw₁ : Affine.Point.some
    (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)))
    sorry =
  Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) sorry + toAffine W Q
Tactic: rw [toAffine_some <| nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy, toAffine_of_Z_ne_zero hP hPz,
    toAffine_of_Z_ne_zero hQ hQz,
    Affine.Point.add_some <| by rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point (goal)
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have pos : ∀ (hPz : P z = 0), toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
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
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
pos : ∀ (hPz : P z = 0), toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have neg : ∀ (hPz : ¬P z = 0), toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
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
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have pos : Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
Tactic: rw [toAffine_of_Z_eq_zero hPz, zero_add]