awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
hx : ¬P x * Q z = Q x * P z
neg :
  Eq (α := PointClass F) ⟦W.add P Q⟧
    ⟦![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]⟧
neg₁ :
  Eq (α := PointClass F)
    ⟦W.addZ P Q •
        ![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]⟧
    ⟦![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]⟧
neg₂ neg₃ :
  Eq (α := PointClass F)
    ⟦![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]⟧
    ⟦![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]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧)
    ⟦![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]⟧

Tactic:
rw [addMap_eq, add_of_X_ne hP hQ hPz hQz hx, smul_eq _ <| isUnit_addZ_of_X_ne hP hQ hx]

Premises used: WeierstrassCurve.Projective.smul_eq, WeierstrassCurve.Projective.addMap_eq, WeierstrassCurve.Projective.add_of_X_ne, WeierstrassCurve.Projective.isUnit_addZ_of_X_ne
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : PointClass F
hP : W.NonsingularLift P
hQ : W.NonsingularLift Q
mk :
  ∀ (a : Fin 3 → F)
    (hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)),
    W.NonsingularLift (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a) Q)
⊢ W.NonsingularLift (W.addMap P Q)

Tactic:
rcases P
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : PointClass F
hQ : W.NonsingularLift Q
a : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)
mk :
  ∀ (a_1 : Fin 3 → F)
    (hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1)),
    W.NonsingularLift
      (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)
        (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1))
⊢ W.NonsingularLift (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a) Q)

Tactic:
rcases Q
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : PointClass F
a : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)
a_1 : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1)
⊢ W.NonsingularLift
    (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)
      (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1))

Tactic:
nonsingular_add hP hQ

Premises used: WeierstrassCurve.Projective.nonsingular_add, WeierstrassCurve.Projective.NonsingularLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : PointClass F
a : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)
a_1 : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1)
⊢ W.NonsingularLift
    (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a)
      (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1))

Tactic:
exact nonsingular_add hP hQ

Premises used: WeierstrassCurve.Projective.nonsingular_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : PointClass R
h : W'.NonsingularLift P
⊢ { point := P, nonsingular := h : W'.Point }.point = P

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : Nontrivial R
⊢ Eq.{r + 1} (α := W'.Point) 0 { point := ⟦![0, 1, 0]⟧, nonsingular := ⋯ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : Nontrivial R
⊢ Eq.{r + 1} (α := PointClass R) (point (W' := W') 0) ⟦![0, 1, 0]⟧

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : Nontrivial R
X Y : R
h : W'.NonsingularLift ⟦![X, Y, 1]⟧
⊢ { point := ⟦![X, Y, 1]⟧, nonsingular := h : W'.Point } ≠ 0

Tactic:
(not_equiv_of_Z_eq_zero_right one_ne_zero rfl).comp <| Quotient.eq.mp.comp Point.ext_iff.mp

Premises used: WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_right, Function.comp, WeierstrassCurve.Projective.Point.ext_iff, Iff.mp, Not, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : Nontrivial R
⊢ Eq.{r + 1} (α := W'.Point) (fromAffine 0) 0

Tactic:
rfl

Premises used: WeierstrassCurve.Projective.Point.fromAffine, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : Nontrivial R
X Y : R
h : W'.toAffine.Nonsingular X Y
⊢ fromAffine (Affine.Point.some X Y h) = { point := ⟦![X, Y, 1]⟧, nonsingular := ⋯ }

Tactic:
rfl

Premises used: WeierstrassCurve.Projective.Point.fromAffine, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : Nontrivial R
X Y : R
h : W'.toAffine.Nonsingular X Y
⊢ fromAffine (Affine.Point.some X Y h) ≠ 0

Tactic:
mk_ne_zero <| (nonsingularLift_some ..).mpr h

Premises used: Iff.mpr, WeierstrassCurve.Projective.nonsingularLift_some, WeierstrassCurve.Projective.Point.mk_ne_zero, WeierstrassCurve.Projective.Point.fromAffine
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P : W.Point
⊢ -P = P.neg

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P : W.Point
⊢ (-P).point = W.negMap P.point

Tactic:
rfl

Premises used: Quotient.map, Quot.map, WeierstrassCurve.Projective.negMap, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : W.Point
⊢ P + Q = P.add Q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : W.Point
⊢ (P + Q).point = W.addMap P.point Q.point

Tactic:
rfl

Premises used: Quotient.map₂, WeierstrassCurve.Projective.addMap, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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 / P z) (P y / P z) ⋯ else 0) 0
rw₁ rw₂ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
⊢ Eq (α := W.toAffine.Point) (toAffine W P) 0

Tactic:
rw [toAffine, dif_neg <| not_and_of_not_left _ hP]

Premises used: not_and_of_not_left, dif_neg, WeierstrassCurve.Projective.Point.toAffine
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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 / P z) (P y / P z) ⋯ else 0) 0
rw₁ rw₂ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
⊢ Eq (α := W.toAffine.Point) (toAffine W P) 0

