awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.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' : Jacobian 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).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblZ P)
rw₁ :
  (W'⁄B).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₂ rw₃ : (W'⁄B).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).dblZ ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).dblZ ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblZ P)

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

Premises used: RingHom.coe_coe, WeierstrassCurve.Jacobian.map_dblZ, WeierstrassCurve.Jacobian.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.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' : Jacobian 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).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblX P)
rw₁ :
  (W'⁄B).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₂ rw₃ : (W'⁄B).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).dblX ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).dblX ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblX P)

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

Premises used: WeierstrassCurve.Jacobian.map_dblX, RingHom.coe_coe, WeierstrassCurve.Jacobian.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.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' : Jacobian 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: WeierstrassCurve.Jacobian.map_negDblY, RingHom.coe_coe, WeierstrassCurve.Jacobian.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.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' : Jacobian 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.Jacobian.map_baseChange, WeierstrassCurve.Jacobian.map_dblY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.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' : Jacobian 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.Jacobian.map_dblXYZ, WeierstrassCurve.Jacobian.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.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' : Jacobian 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: WeierstrassCurve.Jacobian.map_addX, RingHom.coe_coe, WeierstrassCurve.Jacobian.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.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' : Jacobian 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: RingHom.coe_coe, WeierstrassCurve.Jacobian.map_baseChange, WeierstrassCurve.Jacobian.map_negAddY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.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' : Jacobian 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.Jacobian.map_addY, WeierstrassCurve.Jacobian.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.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' : Jacobian 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.Jacobian.map_baseChange, WeierstrassCurve.Jacobian.map_addXYZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.neg P x = P x

Tactic:
rfl

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

Tactic:
rfl

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

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, WeierstrassCurve.Jacobian.neg, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
rw : ![(u • P) x, HPow.hPow (β := ℕ) u 3 * W'.negY P, (u • P) z] = u • W'.neg P
⊢ W'.neg (u • P) = u • W'.neg P

Tactic:
rw [neg, negY_smul]

Premises used: WeierstrassCurve.Jacobian.neg, WeierstrassCurve.Jacobian.negY_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ ![(u • P) x, HPow.hPow (β := ℕ) u 3 * W'.negY P, (u • P) z] = u • W'.neg P

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian 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, Set.range, Eq.symm, WeierstrassCurve.Jacobian.neg_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian 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.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian 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.Jacobian.neg_smul_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian 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.Jacobian.neg_smul_equiv
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : ![P x, W'.negY P, P z] = ![P x, -P y, 0]
rw₁ : ![P x, -P y, P z] = ![P x, -P y, 0]
rw₂ rw₃ : ![P x, -P y, 0] = ![P x, -P y, 0]
⊢ W'.neg P = ![P x, -P y, 0]

Tactic:
rw [neg, negY_of_Z_eq_zero hPz, hPz]

Premises used: WeierstrassCurve.Jacobian.neg, WeierstrassCurve.Jacobian.negY_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z = 0
⊢ ∀ {n : ℕ}, IsUnit (P x ^ n)

Tactic:
have hX {n : ℕ} : IsUnit <| P x ^ n := (isUnit_X_of_Z_eq_zero hP hPz).pow n
-- 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
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
⊢ Odd (α := ℕ) 3

Tactic:
decide
-- 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
hX : ∀ {n : ℕ}, IsUnit (P x ^ n)
erw : ![P x, -P y, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]
erw₁ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (-(P y / P x)) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₂ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y / P x) 2 * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y,
      -(P y / P x) * ![1, 1, 0] z]
erw₃ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P y) 2 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₄ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 3 / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₅ :
  ![P x, -P y, 0] =
    ![HPow.hPow (β := ℕ) (P x) 2 * P x / HPow.hPow (β := ℕ) (P x) 2 * ![1, 1, 0] x,
      HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₆ :
  ![P x, -P y, 0] =
    ![P x * ![1, 1, 0] x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₇ : ![P x, -P y, 0] = ![P x, HPow.hPow (β := ℕ) (-(P y / P x)) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₈ : ![P x, -P y, 0] = ![P x, -HPow.hPow (β := ℕ) (P y / P x) 3 * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₉ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P y) 3 / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₀ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P y) 2 * P y / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₁ :
  ![P x, -P y, 0] =
    ![P x, -(HPow.hPow (β := ℕ) (P x) 3 * P y / HPow.hPow (β := ℕ) (P x) 3) * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₂ : ![P x, -P y, 0] = ![P x, -P y * ![1, 1, 0] y, -(P y / P x) * ![1, 1, 0] z]
erw₁₃ : ![P x, -P y, 0] = ![P x, -P y, -(P y / P x) * ![1, 1, 0] z]
erw₁₄ erw₁₅ : ![P x, -P y, 0] = ![P x, -P y, 0]
⊢ W.neg P = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (-(P y / P x)) ![1, 1, 0]

Tactic:
erw [neg_of_Z_eq_zero' hPz, smul_fin3, neg_sq, div_pow, (equation_of_Z_eq_zero hPz).mp hP.left,
    pow_succ, hX.mul_div_cancel_left, mul_one, Odd.neg_pow <| by decide, div_pow, pow_succ,
    (equation_of_Z_eq_zero hPz).mp hP.left, hX.mul_div_cancel_left, mul_one, mul_zero]

Premises used: Odd.neg_pow, IsUnit.mul_div_cancel_left, pow_succ, WeierstrassCurve.Jacobian.smul_fin3, neg_sq, MulZeroClass.mul_zero, And.left, div_pow, WeierstrassCurve.Jacobian.equation_of_Z_eq_zero, Iff.mp, mul_one, 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 :
  ![P x, W.negY P, P z] =
    ![HPow.hPow (β := ℕ) (P z) 2 *
        ![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]
          x,
      HPow.hPow (β := ℕ) (P z) 3 *
        ![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]
          y,
      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]
          z]
⊢ W.neg P =
    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]

Tactic:
rw [neg, smul_fin3]

Premises used: WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
simp :
  ![P x, W.negY P, P z] =
    ![HPow.hPow (β := ℕ) (P z) 2 * (P x / HPow.hPow (β := ℕ) (P z) 2),
      HPow.hPow (β := ℕ) (P z) 3 *
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
      P z * 1]
⊢ ![P x, W.negY P, P z] =
    ![HPow.hPow (β := ℕ) (P z) 2 *
        ![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]
          x,
      HPow.hPow (β := ℕ) (P z) 3 *
        ![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]
          y,
      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]
          z]

