awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P_1 : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
pos : (MulAction.orbitRel Fˣ (Fin 3 → F) : (Fin 3 → F) → (Fin 3 → F) → Prop) ![1, 1, 0] P
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧

Tactic:
rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
      smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2, Quotient.eq]

Premises used: IsUnit.pow, WeierstrassCurve.Jacobian.smul_eq, WeierstrassCurve.Jacobian.addMap_eq, OfNat.ofNat, WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero, WeierstrassCurve.Jacobian.add_of_Z_eq_zero, Quotient.eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P_1 : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F) : (Fin 3 → F) → (Fin 3 → F) → Prop) ![1, 1, 0] P

Tactic:
Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz

Premises used: WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero, Setoid.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P_1 : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : P z = 0
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F) : (Fin 3 → F) → (Fin 3 → F) → Prop) ![1, 1, 0] P

Tactic:
exact Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz

Premises used: WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero, Setoid.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P_1 : PointClass F
Q : Fin 3 → F
hQ : W.Nonsingular Q
hQz : Q z = 0
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
hPz : ¬P z = 0
neg : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦P⟧
neg₁ : Eq (α := PointClass F) ⟦-(Q x * P z) • P⟧ ⟦P⟧
neg₂ neg₃ : Eq (α := PointClass F) ⟦P⟧ ⟦P⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦P⟧

Tactic:
rw [addMap_eq, add_of_Z_eq_zero_right hQ.left hPz hQz,
      smul_eq _ ((isUnit_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg]

Premises used: Ne.isUnit, IsUnit.mul, And.left, IsUnit.neg, WeierstrassCurve.Jacobian.smul_eq, WeierstrassCurve.Jacobian.addMap_eq, WeierstrassCurve.Jacobian.add_of_Z_eq_zero_right, WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3
pos :
  ∀ (hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3),
    Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![1, 1, 0]⟧
neg :
  ∀ (hy : ¬P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3),
    Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![1, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![1, 1, 0]⟧

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

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
pos : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦![1, 1, 0]⟧
pos₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0]⟧ ⟦![1, 1, 0]⟧
pos₂ pos₃ : Eq.{u + 1} (α := PointClass F) ⟦![1, 1, 0]⟧ ⟦![1, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![1, 1, 0]⟧

Tactic:
rw [addMap_eq, add_of_Y_eq hPz hQz hx hy hy',
      smul_eq _ <| isUnit_dblU_of_Y_eq hP hPz hQz hx hy hy']

Premises used: WeierstrassCurve.Jacobian.add_of_Y_eq, WeierstrassCurve.Jacobian.smul_eq, WeierstrassCurve.Jacobian.addMap_eq, WeierstrassCurve.Jacobian.isUnit_dblU_of_Y_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3
hy : ¬P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
neg : Eq (α := PointClass F) ⟦W.add P Q⟧ ⟦![1, 1, 0]⟧
neg₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0]⟧ ⟦![1, 1, 0]⟧
neg₂ neg₃ : Eq.{u + 1} (α := PointClass F) ⟦![1, 1, 0]⟧ ⟦![1, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧) ⟦![1, 1, 0]⟧

Tactic:
rw [addMap_eq, add_of_Y_ne hP.left hQ hPz hQz hx hy,
      smul_eq _ <| isUnit_addU_of_Y_ne hPz hQz hy]

Premises used: And.left, WeierstrassCurve.Jacobian.smul_eq, WeierstrassCurve.Jacobian.addMap_eq, WeierstrassCurve.Jacobian.add_of_Y_ne, WeierstrassCurve.Jacobian.isUnit_addU_of_Y_ne
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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 * 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)
pos :
  ∀ (hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2),
    Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧)
      ⟦![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]⟧
neg :
  ∀ (hx : ¬P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2),
    Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧)
      ⟦![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]⟧
⊢ Eq (α := PointClass F) (W.addMap ⟦P⟧ ⟦Q⟧)
    ⟦![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]⟧

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

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.NonsingularLift, WeierstrassCurve.Jacobian.nonsingular_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.nonsingular_add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian 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.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : Nontrivial R
⊢ Eq.{r + 1} (α := W'.Point) 0 { point := ⟦![1, 1, 0]⟧, nonsingular := ⋯ }

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl, WeierstrassCurve.Jacobian.Point.fromAffine
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian 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: rfl, WeierstrassCurve.Jacobian.Point.fromAffine
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian 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.Jacobian.nonsingularLift_some, WeierstrassCurve.Jacobian.Point.mk_ne_zero, WeierstrassCurve.Jacobian.Point.fromAffine
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : W.Point
⊢ -P = P.neg

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: WeierstrassCurve.Jacobian.addMap, Quotient.map₂, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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
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, WeierstrassCurve.Jacobian.Point.toAffine, dif_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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
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, WeierstrassCurve.Jacobian.Point.toAffine, dif_neg, not_and_not_right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
⊢ Eq (α := W.toAffine.Point) (toAffine W ![1, 1, 0]) 0

Tactic:
toAffine_of_Z_eq_zero rfl

Premises used: WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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) ⋯
rw₁ rw₂ :
  Affine.Point.some (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) ⋯
⊢ toAffine W P = Affine.Point.some (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯

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

Premises used: dif_pos, WeierstrassCurve.Jacobian.Point.toAffine
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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, one_pow, div_one]

Premises used: one_pow, WeierstrassCurve.Jacobian.Point.toAffine_of_Z_ne_zero, WeierstrassCurve.Jacobian.fin3_def_ext, one_ne_zero, div_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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)
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.Jacobian.Nonsingular
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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)
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.Jacobian.Point
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)
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: WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero, mul_eq_zero_of_right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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
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
⊢ 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.Jacobian.Point.toAffine_of_Z_ne_zero, WeierstrassCurve.Jacobian.nonsingular_smul, WeierstrassCurve.Affine.Point.some.injEq, IsUnit.ne_zero, mul_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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
⊢ (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:
simp only [smul_fin3_ext, mul_pow, mul_div_mul_left _ _ (hu.pow _).ne_zero, and_self]

Premises used: and_self, IsUnit.pow, mul_div_mul_left, WeierstrassCurve.Jacobian.smul_fin3_ext, IsUnit.ne_zero, mul_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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)
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.Jacobian.nonsingular_smul, Iff.mp, WeierstrassCurve.Jacobian.Point.toAffine_of_singular
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.Point.toAffine_smul, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.Point.toAffine_smul, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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)
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.Jacobian.Point
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)
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 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]

Premises used: WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero, WeierstrassCurve.Affine.Point.neg_zero, WeierstrassCurve.Jacobian.Point.toAffine_smul, WeierstrassCurve.Jacobian.isUnit_Y_of_Z_eq_zero, WeierstrassCurve.Jacobian.Point.toAffine_zero, IsUnit.div, IsUnit.neg, WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero, WeierstrassCurve.Jacobian.neg_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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) ⋯
neg₄ 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)
      (W.toAffine.negY (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)

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.Jacobian.Point.toAffine_of_Z_ne_zero, Ne.isUnit, WeierstrassCurve.Affine.Point.neg_some, WeierstrassCurve.Jacobian.nonsingular_smul, WeierstrassCurve.Jacobian.Point.toAffine_some, WeierstrassCurve.Jacobian.Point.toAffine_smul, Iff.mp, WeierstrassCurve.Jacobian.neg_of_Z_ne_zero