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.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)
neg : ∀ (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)

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 :
  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
pos₃ pos₄ : Eq (α := W.toAffine.Point) (toAffine W P) (toAffine W P)
⊢ toAffine W (W.add P Q) = 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]

Premises used: WeierstrassCurve.Projective.Point.toAffine_smul, Ne.isUnit, WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, IsUnit.mul, IsUnit.pow, WeierstrassCurve.Projective.add_of_Z_eq_zero_right, And.left, IsUnit.neg, WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero, add_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
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)
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)
⊢ 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

Premises used: WeierstrassCurve.Projective.negY, 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
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
pos : Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)

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

Premises used: WeierstrassCurve.Projective.Y_eq_iff', WeierstrassCurve.Affine.Point.add_of_Y_eq, And.right, And.left, WeierstrassCurve.Projective.Point.toAffine_of_Z_ne_zero, WeierstrassCurve.Projective.X_eq_iff, Iff.mp
-- 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
pos : ∀ (hy : P y * Q z = Q y * P z), Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
neg : ∀ (hy : ¬P y * Q z = Q y * P z), Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0

Tactic:
by_cases hy : P y * Q z = Q y * P z

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
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
hy : P y * Q z = Q y * P z
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0])) 0
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) 0
pos₂ pos₃ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0

Tactic:
rw [add_of_Y_eq hP.left hPz hQz hxy.left hy hxy.right,
            toAffine_smul _ <| isUnit_dblU_of_Y_eq hP hPz hQz hxy.left hy hxy.right, toAffine_zero]

Premises used: WeierstrassCurve.Projective.Point.toAffine_smul, WeierstrassCurve.Projective.isUnit_dblU_of_Y_eq, And.right, And.left, WeierstrassCurve.Projective.add_of_Y_eq, WeierstrassCurve.Projective.Point.toAffine_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
hQz : ¬Q z = 0
hxy : P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z
hy : ¬P y * Q z = Q y * P z
neg :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0])) 0
neg₁ : Eq (α := W.toAffine.Point) (toAffine W ![0, 1, 0]) 0
neg₂ neg₃ : Eq.{u + 1} (α := W.toAffine.Point) 0 0
⊢ Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0

Tactic:
rw [add_of_Y_ne hP.left hQ.left hPz hQz hxy.left hy,
            toAffine_smul _ <| isUnit_addU_of_Y_ne hPz hQz hy, toAffine_zero]

Premises used: WeierstrassCurve.Projective.Point.toAffine_smul, WeierstrassCurve.Projective.isUnit_addU_of_Y_ne, And.left, WeierstrassCurve.Projective.Point.toAffine_zero, WeierstrassCurve.Projective.add_of_Y_ne
-- 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)
⊢ 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:
have := toAffine_add_of_Z_ne_zero hP hQ hPz hQz hxy
-- 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)
this :
  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)
pos :
  ∀ (hx : P x * Q z = Q x * P z),
    toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
neg :
  ∀ (hx : ¬P x * Q z = Q x * 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)

Tactic:
by_cases hx : P x * Q z = Q x * P z

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
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
this :
  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)
hx : P x * Q z = Q x * P z
pos :
  toAffine W
      (W.dblZ P •
        ![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)
pos₁ pos₂ pos₃ pos₄ :
  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)
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)

Tactic:
rwa [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            toAffine_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx]

Premises used: WeierstrassCurve.Projective.Point.toAffine_smul, WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne', And.left, WeierstrassCurve.Projective.add_of_Y_ne', Iff.mp, not_and
-- 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)
this :
  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)
hx : ¬P x * Q z = Q x * P z
neg :
  toAffine W
      (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]) =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
neg₁ neg₂ neg₃ neg₄ :
  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)
⊢ toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)

Tactic:
rwa [add_of_X_ne hP.left hQ.left hPz hQz hx,
            toAffine_smul _ <| isUnit_addZ_of_X_ne hP.left hQ.left hx]

Premises used: WeierstrassCurve.Projective.Point.toAffine_smul, And.left, 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 : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
⊢ { point := ⟦P⟧, nonsingular := hP : W.Point }.toAffineLift = toAffine W P

Tactic:
rfl

Premises used: WeierstrassCurve.Projective.Point.toAffineLift, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ { point := ⟦P⟧, nonsingular := hP : W.Point }.toAffineLift = 0

Tactic:
toAffine_of_Z_eq_zero hPz

Premises used: WeierstrassCurve.Projective.Point.toAffineLift, WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
⊢ Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift 0) 0

Tactic:
toAffine_zero

Premises used: WeierstrassCurve.Projective.Point.toAffineLift, 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.NonsingularLift ⟦P⟧
hPz : P z ≠ 0
⊢ { point := ⟦P⟧, nonsingular := hP : W.Point }.toAffineLift = Affine.Point.some (P x / P z) (P y / P z) ⋯