Tactic:
simp only [fin3_def_ext]

Premises used: WeierstrassCurve.Jacobian.fin3_def_ext
-- 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 :
  ![P x, W.negY P, P z] =
    ![P x,
      HPow.hPow (β := ℕ) (P z) 3 *
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
      P z * 1]
rw₁ : ![P x, W.negY P, P z] = ![P x, HPow.hPow (β := ℕ) (P z) 3 * (W.negY P / HPow.hPow (β := ℕ) (P z) 3), P z * 1]
rw₂ : ![P x, W.negY P, P z] = ![P x, W.negY P, P z * 1]
rw₃ rw₄ : ![P x, W.negY P, P z] = ![P x, W.negY P, P z]
⊢ ![P x, W.negY P, P z] =
    ![HPow.hPow (β := ℕ) (P z) 2 * (P x / HPow.hPow (β := ℕ) (P z) 2),
      HPow.hPow (β := ℕ) (P z) 3 *
        W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3),
      P z * 1]

Tactic:
rw [mul_div_cancel₀ _ <| pow_ne_zero 2 hPz, ← negY_of_Z_ne_zero hPz,
    mul_div_cancel₀ _ <| pow_ne_zero 3 hPz, mul_one]

Premises used: WeierstrassCurve.Jacobian.negY_of_Z_ne_zero, pow_ne_zero, mul_div_cancel₀, mul_one, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : P z ≠ 0
⊢ W.Nonsingular
    ![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:
(nonsingular_some ..).mpr <| (Affine.nonsingular_neg ..).mpr <|
    (nonsingular_of_Z_ne_zero hPz).mp hP

Premises used: Iff.mpr, Iff.mp, WeierstrassCurve.Jacobian.nonsingular_some, WeierstrassCurve.Jacobian.nonsingular_of_Z_ne_zero, WeierstrassCurve.Affine.nonsingular_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
pos : ∀ (hPz : P z = 0), 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.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian 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 hPz, nonsingular_smul _
        ((isUnit_Y_of_Z_eq_zero hP hPz).div <| isUnit_X_of_Z_eq_zero hP hPz).neg, nonsingular_zero]

Premises used: WeierstrassCurve.Jacobian.nonsingular_smul, WeierstrassCurve.Jacobian.isUnit_Y_of_Z_eq_zero, IsUnit.div, IsUnit.neg, WeierstrassCurve.Jacobian.nonsingular_zero, WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero, WeierstrassCurve.Jacobian.neg_of_Z_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hP : W.Nonsingular P
hPz : ¬P z = 0
⊢ 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: Ne.isUnit, WeierstrassCurve.Jacobian.nonsingular_smul, _private.0.WeierstrassCurve.Jacobian.nonsingular_neg_of_Z_ne_zero, WeierstrassCurve.Jacobian.neg_of_Z_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ addZ P (W'.neg P) = 0

Tactic:
addZ_of_X_eq rfl

Premises used: WeierstrassCurve.Jacobian.addZ_of_X_eq, rfl