Tactic:
rw [toAffine, dif_neg <| not_and_not_right.mpr fun _ => hPz]

Premises used: Iff.mpr, dif_neg, not_and_not_right, WeierstrassCurve.Projective.Point.toAffine
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
⊢ Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) 0

Tactic:
toAffine_of_Z_eq_zero rfl

Premises used: WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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 / P z) (P y / P z) ⋯ else 0) =
    Affine.Point.some (P x / P z) (P y / P z) ⋯
rw₁ rw₂ : Affine.Point.some (P x / P z) (P y / P z) ⋯ = Affine.Point.some (P x / P z) (P y / P z) ⋯
⊢ toAffine W P = Affine.Point.some (P x / P z) (P y / P z) ⋯

Tactic:
rw [toAffine, dif_pos ⟨hP, hPz⟩]

Premises used: dif_pos, WeierstrassCurve.Projective.Point.toAffine
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
X Y : F
h : W.Nonsingular ![X, Y, 1]
⊢ toAffine W ![X, Y, 1] = Affine.Point.some X Y ⋯

Tactic:
simp only [toAffine_of_Z_ne_zero h one_ne_zero, fin3_def_ext, div_one]

Premises used: WeierstrassCurve.Projective.fin3_def_ext, WeierstrassCurve.Projective.Point.toAffine_of_Z_ne_zero, one_ne_zero, div_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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)
neg : ∀ (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)

Tactic:
by_cases hP : W.Nonsingular P

Premises used: WeierstrassCurve.Projective.Nonsingular
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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)
neg : ∀ (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)

Tactic:
by_cases hPz : P z = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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)
pos₁ pos₂ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)

Tactic:
rw [toAffine_of_Z_eq_zero <| mul_eq_zero_of_right u hPz, toAffine_of_Z_eq_zero hPz]

Premises used: mul_eq_zero_of_right, WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
neg : (u • P) x / (u • P) z = P x / P z ∧ (u • P) y / (u • P) z = P y / P z
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)

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]

Premises used: Iff.mpr, WeierstrassCurve.Projective.Point.toAffine_of_Z_ne_zero, WeierstrassCurve.Affine.Point.some.injEq, IsUnit.ne_zero, mul_ne_zero, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ (u • P) x / (u • P) z = P x / P z ∧ (u • P) y / (u • P) z = P y / P z

Tactic:
simp only [smul_fin3_ext, mul_div_mul_left _ _ hu.ne_zero, and_self]

Premises used: and_self, mul_div_mul_left, IsUnit.ne_zero, WeierstrassCurve.Projective.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
u : F
hu : IsUnit u
hP : ¬W.Nonsingular P
neg : Eq (α := W.toAffine.Point) 0 (toAffine W P)
neg₁ neg₂ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (u • P)) (toAffine W P)

Tactic:
rw [toAffine_of_singular <| hP.comp (nonsingular_smul P hu).mp, toAffine_of_singular hP]

