awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
a :
  P x * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                            2 * P y * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) * P z * P z +
                          HPow.hPow (β := ℕ) (P x) 2 * P x * HPow.hPow (β := ℕ) (P z) 2 -
                        W'.a₁ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) *
                            HPow.hPow (β := ℕ) (P z) 2 *
                          P z -
                      W'.a₁ * P y * P x * P z * HPow.hPow (β := ℕ) (P z) 2 +
                    2 * W'.a₂ * P x * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                  W'.a₃ * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) * HPow.hPow (β := ℕ) (P z) 4 *
                    P z -
                W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (P z) 4 +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P z) 4 +
          2 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (P z) 4 +
        -2 * HPow.hPow (β := ℕ) (P z) 2 * 0 -
      (HPow.hPow (β := ℕ) (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3))) 2 +
        -2 * HPow.hPow (β := ℕ) (P z) 2 *
          (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 6))) =
    0
⊢ W'.addX P (W'.neg P) + -2 * HPow.hPow (β := ℕ) (P z) 2 * 0 -
      (HPow.hPow (β := ℕ) (W'.dblZ P) 2 +
        -2 * HPow.hPow (β := ℕ) (P z) 2 *
          (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 6))) =
    0

Tactic:
rw [addX, neg_X, neg_Y, neg_Z, dblZ, negY]

Premises used: WeierstrassCurve.Jacobian.negY, WeierstrassCurve.Jacobian.dblZ, WeierstrassCurve.Jacobian.neg_X, WeierstrassCurve.Jacobian.neg_Z, WeierstrassCurve.Jacobian.neg_Y, WeierstrassCurve.Jacobian.addX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                            2 * P y * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) * P z * P z +
                          HPow.hPow (β := ℕ) (P x) 2 * P x * HPow.hPow (β := ℕ) (P z) 2 -
                        W'.a₁ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) *
                            HPow.hPow (β := ℕ) (P z) 2 *
                          P z -
                      W'.a₁ * P y * P x * P z * HPow.hPow (β := ℕ) (P z) 2 +
                    2 * W'.a₂ * P x * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                  W'.a₃ * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3) * HPow.hPow (β := ℕ) (P z) 4 *
                    P z -
                W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (P z) 4 +
              W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P z) 4 +
          2 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (P z) 4 +
        -2 * HPow.hPow (β := ℕ) (P z) 2 * 0 -
      (HPow.hPow (β := ℕ) (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3))) 2 +
        -2 * HPow.hPow (β := ℕ) (P z) 2 *
          (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 6))) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
a :
  W'.addX P (W'.neg P) + -2 * HPow.hPow (β := ℕ) (P z) 2 * 0 -
      (HPow.hPow (β := ℕ) (W'.dblZ P) 2 +
        -2 * HPow.hPow (β := ℕ) (P z) 2 *
          (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 6))) =
    0
