awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negDblY P)
rw₁ :
  (W'⁄B).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₂ rw₃ : (W'⁄B).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).negDblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).negDblY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).negDblY P)

Tactic:
rw [← RingHom.coe_coe, ← map_negDblY, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Projective.map_negDblY, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblY P)
rw₁ :
  (W'⁄B).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₂ rw₃ : (W'⁄B).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).dblY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).dblY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblY P)

Tactic:
rw [← RingHom.coe_coe, ← map_dblY, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Projective.map_dblY, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
rw : (W'⁄B).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).dblXYZ P
rw₁ :
  (W'⁄B).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₂ rw₃ : (W'⁄B).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).dblXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).dblXYZ ((⇑f : (a : A) → B) ∘ P) = (⇑f : (a : A) → B) ∘ (W'⁄A).dblXYZ P

Tactic:
rw [← RingHom.coe_coe, ← map_dblXYZ, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Projective.map_dblXYZ, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addX P Q)
rw₁ :
  (W'⁄B).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((W'⁄A).map (↑f : A →+* B)).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
rw₂ rw₃ :
  (W'⁄B).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    (W'⁄B).addX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
⊢ (W'⁄B).addX ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).addX P Q)

Tactic:
rw [← RingHom.coe_coe, ← map_addX, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Projective.map_addX, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negAddY P Q)
rw₁ :
  (W'⁄B).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((W'⁄A).map (↑f : A →+* B)).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
rw₂ rw₃ :
  (W'⁄B).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    (W'⁄B).negAddY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
⊢ (W'⁄B).negAddY ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).negAddY P Q)

Tactic:
rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]

Premises used: WeierstrassCurve.Projective.map_negAddY, RingHom.coe_coe, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addY P Q)
rw₁ :
  (W'⁄B).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((W'⁄A).map (↑f : A →+* B)).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
rw₂ rw₃ :
  (W'⁄B).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    (W'⁄B).addY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
⊢ (W'⁄B).addY ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (f : (a : A) → B) ((W'⁄A).addY P Q)

