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

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

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

Premises used: WeierstrassCurve.Projective.negY, WeierstrassCurve.Projective.neg_Y, HSub.hSub, WeierstrassCurve.Projective.neg_X, Iff.mp, WeierstrassCurve.Projective.neg_Z, OfNat.ofNat, WeierstrassCurve.Projective.equation_iff, WeierstrassCurve.Projective.dblZ, WeierstrassCurve.Projective.negAddY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addY P (W'.neg P) = -W'.dblZ P

Tactic:
simp only [addY, addX_neg, negAddY_neg hP, addZ_neg, negY, fin3_def_ext, mul_zero, sub_zero]

Premises used: WeierstrassCurve.Projective.negY, sub_zero, WeierstrassCurve.Projective.addX_neg, WeierstrassCurve.Projective.negAddY_neg, MulZeroClass.mul_zero, WeierstrassCurve.Projective.fin3_def_ext, WeierstrassCurve.Projective.addZ_neg, WeierstrassCurve.Projective.addY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
hP : W'.Equation P
erw :
  ![W'.addX P (W'.neg P), W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₁ :
  ![0, W'.addY P (W'.neg P), W'.addZ P (W'.neg P)] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₂ :
  ![0, -W'.dblZ P, W'.addZ P (W'.neg P)] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₃ : ![0, -W'.dblZ P, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]
erw₄ : ![0, -W'.dblZ P, 0] = ![-W'.dblZ P * ![0, 1, 0] x, -W'.dblZ P * ![0, 1, 0] y, -W'.dblZ P * ![0, 1, 0] z]
erw₅ : ![0, -W'.dblZ P, 0] = ![0, -W'.dblZ P * ![0, 1, 0] y, 0]
erw₆ erw₇ : ![0, -W'.dblZ P, 0] = ![0, -W'.dblZ P, 0]
⊢ W'.addXYZ P (W'.neg P) = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-W'.dblZ P) ![0, 1, 0]

Tactic:
erw [addXYZ, addX_neg, addY_neg hP, addZ_neg, smul_fin3, mul_zero, mul_one]

Premises used: WeierstrassCurve.Projective.addY_neg, WeierstrassCurve.Projective.addX_neg, MulZeroClass.mul_zero, WeierstrassCurve.Projective.smul_fin3, WeierstrassCurve.Projective.addZ_neg, mul_one, WeierstrassCurve.Projective.addXYZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ Eq (α := PointClass R) (W'.negMap ⟦P⟧) ⟦W'.neg P⟧

Tactic:
rfl

Premises used: Quotient.map, WeierstrassCurve.Projective.negMap, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
rw : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![0, 1, 0]⟧
rw₁ : Eq (α := PointClass F) ⟦HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-P y) ![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
rw₂ rw₃ : Eq.{u + 1} (α := PointClass F) ⟦![0, 1, 0]⟧ ⟦![0, 1, 0]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![0, 1, 0]⟧

Tactic:
rw [negMap_eq, neg_of_Z_eq_zero hP.left hPz, smul_eq _ (isUnit_Y_of_Z_eq_zero hP hPz).neg]

Premises used: WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, WeierstrassCurve.Projective.smul_eq, WeierstrassCurve.Projective.negMap_eq, And.left, WeierstrassCurve.Projective.neg_of_Z_eq_zero, IsUnit.neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
rw : Eq (α := PointClass F) ⟦W.neg P⟧ ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
rw₁ :
  Eq (α := PointClass F) ⟦P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
    ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
rw₂ rw₃ :
  Eq (α := PointClass F) ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
    ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧
⊢ Eq (α := PointClass F) (W.negMap ⟦P⟧) ⟦![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]⟧

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

Premises used: Ne.isUnit, WeierstrassCurve.Projective.smul_eq, WeierstrassCurve.Projective.neg_of_Z_ne_zero, WeierstrassCurve.Projective.negMap_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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.Projective.nonsingular_neg, WeierstrassCurve.Projective.NonsingularLift
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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.Projective.nonsingular_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
⊢ W'.add P Q = W'.dblXYZ P

Tactic:
if_pos h

Premises used: if_pos, WeierstrassCurve.Projective.add
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.smul_equiv_smul, WeierstrassCurve.Projective.dblXYZ_smul, WeierstrassCurve.Projective.add_of_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.add P P = W'.dblXYZ P

Tactic:
add_of_equiv <| Setoid.refl _

Premises used: WeierstrassCurve.Projective.add_of_equiv, Setoid.refl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.add_self
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : ¬P ≈ Q
⊢ W'.add P Q = W'.addXYZ P Q

Tactic:
if_neg h

Premises used: WeierstrassCurve.Projective.add, if_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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: WeierstrassCurve.Projective.smul_equiv_smul, WeierstrassCurve.Projective.addXYZ_smul, Function.comp, Iff.mp, WeierstrassCurve.Projective.add_of_not_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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: WeierstrassCurve.Projective.add_smul_of_equiv, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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: WeierstrassCurve.Projective.add_smul_of_equiv, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.add_smul_of_not_equiv, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.add_smul_of_not_equiv, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.add_smul_equiv, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective 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.Projective.add_smul_equiv, Units.isUnit
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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 y) 4) ![0, 1, 0]
rw₁ rw₂ :
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P y) 4) ![0, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (HPow.hPow (β := ℕ) (P y) 4) ![0, 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: WeierstrassCurve.Projective.equiv_of_Z_eq_zero, WeierstrassCurve.Projective.dblXYZ_of_Z_eq_zero, WeierstrassCurve.Projective.add_of_equiv, And.left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
hQz : Q z ≠ 0
rw : W'.addXYZ P Q = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
rw₁ rw₂ : (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
⊢ W'.add P Q = (HPow.hPow (β := ℕ) (P y) 2 * 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.Projective.not_equiv_of_Z_eq_zero_left, WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_left, WeierstrassCurve.Projective.add_of_not_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z = 0
rw : W'.addXYZ P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
rw₁ rw₂ : -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P = -(HPow.hPow (β := ℕ) (Q y) 2 * P z) • P
⊢ W'.add P Q = -(HPow.hPow (β := ℕ) (Q y) 2 * 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.Projective.not_equiv_of_Z_eq_zero_right, WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_right, WeierstrassCurve.Projective.add_of_not_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z = Q y * P z
hy' : P y * Q z = W.negY Q * P z
rw : W.dblXYZ P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
rw₁ rw₂ :
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (W.dblU P) ![0, 1, 0]

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

Premises used: WeierstrassCurve.Projective.add_of_equiv, WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eq, WeierstrassCurve.Projective.dblXYZ_of_Y_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective 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 * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
rw : W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
rw₁ rw₂ :
  HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0] =
    HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
⊢ W.add P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 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.Projective.addXYZ_of_X_eq, WeierstrassCurve.Projective.add_of_not_equiv, WeierstrassCurve.Projective.not_equiv_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.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
rw :
  W.dblXYZ P =
    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]
rw₁ rw₂ :
  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] =
    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]