Premises used: Function.comp, WeierstrassCurve.Projective.Point.toAffine_of_singular, Iff.mp, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
h : P ≈ Q
rcases : ∀ (u : Fˣ), Eq (α := W.toAffine.Point) (toAffine W ((fun (m : Fˣ) ↦ m • Q) u)) (toAffine W Q)
⊢ Eq (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)

Tactic:
rcases h with ⟨u, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
Q : Fin 3 → F
u : Fˣ
⊢ Eq (α := W.toAffine.Point) (toAffine W ((fun (m : Fˣ) ↦ m • Q) u)) (toAffine W Q)

Tactic:
toAffine_smul Q u.isUnit

Premises used: WeierstrassCurve.Projective.Point.toAffine_smul, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
Q : Fin 3 → F
u : Fˣ
⊢ Eq (α := W.toAffine.Point) (toAffine W ((fun (m : Fˣ) ↦ m • Q) u)) (toAffine W Q)

Tactic:
exact toAffine_smul Q u.isUnit

Premises used: WeierstrassCurve.Projective.Point.toAffine_smul, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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)
neg : ∀ (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)

Tactic:
by_cases hPz : P z = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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) ![0, 1, 0]))
    (-toAffine W P)
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) (-toAffine W P)
pos₂ : Eq (α := W.toAffine.Point) 0 (-toAffine W P)
pos₃ : Eq.{u + 1} (α := W.toAffine.Point) 0 (-0)
pos₄ pos₅ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-toAffine W P)

Tactic:
rw [neg_of_Z_eq_zero hP.left hPz, toAffine_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg,
      toAffine_zero, toAffine_of_Z_eq_zero hPz, Affine.Point.neg_zero]

Premises used: WeierstrassCurve.Projective.Point.toAffine_smul, WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, WeierstrassCurve.Affine.Point.neg_zero, And.left, WeierstrassCurve.Projective.neg_of_Z_eq_zero, IsUnit.neg, WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero, WeierstrassCurve.Projective.Point.toAffine_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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) ⋯
neg₄ 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) (W.toAffine.negY (P x / P z) (P y / P z)) ⋯
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.neg P)) (-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]

Premises used: WeierstrassCurve.Projective.Point.toAffine_smul, WeierstrassCurve.Projective.Point.toAffine_some, Ne.isUnit, WeierstrassCurve.Affine.Point.neg_some, WeierstrassCurve.Projective.neg_of_Z_ne_zero, WeierstrassCurve.Projective.Point.toAffine_of_Z_ne_zero, Iff.mp, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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) ⋯
rw₃ 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
      (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)))
      ⋯
⊢ 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)

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]]

Premises used: WeierstrassCurve.Projective.Point.toAffine_some, WeierstrassCurve.Projective.Point.toAffine_of_Z_ne_zero, WeierstrassCurve.Affine.Point.add_some, _private.0.WeierstrassCurve.Projective.nonsingular_add_of_Z_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)
neg : ∀ (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)

Tactic:
by_cases hPz : P z = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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 : Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (toAffine W Q)
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)

Tactic:
rw [toAffine_of_Z_eq_zero hPz, zero_add]

Premises used: zero_add, WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)
neg : ∀ (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)

Tactic:
by_cases hQz : Q z = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)
pos₃ pos₄ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) (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]

Premises used: WeierstrassCurve.Projective.Point.toAffine_smul, WeierstrassCurve.Projective.add_of_Z_eq_zero, WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, IsUnit.pow, WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero, WeierstrassCurve.Projective.Point.toAffine_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
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)
neg₁ neg₂ : Eq (α := W.toAffine.Point) (toAffine W Q) (toAffine W Q)
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P 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]

Premises used: WeierstrassCurve.Projective.Point.toAffine_smul, Ne.isUnit, WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, WeierstrassCurve.Projective.add_of_Z_eq_zero_left, IsUnit.mul, IsUnit.pow, And.left, OfNat.ofNat