Tactic:
rw [← RingHom.coe_coe, ← map_addY, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Projective.map_addY, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
rw :
  (W'⁄B).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).addXYZ P Q
rw₁ :
  (W'⁄B).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    ((W'⁄A).map (↑f : A →+* B)).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
rw₂ rw₃ :
  (W'⁄B).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q) =
    (W'⁄B).addXYZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ((⇑(↑f : A →+* B) : (a : A) → B) ∘ Q)
⊢ (W'⁄B).addXYZ ((⇑f : (a : A) → B) ∘ P) ((⇑f : (a : A) → B) ∘ Q) = (⇑f : (a : A) → B) ∘ (W'⁄A).addXYZ P Q

Tactic:
rw [← RingHom.coe_coe, ← map_addXYZ, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Projective.map_addXYZ, WeierstrassCurve.Projective.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.neg P x = P x

Tactic:
rfl

Premises used: Eq.mpr, WeierstrassCurve.Projective.neg, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.neg P y = W'.negY P

Tactic:
rfl

Premises used: WeierstrassCurve.Projective.negY, Eq.mpr, WeierstrassCurve.Projective.neg, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.neg P z = P z

Tactic:
rfl

Premises used: Eq.mpr, WeierstrassCurve.Projective.neg, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
⊢ W'.neg (u • P) = u • W'.neg P

Tactic:
simpa only [neg, negY_smul] using (smul_fin3 (W'.neg P) u).symm

Premises used: WeierstrassCurve.Projective.neg, WeierstrassCurve.Projective.negY_smul, WeierstrassCurve.Projective.smul_fin3, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
u : R
hu : IsUnit u
⊢ W'.neg (u • P) ≈ W'.neg P

Tactic:
⟨hu.unit, (W'.neg_smul ..).symm⟩

Premises used: Set.Mem, setOf, MulAction.orbit, Exists.intro, IsUnit.unit, WeierstrassCurve.Projective.neg_smul, Set.range, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
h : P ≈ Q
rcases : ∀ (u : Rˣ), W'.neg ((fun (m : Rˣ) ↦ m • Q) u) ≈ W'.neg Q
⊢ W'.neg P ≈ W'.neg Q

Tactic:
rcases h with ⟨u, rfl⟩

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

Tactic:
neg_smul_equiv Q u.isUnit

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

Tactic:
exact neg_smul_equiv Q u.isUnit

Premises used: Units.isUnit, WeierstrassCurve.Projective.neg_smul_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → R) (-P y) ![0, 1, 0]

Tactic:
simp [neg, X_eq_zero_of_Z_eq_zero hP hPz, negY_of_Z_eq_zero hP hPz, hPz]

Premises used: WeierstrassCurve.Projective.negY_of_Z_eq_zero, WeierstrassCurve.Projective.neg, WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
erw : ![P x, W.negY P, P z] = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]
erw₁ :
  ![P x, W.negY P, P z] =
    ![P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] x,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
erw₂ :
  ![P x, W.negY P, P z] =
    ![P x, P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] y,
      P z * ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] z]
erw₃ : ![P x, W.negY P, P z] = ![P x, P z * ![P x / P z, W.negY P / P z, 1] y, P z * ![P x / P z, W.negY P / P z, 1] z]
erw₄ : ![P x, W.negY P, P z] = ![P x, W.negY P, P z * ![P x / P z, W.negY P / P z, 1] z]
erw₅ erw₆ : ![P x, W.negY P, P z] = ![P x, W.negY P, P z]
⊢ W.neg P = P z • ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]

Tactic:
erw [neg, smul_fin3, mul_div_cancel₀ _ hPz, ← negY_of_Z_ne_zero hPz, mul_div_cancel₀ _ hPz,
    mul_one]

Premises used: WeierstrassCurve.Projective.neg, WeierstrassCurve.Projective.negY_of_Z_ne_zero, mul_div_cancel₀, WeierstrassCurve.Projective.smul_fin3, mul_one
-- 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
⊢ W.Nonsingular ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1]

Tactic:
(nonsingular_some ..).mpr <| (Affine.nonsingular_neg ..).mpr <|
    (nonsingular_of_Z_ne_zero hPz).mp hP

Premises used: Iff.mpr, WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero, Iff.mp, WeierstrassCurve.Projective.nonsingular_some, WeierstrassCurve.Affine.nonsingular_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
F : Type u
inst : Field F
W : Projective F
P : Fin 3 → F
hP : W.Nonsingular P
pos : ∀ (hPz : P z = 0), W.Nonsingular (W.neg P)
neg : ∀ (hPz : ¬P z = 0), W.Nonsingular (W.neg P)
⊢ W.Nonsingular (W.neg P)

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 : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ W.Nonsingular (W.neg P)

Tactic:
simp only [neg_of_Z_eq_zero hP.left hPz, nonsingular_smul _ (isUnit_Y_of_Z_eq_zero hP hPz).neg,
      nonsingular_zero]

Premises used: WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero, And.left, WeierstrassCurve.Projective.neg_of_Z_eq_zero, WeierstrassCurve.Projective.nonsingular_zero, IsUnit.neg, WeierstrassCurve.Projective.nonsingular_smul
-- 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
⊢ W.Nonsingular (W.neg P)

Tactic:
simp only [neg_of_Z_ne_zero hPz, nonsingular_smul _ <| Ne.isUnit hPz,
      nonsingular_neg_of_Z_ne_zero hP hPz]

Premises used: _private.0.WeierstrassCurve.Projective.nonsingular_neg_of_Z_ne_zero, Ne.isUnit, WeierstrassCurve.Projective.neg_of_Z_ne_zero, WeierstrassCurve.Projective.nonsingular_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
rw :
  -3 * HPow.hPow (β := ℕ) (P x) 2 * P x * P z + 3 * P x * HPow.hPow (β := ℕ) (P x) 2 * P z +
                        HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                      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 -
                  W'.a₁ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * HPow.hPow (β := ℕ) (P z) 2 -
                W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (P z) 2 -
          W'.a₃ * (-P y - W'.a₁ * P x - W'.a₃ * P z) * HPow.hPow (β := ℕ) (P z) 2 * P z -
        W'.a₄ * P x * P z * HPow.hPow (β := ℕ) (P z) 2 +
      W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * P z =
    0
⊢ W'.addZ P (W'.neg P) = 0

