awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.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.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
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: WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero, zero_add
-- 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.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.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
pos :
  Eq (α := W.toAffine.Point)
    (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0]))
    (toAffine W Q)
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![1, 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_X_of_Z_eq_zero hP hPz).pow 2,
        toAffine_zero, toAffine_of_Z_eq_zero hQz]

Premises used: WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero, IsUnit.pow, WeierstrassCurve.Jacobian.Point.toAffine_smul, WeierstrassCurve.Jacobian.Point.toAffine_zero, OfNat.ofNat, WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero, WeierstrassCurve.Jacobian.add_of_Z_eq_zero
-- 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.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : ¬Q z = 0
neg : Eq (α := W.toAffine.Point) (toAffine W ((P x * 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_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]

Premises used: Ne.isUnit, IsUnit.mul, WeierstrassCurve.Jacobian.add_of_Z_eq_zero_left, And.left, WeierstrassCurve.Jacobian.Point.toAffine_smul, WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero
-- 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.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.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : Q z = 0
pos : toAffine W (-(Q x * 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_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg,
        toAffine_of_Z_eq_zero hQz, add_zero]

Premises used: WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero, Ne.isUnit, IsUnit.mul, And.left, WeierstrassCurve.Jacobian.Point.toAffine_smul, IsUnit.neg, add_zero, 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
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 * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
        P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3),
    toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
neg :
  ∀
    (hxy :
      ¬(P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
          P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3)),
    toAffine W (W.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 ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3

Premises used: WeierstrassCurve.Jacobian.negY, OfNat.ofNat
-- 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.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy :
  P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
    P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3
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.Jacobian.Point.toAffine_of_Z_ne_zero, WeierstrassCurve.Jacobian.X_eq_iff, WeierstrassCurve.Affine.Point.add_of_Y_eq, And.right, And.left, WeierstrassCurve.Jacobian.Y_eq_iff', Iff.mp
-- 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.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy :
  P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
    P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3
pos :
  ∀ (hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3),
    Eq (α := W.toAffine.Point) (toAffine W (W.add P Q)) 0
neg :
  ∀ (hy : ¬P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3),
    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 ^ 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
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy :
  P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
    P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
pos :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0])) 0
pos₁ : Eq (α := W.toAffine.Point) (toAffine W ![1, 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 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.Jacobian.add_of_Y_eq, And.right, And.left, WeierstrassCurve.Jacobian.Point.toAffine_smul, WeierstrassCurve.Jacobian.Point.toAffine_zero, WeierstrassCurve.Jacobian.isUnit_dblU_of_Y_eq
-- 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.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy :
  P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
    P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3
hy : ¬P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3
neg :
  Eq (α := W.toAffine.Point) (toAffine W (HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0])) 0
neg₁ : Eq (α := W.toAffine.Point) (toAffine W ![1, 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: And.left, WeierstrassCurve.Jacobian.Point.toAffine_smul, WeierstrassCurve.Jacobian.Point.toAffine_zero, 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.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy :
  ¬(P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
      P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3)
⊢ toAffine W
      ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        1] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)

Tactic:
have := toAffine_add_of_Z_ne_zero hP hQ hPz hQz hxy
-- 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.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy :
  ¬(P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
      P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3)
this :
  toAffine W
      ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        1] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
pos :
  ∀ (hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2),
    toAffine W (W.add P Q) = HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
neg :
  ∀ (hx : ¬P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2),
    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 ^ 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
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy :
  ¬(P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
      P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3)
this :
  toAffine W
      ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        1] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
pos :
  toAffine W
      (W.dblZ P •
        ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
              (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
          W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3)
            (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
              (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
          1]) =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
pos₁ pos₂ pos₃ pos₄ :
  toAffine W
      ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        1] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
⊢ 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 hx <| not_and.mp hxy hx]

Premises used: WeierstrassCurve.Jacobian.add_of_Y_ne', And.left, WeierstrassCurve.Jacobian.isUnit_dblZ_of_Y_ne', WeierstrassCurve.Jacobian.Point.toAffine_smul, Iff.mp, not_and
-- 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.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy :
  ¬(P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2 ∧
      P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3)
this :
  toAffine W
      ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        1] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
hx : ¬P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
neg :
  toAffine W
      (addZ 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]) =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
neg₁ neg₂ neg₃ neg₄ :
  toAffine W
      ![W.toAffine.addX (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        W.toAffine.addY (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
          (P y / HPow.hPow (β := ℕ) (P z) 3)
          (W.toAffine.slope (P x / HPow.hPow (β := ℕ) (P z) 2) (Q x / HPow.hPow (β := ℕ) (Q z) 2)
            (P y / HPow.hPow (β := ℕ) (P z) 3) (Q y / HPow.hPow (β := ℕ) (Q z) 3)),
        1] =
    HAdd.hAdd (α := W.toAffine.Point) (toAffine W P) (toAffine W Q)
⊢ 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 hx]

Premises used: And.left, WeierstrassCurve.Jacobian.add_of_X_ne, WeierstrassCurve.Jacobian.Point.toAffine_smul, WeierstrassCurve.Jacobian.isUnit_addZ_of_X_ne
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.NonsingularLift ⟦P⟧
⊢ { point := ⟦P⟧, nonsingular := hP : W.Point }.toAffineLift = toAffine W P

Tactic:
rfl

Premises used: rfl, WeierstrassCurve.Jacobian.Point.toAffineLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.Point.toAffine_of_Z_eq_zero, WeierstrassCurve.Jacobian.Point.toAffineLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
⊢ Eq.{u + 1} (α := W.toAffine.Point) (toAffineLift 0) 0

Tactic:
toAffine_zero

Premises used: WeierstrassCurve.Jacobian.Point.toAffine_zero, WeierstrassCurve.Jacobian.Point.toAffineLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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 / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) ⋯

Tactic:
toAffine_of_Z_ne_zero hP hPz

Premises used: WeierstrassCurve.Jacobian.Point.toAffine_of_Z_ne_zero, WeierstrassCurve.Jacobian.Point.toAffineLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.Point.toAffine_some, WeierstrassCurve.Jacobian.Point.toAffineLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.Point.toAffine_neg, WeierstrassCurve.Jacobian.Point.toAffineLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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.Jacobian.Point.toAffine_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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⟩⟩