Tactic:
toAffine_of_Z_ne_zero hP hPz

Premises used: WeierstrassCurve.Projective.Point.toAffineLift, WeierstrassCurve.Projective.Point.toAffine_of_Z_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
X Y : F
h : W.NonsingularLift ⟦![X, Y, 1]⟧
⊢ { point := ⟦![X, Y, 1]⟧, nonsingular := h : W.Point }.toAffineLift = Affine.Point.some X Y ⋯

Tactic:
toAffine_some h

Premises used: WeierstrassCurve.Projective.Point.toAffine_some, WeierstrassCurve.Projective.Point.toAffineLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P : W.Point
mk :
  ∀ {point : 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)),
    (-{ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a,
            nonsingular := hP : W.Point }).toAffineLift =
      -{ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a,
            nonsingular := hP }.toAffineLift
⊢ (-P).toAffineLift = -P.toAffineLift

Tactic:
rcases P with @⟨⟨_⟩, hP⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
point : 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)
⊢ (-{ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point }).toAffineLift =
    -{ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a,
          nonsingular := hP }.toAffineLift

Tactic:
toAffine_neg hP

Premises used: WeierstrassCurve.Projective.Point.toAffine_neg, WeierstrassCurve.Projective.Point.toAffineLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
point : 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)
⊢ (-{ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point }).toAffineLift =
    -{ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a,
          nonsingular := hP }.toAffineLift

Tactic:
exact toAffine_neg hP

Premises used: WeierstrassCurve.Projective.Point.toAffine_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : W.Point
mk :
  ∀ {point : 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))
    {point : PointClass F} (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)),
    ({ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
            W.Point } +
          { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
            nonsingular := hQ : W.Point }).toAffineLift =
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a,
            nonsingular := hP : W.Point }.toAffineLift +
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
            nonsingular := hQ : W.Point }.toAffineLift
⊢ (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift

Tactic:
rcases P, Q with ⟨@⟨⟨_⟩, hP⟩, @⟨⟨_⟩, hQ⟩⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
point : 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)
point_1 : PointClass F
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)
⊢ ({ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point } +
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
          nonsingular := hQ : W.Point }).toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point }.toAffineLift +
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
          nonsingular := hQ : W.Point }.toAffineLift

Tactic:
toAffine_add hP hQ

Premises used: WeierstrassCurve.Projective.Point.toAffineLift, WeierstrassCurve.Projective.Point.toAffine_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
point : 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)
point_1 : PointClass F
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)
⊢ ({ point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point } +
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
          nonsingular := hQ : W.Point }).toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a, nonsingular := hP :
          W.Point }.toAffineLift +
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a_1,
          nonsingular := hQ : W.Point }.toAffineLift

Tactic:
exact toAffine_add hP hQ

Premises used: WeierstrassCurve.Projective.Point.toAffine_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
pos :
  ∀ (hPz : P z = 0),
    fromAffine
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
            nonsingular := hP : W.Point }.toAffineLift =
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
        nonsingular := hP }
neg :
  ∀ (hPz : ¬P z = 0),
    fromAffine
        { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
            nonsingular := hP : W.Point }.toAffineLift =
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
        nonsingular := hP }
⊢ fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }

Tactic:
by_cases hPz : P z = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : P z = 0
pos :
  Point.point (W' := W) (fromAffine 0) =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point
⊢ fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }

Tactic:
rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_eq_zero hPz]

Premises used: WeierstrassCurve.Projective.Point.ext_iff, WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero, WeierstrassCurve.Projective.Point.toAffineLift_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : P z = 0
⊢ Point.point (W' := W) (fromAffine 0) =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point

Tactic:
Quotient.eq.mpr <| Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz

Premises used: Iff.mpr, Setoid.symm, WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : P z = 0
⊢ Point.point (W' := W) (fromAffine 0) =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point

Tactic:
exact Quotient.eq.mpr <| Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz

Premises used: Iff.mpr, Setoid.symm, WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
W' : Projective R
W : Projective F
inst_6 : DecidableEq F
point : PointClass F
P : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P)
hPz : ¬P z = 0
neg :
  (fromAffine (Affine.Point.some (P x / P z) (P y / P z) ⋯)).point =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP :
        W.Point }.point
⊢ fromAffine
      { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P,
          nonsingular := hP : W.Point }.toAffineLift =
    { point := Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) P, nonsingular := hP }

Tactic:
rw [Point.ext_iff, toAffineLift_eq, toAffine_of_Z_ne_zero hP hPz]

Premises used: WeierstrassCurve.Projective.Point.ext_iff, WeierstrassCurve.Projective.Point.toAffine_of_Z_ne_zero, WeierstrassCurve.Projective.Point.toAffineLift_eq