Tactic:
rw [addZ, neg_X, neg_Y, neg_Z, negY]

Premises used: WeierstrassCurve.Projective.negY, WeierstrassCurve.Projective.neg_Y, WeierstrassCurve.Projective.neg_X, WeierstrassCurve.Projective.addZ, WeierstrassCurve.Projective.neg_Z
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * HPow.hPow (β := ℕ) (P x) 2 * P x * P z + 3 * P x * HPow.hPow (β := ℕ) (P x) 2 * P z +
                        HPow.hPow (β := ℕ) (P y) 2 * HPow.hPow (β := ℕ) (P z) 2 -
                      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 -
                  W'.a₁ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * HPow.hPow (β := ℕ) (P z) 2 -
                W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
              W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
            W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (P z) 2 -
          W'.a₃ * (-P y - W'.a₁ * P x - W'.a₃ * P z) * HPow.hPow (β := ℕ) (P z) 2 * P z -
        W'.a₄ * P x * P z * HPow.hPow (β := ℕ) (P z) 2 +
      W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * P z =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
rw :
  -P x * HPow.hPow (β := ℕ) (-P y - W'.a₁ * P x - W'.a₃ * P z) 2 * P z + P x * HPow.hPow (β := ℕ) (P y) 2 * P z -
                                2 * P x * P y * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                              2 * P x * P y * (-P y - W'.a₁ * P x - W'.a₃ * P z) * 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 +
                        W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P x * P z -
                      W'.a₂ * P x * HPow.hPow (β := ℕ) (P x) 2 * P z -
                    W'.a₃ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 +
                  W'.a₃ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * 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₄ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
          W'.a₄ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
        3 * W'.a₆ * P x * P z * HPow.hPow (β := ℕ) (P z) 2 -
      3 * W'.a₆ * P x * HPow.hPow (β := ℕ) (P z) 2 * P z =
    0
⊢ W'.addX P (W'.neg P) = 0

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

Premises used: WeierstrassCurve.Projective.negY, WeierstrassCurve.Projective.neg_Y, WeierstrassCurve.Projective.neg_X, WeierstrassCurve.Projective.addX, WeierstrassCurve.Projective.neg_Z
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * HPow.hPow (β := ℕ) (-P y - W'.a₁ * P x - W'.a₃ * P z) 2 * P z + P x * HPow.hPow (β := ℕ) (P y) 2 * P z -
                                2 * P x * P y * (-P y - W'.a₁ * P x - W'.a₃ * P z) * P z +
                              2 * P x * P y * (-P y - W'.a₁ * P x - W'.a₃ * P z) * 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 +
                        W'.a₂ * HPow.hPow (β := ℕ) (P x) 2 * P x * P z -
                      W'.a₂ * P x * HPow.hPow (β := ℕ) (P x) 2 * P z -
                    W'.a₃ * P x * P y * HPow.hPow (β := ℕ) (P z) 2 +
                  W'.a₃ * P x * (-P y - W'.a₁ * P x - W'.a₃ * P z) * 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₄ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 -
          W'.a₄ * HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (P z) 2 +
        3 * W'.a₆ * P x * P z * HPow.hPow (β := ℕ) (P z) 2 -
      3 * W'.a₆ * P x * HPow.hPow (β := ℕ) (P z) 2 * P z =
    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 :
  -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
⊢ 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

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

Premises used: WeierstrassCurve.Projective.negY, WeierstrassCurve.Projective.neg_Y, WeierstrassCurve.Projective.neg_X, WeierstrassCurve.Projective.neg_Z, WeierstrassCurve.Projective.dblZ, WeierstrassCurve.Projective.negAddY