awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 / P z, W.toAffine.negY (P x / P z) (P y / P z), 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
neg :
  Eq (α := W.toAffine.Point) (toAffine W (P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 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 / P z, W.toAffine.negY (P x / P z) (P y / P z), 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
neg :
  Eq (α := W.toAffine.Point) (toAffine W (P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]))
    (-toAffine W P)
neg₁ : Eq (α := W.toAffine.Point) (toAffine W ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]) (-toAffine W P)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have neg₂ : Affine.Point.some (P x / P z) (W.toAffine.negY (P x / P z) (P y / P z)) 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
neg :
  Eq (α := W.toAffine.Point) (toAffine W (P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]))
    (-toAffine W P)
neg₁ : Eq (α := W.toAffine.Point) (toAffine W ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]) (-toAffine W P)
neg₂ : Affine.Point.some (P x / P z) (W.toAffine.negY (P x / P z) (P y / P z)) ⋯ = -toAffine W P
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have neg₃ : Affine.Point.some (P x / P z) (W.toAffine.negY (P x / P z) (P y / P z)) sorry = -Affine.Point.some (P x / P z) (P y / P z) 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
neg :
  Eq (α := W.toAffine.Point) (toAffine W (P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]))
    (-toAffine W P)
neg₁ : Eq (α := W.toAffine.Point) (toAffine W ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]) (-toAffine W P)
neg₂ : Affine.Point.some (P x / P z) (W.toAffine.negY (P x / P z) (P y / P z)) ⋯ = -toAffine W P
neg₃ :
  Affine.Point.some (P x / P z) (W.toAffine.negY (P x / P z) (P y / P z)) ⋯ =
    -Affine.Point.some (P x / P z) (P y / P z) ⋯
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)
have neg₄ : Affine.Point.some (P x / P z) (W.toAffine.negY (P x / P z) (P y / P z)) sorry =
  Affine.Point.some (P x / P z) (W.toAffine.negY (P x / P z) (P y / P z)) 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ toAffine W
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have rw : Affine.Point.some
    (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
    (W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
    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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
rw :
  Affine.Point.some
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      ⋯ =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
⊢ toAffine W
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have rw₁ : Affine.Point.some
    (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
    (W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
    sorry =
  Affine.Point.some (P x / P z) (P y / P z) 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
rw :
  Affine.Point.some
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      ⋯ =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
rw₁ :
  Affine.Point.some
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      ⋯ =
    Affine.Point.some (P x / P z) (P y / P z) ⋯ + toAffine W Q
⊢ toAffine W
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have rw₂ : Affine.Point.some
    (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
    (W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
    sorry =
  Affine.Point.some (P x / P z) (P y / P z) sorry + Affine.Point.some (Q x / Q z) (Q y / Q z) sorry
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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
rw :
  Affine.Point.some
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      ⋯ =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
rw₁ :
  Affine.Point.some
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      ⋯ =
    Affine.Point.some (P x / P z) (P y / P z) ⋯ + toAffine W Q
rw₂ :
  Affine.Point.some
      (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      (W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
      ⋯ =
    Affine.Point.some (P x / P z) (P y / P z) ⋯ + Affine.Point.some (Q x / Q z) (Q y / Q z) ⋯
⊢ toAffine W
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have rw₃ : Affine.Point.some
    (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
    (W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
    sorry =
  Affine.Point.some
    (W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
    (W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)))
    sorry
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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
have pos : ∀ (hQz : Q z = 0), Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
Tactic: by_cases hQz : Q z = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
pos : ∀ (hQz : Q z = 0), Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
have neg : ∀ (hQz : ¬Q z = 0), Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
Tactic: by_cases hQz : Q z = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
have pos : Eq (α := W.toAffine.Point)
  (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]))
  (toAffine W Q)
Tactic: rw [add_of_Z_eq_zero hP hQ hPz hQz, toAffine_smul _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4,
        toAffine_zero, toAffine_of_Z_eq_zero hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
pos :
  Eq (α := W.toAffine.Point)
    (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]))
    (toAffine W Q)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
have pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) (toAffine W Q)
Tactic: rw [add_of_Z_eq_zero hP hQ hPz hQz, toAffine_smul _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4,
        toAffine_zero, toAffine_of_Z_eq_zero hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
pos :
  Eq (α := W.toAffine.Point)
    (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]))
    (toAffine W Q)
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) (toAffine W Q)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
have pos₂ : Eq (α := W.toAffine.Point) 0 (toAffine W Q)
Tactic: rw [add_of_Z_eq_zero hP hQ hPz hQz, toAffine_smul _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4,
        toAffine_zero, toAffine_of_Z_eq_zero hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
pos :
  Eq (α := W.toAffine.Point)
    (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]))
    (toAffine W Q)
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) (toAffine W Q)
pos₂ : Eq (α := W.toAffine.Point) 0 (toAffine W Q)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
have pos₃ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
Tactic: rw [add_of_Z_eq_zero hP hQ hPz hQz, toAffine_smul _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4,
        toAffine_zero, toAffine_of_Z_eq_zero hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
have neg : Eq (α := W.toAffine.Point) (toAffine W ((HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q)) (toAffine W Q)
Tactic: rw [add_of_Z_eq_zero_left hP.left hPz hQz,
        toAffine_smul _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).mul <| Ne.isUnit hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
neg : Eq (α := W.toAffine.Point) (toAffine W ((HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q)) (toAffine W Q)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
have neg₁ : Eq (α := W.toAffine.Point) (toAffine W Q) (toAffine W Q)
Tactic: rw [add_of_Z_eq_zero_left hP.left hPz hQz,
        toAffine_smul _ <| ((isUnit_Y_of_Z_eq_zero hP hPz).pow 2).mul <| Ne.isUnit hQz]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 : ∀ (hQz : Q z = 0), toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
Tactic: by_cases hQz : Q z = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
pos : ∀ (hQz : Q 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 : ∀ (hQz : ¬Q z = 0), toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
Tactic: by_cases hQz : Q z = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have pos : toAffine W (-(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
Tactic: rw [add_of_Z_eq_zero_right hQ.left hPz hQz,
        toAffine_smul _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg,
        toAffine_of_Z_eq_zero hQz, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
pos :
  toAffine W (-(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P) = 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 pos₁ : toAffine W P = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
Tactic: rw [add_of_Z_eq_zero_right hQ.left hPz hQz,
        toAffine_smul _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg,
        toAffine_of_Z_eq_zero hQz, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
pos :
  toAffine W (-(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
pos₁ : toAffine W P = 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 pos₂ : toAffine W P = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) 0
Tactic: rw [add_of_Z_eq_zero_right hQ.left hPz hQz,
        toAffine_smul _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg,
        toAffine_of_Z_eq_zero hQz, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
pos :
  toAffine W (-(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
pos₁ : toAffine W P = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
pos₂ : toAffine W P = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) 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 P) (toAffine W P)
Tactic: rw [add_of_Z_eq_zero_right hQ.left hPz hQz,
        toAffine_smul _ (((isUnit_Y_of_Z_eq_zero hQ hQz).pow 2).mul <| Ne.isUnit hPz).neg,
        toAffine_of_Z_eq_zero hQz, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
have pos : ∀ (hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z),
  toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
Tactic: by_cases hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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
pos :
  ∀ (hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z),
    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 : ∀ (hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)),
  toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
Tactic: by_cases hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point (goal)
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
⊢ 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)) 0
Tactic: rw [toAffine_of_Z_ne_zero hP hPz, toAffine_of_Z_ne_zero hQ hQz, Affine.Point.add_of_Y_eq
            ((X_eq_iff hPz hQz).mp hxy.left) ((Y_eq_iff' hPz hQz).mp hxy.right)]