⊢ W'.addX P (W'.neg P) = HPow.hPow (β := ℕ) (W'.dblZ P) 2

Tactic:
linear_combination (norm := (rw [addX, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1))
    -2 * P z ^ 2 * (equation_iff _).mp hP

Premises used: WeierstrassCurve.Jacobian.negY, WeierstrassCurve.Jacobian.dblZ, WeierstrassCurve.Jacobian.neg_X, WeierstrassCurve.Jacobian.neg_Z, WeierstrassCurve.Jacobian.equation_iff, WeierstrassCurve.Jacobian.neg_Y, Iff.mp, OfNat.ofNat, WeierstrassCurve.Jacobian.addX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
a :
  W'.negAddY P (W'.neg P) + -2 * HPow.hPow (β := ℕ) (P z) 3 * (P y - W'.negY P) * 0 -
      (HPow.hPow (β := ℕ) (W'.dblZ P) 3 +
        -2 * HPow.hPow (β := ℕ) (P z) 3 * (P y - W'.negY P) *
          (HPow.hPow (β := ℕ) (P y) 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * HPow.hPow (β := ℕ) (P z) 3 -
            (HPow.hPow (β := ℕ) (P x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
                W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 4 +
              W'.a₆ * HPow.hPow (β := ℕ) (P z) 6))) =
    0
⊢ W'.negAddY P (W'.neg P) = HPow.hPow (β := ℕ) (W'.dblZ P) 3

Tactic:
linear_combination (norm := (rw [negAddY, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1))
    -2 * P z ^ 3 * (P y - W'.negY P) * (equation_iff _).mp hP

Premises used: WeierstrassCurve.Jacobian.negAddY, WeierstrassCurve.Jacobian.negY, HSub.hSub, WeierstrassCurve.Jacobian.dblZ, WeierstrassCurve.Jacobian.neg_X, WeierstrassCurve.Jacobian.neg_Z, WeierstrassCurve.Jacobian.equation_iff, WeierstrassCurve.Jacobian.neg_Y, Iff.mp, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
rw : -![HPow.hPow (β := ℕ) (W'.dblZ P) 2, HPow.hPow (β := ℕ) (W'.dblZ P) 3, 0] y = -HPow.hPow (β := ℕ) (W'.dblZ P) 3
⊢ W'.addY P (W'.neg P) = -HPow.hPow (β := ℕ) (W'.dblZ P) 3

Tactic:
rw [addY, addX_neg hP, negAddY_neg hP, addZ_neg, negY_of_Z_eq_zero rfl]

Premises used: WeierstrassCurve.Jacobian.addY, WeierstrassCurve.Jacobian.negAddY_neg, WeierstrassCurve.Jacobian.addZ_neg, WeierstrassCurve.Jacobian.addX_neg, WeierstrassCurve.Jacobian.negY_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -![HPow.hPow (β := ℕ) (W'.dblZ P) 2, HPow.hPow (β := ℕ) (W'.dblZ P) 3, 0] y = -HPow.hPow (β := ℕ) (W'.dblZ P) 3

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
rw :
  ![HPow.hPow (β := ℕ) (W'.dblZ P) 2, -HPow.hPow (β := ℕ) (W'.dblZ P) 3, 0] =
    ![HPow.hPow (β := ℕ) (-W'.dblZ P) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-W'.dblZ P) 3 * ![1, 1, 0] y,
      -W'.dblZ P * ![1, 1, 0] z]
⊢ W'.addXYZ P (W'.neg P) = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![1, 1, 0]

Tactic:
rw [addXYZ, addX_neg hP, addY_neg hP, addZ_neg, smul_fin3]

Premises used: WeierstrassCurve.Jacobian.addY_neg, WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.addZ_neg, WeierstrassCurve.Jacobian.addXYZ, WeierstrassCurve.Jacobian.addX_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![HPow.hPow (β := ℕ) (W'.dblZ P) 2, -HPow.hPow (β := ℕ) (W'.dblZ P) 3, 0] =
    ![HPow.hPow (β := ℕ) (-W'.dblZ P) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-W'.dblZ P) 3 * ![1, 1, 0] y,
      -W'.dblZ P * ![1, 1, 0] z]

Tactic:
simp +decide [fin3_def_ext, Odd.neg_pow]

Premises used: Odd.neg_pow, WeierstrassCurve.Jacobian.fin3_def_ext, Decidable.decide
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ Eq (α := PointClass R) (W'.negMap ⟦P⟧) ⟦W'.neg P⟧

Tactic:
rfl

Premises used: Quotient.map, WeierstrassCurve.Jacobian.negMap, 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 : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![1, 1, 0]⟧
rw₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]⟧ ⟦![1, 1, 0]⟧
rw₂ rw₃ : Eq.{u + 1} (α := PointClass F) ⟦![1, 1, 0]⟧ ⟦![1, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![1, 1, 0]⟧

Tactic:
rw [negMap_eq, neg_of_Z_eq_zero hP hPz,
    smul_eq _ ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg]

Premises used: WeierstrassCurve.Jacobian.isUnit_Y_of_Z_eq_zero, IsUnit.div, IsUnit.neg, WeierstrassCurve.Jacobian.smul_eq, WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero, WeierstrassCurve.Jacobian.negMap_eq, 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
hPz : P z ≠ 0
rw :
  Eq (α := PointClass F) ⟦W.neg P⟧
    ⟦![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]⟧
rw₁ :
  Eq (α := PointClass F)
    ⟦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]⟧
    ⟦![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]⟧
rw₂ rw₃ :
  Eq (α := PointClass F)
    ⟦![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]⟧
    ⟦![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]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧)
    ⟦![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]⟧

Tactic:
rw [negMap_eq, neg_of_Z_ne_zero hPz, smul_eq _ <| Ne.isUnit hPz]

Premises used: Ne.isUnit, WeierstrassCurve.Jacobian.smul_eq, WeierstrassCurve.Jacobian.neg_of_Z_ne_zero, WeierstrassCurve.Jacobian.negMap_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : PointClass F
hP : W.NonsingularLift P
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.negMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a))
⊢ W.NonsingularLift (W.negMap P)

Tactic:
rcases P with ⟨_⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : 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)
⊢ W.NonsingularLift (W.negMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a))

Tactic:
nonsingular_neg hP

Premises used: WeierstrassCurve.Jacobian.NonsingularLift, WeierstrassCurve.Jacobian.nonsingular_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : 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)
⊢ W.NonsingularLift (W.negMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F)) : (Fin 3 → F) → (Fin 3 → F) → Prop) a))

Tactic:
exact nonsingular_neg hP

Premises used: WeierstrassCurve.Jacobian.nonsingular_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.add P Q = W'.dblXYZ P

Tactic:
if_pos h

Premises used: WeierstrassCurve.Jacobian.add, if_pos
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
rw : W'.dblXYZ (u • P) = HPow.hPow (β := ℕ) u 4 • W'.add P Q
rw₁ : HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P = HPow.hPow (β := ℕ) u 4 • W'.add P Q
rw₂ rw₃ : HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P = HPow.hPow (β := ℕ) u 4 • W'.dblXYZ P
⊢ W'.add (u • P) (v • Q) = HPow.hPow (β := ℕ) u 4 • W'.add P Q

Tactic:
rw [add_of_equiv <| (smul_equiv_smul P Q hu hv).mpr h, dblXYZ_smul, add_of_equiv h]

Premises used: Iff.mpr, WeierstrassCurve.Jacobian.add_of_equiv, WeierstrassCurve.Jacobian.dblXYZ_smul, WeierstrassCurve.Jacobian.smul_equiv_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.add P P = W'.dblXYZ P

Tactic:
add_of_equiv <| Setoid.refl _

Premises used: WeierstrassCurve.Jacobian.add_of_equiv, Setoid.refl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : P = Q
⊢ W'.add P Q = W'.dblXYZ P

Tactic:
h ▸ add_self P

Premises used: Eq.rec, WeierstrassCurve.Jacobian.add_self
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : ¬P ≈ Q
⊢ W'.add P Q = W'.addXYZ P Q

Tactic:
if_neg h

Premises used: WeierstrassCurve.Jacobian.add, if_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
h : ¬P ≈ Q
u v : R
hu : IsUnit u
hv : IsUnit v
rw : W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q
rw₁ : HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q = HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q
rw₂ rw₃ : HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
⊢ W'.add (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q

Tactic:
rw [add_of_not_equiv <| h.comp (smul_equiv_smul P Q hu hv).mp, addXYZ_smul, add_of_not_equiv h]

Premises used: Function.comp, WeierstrassCurve.Jacobian.addXYZ_smul, Iff.mp, WeierstrassCurve.Jacobian.add_of_not_equiv, WeierstrassCurve.Jacobian.smul_equiv_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
pos : ∀ (h : P ≈ Q), W'.add (u • P) (v • Q) ≈ W'.add P Q
neg : ∀ (h : ¬P ≈ Q), W'.add (u • P) (v • Q) ≈ W'.add P Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
by_cases h : P ≈ Q
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ HPow.hPow (β := ℕ) u 4 • W'.add P Q = W'.add (u • P) (v • Q)

Tactic:
(add_smul_of_equiv h hu hv).symm

Premises used: Eq.symm, WeierstrassCurve.Jacobian.add_smul_of_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ (fun (m : Rˣ) ↦ m • W'.add P Q) (HPow.hPow (β := ℕ) hu.unit 4) = W'.add (u • P) (v • Q)

Tactic:
convert! (add_smul_of_equiv h hu hv).symm

Premises used: Eq.symm, WeierstrassCurve.Jacobian.add_smul_of_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
exact ⟨hu.unit ^ 4, by convert! (add_smul_of_equiv h hu hv).symm⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ HPow.hPow (β := ℕ) (u * v) 2 • W'.add P Q = W'.add (u • P) (v • Q)

Tactic:
(add_smul_of_not_equiv h hu hv).symm

Premises used: WeierstrassCurve.Jacobian.add_smul_of_not_equiv, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ (fun (m : Rˣ) ↦ m • W'.add P Q) (HPow.hPow (β := ℕ) (hu.unit * hv.unit) 2) = W'.add (u • P) (v • Q)

Tactic:
convert! (add_smul_of_not_equiv h hu hv).symm

Premises used: WeierstrassCurve.Jacobian.add_smul_of_not_equiv, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
exact ⟨(hu.unit * hv.unit) ^ 2, by convert! (add_smul_of_not_equiv h hu hv).symm⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P P' Q Q' : Fin 3 → R
hP : P ≈ P'
hQ : Q ≈ Q'
rcases : ∀ (u v : Rˣ), W'.add ((fun (m : Rˣ) ↦ m • P') u) ((fun (m : Rˣ) ↦ m • Q') v) ≈ W'.add P' Q'
⊢ W'.add P Q ≈ W'.add P' Q'

Tactic:
rcases hP, hQ with ⟨⟨u, rfl⟩, ⟨v, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P' Q' : Fin 3 → R
u v : Rˣ
⊢ W'.add ((fun (m : Rˣ) ↦ m • P') u) ((fun (m : Rˣ) ↦ m • Q') v) ≈ W'.add P' Q'

Tactic:
add_smul_equiv P' Q' u.isUnit v.isUnit

Premises used: Set.Mem, WeierstrassCurve.Jacobian.add_smul_equiv, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P' Q' : Fin 3 → R
u v : Rˣ
⊢ W'.add ((fun (m : Rˣ) ↦ m • P') u) ((fun (m : Rˣ) ↦ m • Q') v) ≈ W'.add P' Q'

Tactic:
exact add_smul_equiv P' Q' u.isUnit v.isUnit

Premises used: WeierstrassCurve.Jacobian.add_smul_equiv, Units.isUnit
-- 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.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
rw : W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0]
rw₁ rw₂ :
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P x) 2) ![1, 1, 0]

Tactic:
rw [add_of_equiv <| equiv_of_Z_eq_zero hP hQ hPz hQz, dblXYZ_of_Z_eq_zero hP.left hPz]

Premises used: And.left, WeierstrassCurve.Jacobian.add_of_equiv, WeierstrassCurve.Jacobian.dblXYZ_of_Z_eq_zero, WeierstrassCurve.Jacobian.equiv_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
hQz : Q z ≠ 0
rw : W'.addXYZ P Q = (P x * Q z) • Q
rw₁ rw₂ : (P x * Q z) • Q = (P x * Q z) • Q
⊢ W'.add P Q = (P x * Q z) • Q

Tactic:
rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_left hPz hQz, addXYZ_of_Z_eq_zero_left hP hPz]

Premises used: WeierstrassCurve.Jacobian.add_of_not_equiv, WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_left, WeierstrassCurve.Jacobian.addXYZ_of_Z_eq_zero_left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z = 0
rw : W'.addXYZ P Q = -(Q x * P z) • P
rw₁ rw₂ : -(Q x * P z) • P = -(Q x * P z) • P
⊢ W'.add P Q = -(Q x * P z) • P

Tactic:
rw [add_of_not_equiv <| not_equiv_of_Z_eq_zero_right hPz hQz, addXYZ_of_Z_eq_zero_right hQ hQz]

Premises used: WeierstrassCurve.Jacobian.addXYZ_of_Z_eq_zero_right, WeierstrassCurve.Jacobian.add_of_not_equiv, WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
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 = Q y * HPow.hPow (β := ℕ) (P z) 3
hy' : P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3
rw : W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0]
rw₁ rw₂ :
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![1, 1, 0]

Tactic:
rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx hy, dblXYZ_of_Y_eq hQz hx hy hy']

Premises used: WeierstrassCurve.Jacobian.add_of_equiv, WeierstrassCurve.Jacobian.equiv_of_X_eq_of_Y_eq, WeierstrassCurve.Jacobian.dblXYZ_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.Equation 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 ≠ Q y * HPow.hPow (β := ℕ) (P z) 3
rw : W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0]
rw₁ rw₂ :
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0]

Tactic:
rw [add_of_not_equiv <| not_equiv_of_Y_ne hy, addXYZ_of_X_eq hP hQ hPz hQz hx]

Premises used: WeierstrassCurve.Jacobian.addXYZ_of_X_eq, WeierstrassCurve.Jacobian.not_equiv_of_Y_ne, WeierstrassCurve.Jacobian.add_of_not_equiv