⊢ W.add P Q =
    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]

Tactic:
rw [add_of_equiv <| equiv_of_X_eq_of_Y_eq hPz hQz hx <| Y_eq_of_Y_ne' hP hQ hPz hQz hx hy,
    dblXYZ_of_Z_ne_zero hP hQ hPz hQz hx hy]

Premises used: WeierstrassCurve.Projective.Y_eq_of_Y_ne', WeierstrassCurve.Projective.add_of_equiv, WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero, WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
rw :
  W.addXYZ P Q =
    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]
rw₁ rw₂ :
  W.addZ P Q •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1] =
    W.addZ P Q •
      ![W.toAffine.addX (P x / P z) (Q x / Q z) (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        1]
⊢ W.add P Q =
    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]

Tactic:
rw [add_of_not_equiv <| not_equiv_of_X_ne hx, addXYZ_of_Z_ne_zero hP hQ hPz hQz hx]

Premises used: WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero, WeierstrassCurve.Projective.add_of_not_equiv, WeierstrassCurve.Projective.not_equiv_of_X_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)
rwa : ¬(P x * Q z = Q x * P z ∧ P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z))
rwa₁ rwa₂ rwa₃ rwa₄ : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ ¬(P x / P z = Q x / Q z ∧ P y / P z = W.toAffine.negY (Q x / Q z) (Q y / Q z))

Tactic:
rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]

Premises used: WeierstrassCurve.Projective.Y_eq_iff', WeierstrassCurve.Projective.X_eq_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
pos : ∀ (hPz : P z = 0), W.Nonsingular (W.add P Q)
neg : ∀ (hPz : ¬P z = 0), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P Q)

Tactic:
by_cases hPz : P z = 0

Premises used: OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
pos : ∀ (hQz : Q z = 0), W.Nonsingular (W.add P Q)
neg : ∀ (hQz : ¬Q z = 0), W.Nonsingular (W.add P Q)
⊢ W.Nonsingular (W.add P 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
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z = 0
hQz : Q z = 0
⊢ W.Nonsingular (W.add P Q)

Tactic:
simp only [add_of_Z_eq_zero hP hQ hPz hQz,
        nonsingular_smul _ <| (isUnit_Y_of_Z_eq_zero hP hPz).pow 4, nonsingular_zero]

Premises used: WeierstrassCurve.Projective.add_of_Z_eq_zero, WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, IsUnit.pow, WeierstrassCurve.Projective.nonsingular_zero, OfNat.ofNat, WeierstrassCurve.Projective.nonsingular_smul