awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
P : Fin 3 → R
⊢ (W'.map f).Equation ((⇑f : (a : R) → S) ∘ P) ↔ W'.Equation P

Tactic:
simp only [Equation, map_polynomial, eval_map, ← eval₂_comp, map_eq_zero_iff f hf]

Premises used: MvPolynomial.eval_map, WeierstrassCurve.Jacobian.Equation, map_eq_zero_iff, WeierstrassCurve.Jacobian.map_polynomial, MvPolynomial.eval₂_comp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
f : R →+* S
⊢ Eq (α := MvPolynomial (Fin 3) S) (W'.map f).polynomialX
    (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
        (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
      W'.polynomialX)

Tactic:
simp only [polynomialX, map_polynomial, pderiv_map]

Premises used: WeierstrassCurve.Jacobian.polynomialX, MvPolynomial.pderiv_map, WeierstrassCurve.Jacobian.map_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
f : R →+* S
⊢ Eq (α := MvPolynomial (Fin 3) S) (W'.map f).polynomialY
    (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
        (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
      W'.polynomialY)

Tactic:
simp only [polynomialY, map_polynomial, pderiv_map]

Premises used: MvPolynomial.pderiv_map, WeierstrassCurve.Jacobian.map_polynomial, WeierstrassCurve.Jacobian.polynomialY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
f : R →+* S
⊢ Eq (α := MvPolynomial (Fin 3) S) (W'.map f).polynomialZ
    (((MvPolynomial.map f : RingHom.{r, s} (MvPolynomial (Fin 3) R) (MvPolynomial (Fin 3) S)) :
        (a : MvPolynomial (Fin 3) R) → MvPolynomial (Fin 3) S)
      W'.polynomialZ)

Tactic:
simp only [polynomialZ, map_polynomial, pderiv_map]

Premises used: MvPolynomial.pderiv_map, WeierstrassCurve.Jacobian.map_polynomial, WeierstrassCurve.Jacobian.polynomialZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
P : Fin 3 → R
⊢ (W'.map f).Nonsingular ((⇑f : (a : R) → S) ∘ P) ↔ W'.Nonsingular P

Tactic:
simp only [Nonsingular, W'.map_equation hf, map_polynomialX, map_polynomialY, map_polynomialZ,
    eval_map, ← eval₂_comp, map_ne_zero_iff f hf]

Premises used: WeierstrassCurve.Jacobian.map_equation, MvPolynomial.eval_map, WeierstrassCurve.Jacobian.map_polynomialZ, MvPolynomial.eval₂_comp, WeierstrassCurve.Jacobian.Nonsingular, map_ne_zero_iff, WeierstrassCurve.Jacobian.map_polynomialY, WeierstrassCurve.Jacobian.map_polynomialX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
⊢ (W'⁄A).map (↑f : A →+* B) = W'⁄B

Tactic:
WeierstrassCurve.map_baseChange W' f

Premises used: WeierstrassCurve.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial ((W'⁄A).map (↑f : A →+* B)).polynomial
rw₁ rw₂ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial (W'⁄B).polynomial
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomial
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomial)

Tactic:
rw [← map_polynomial, map_baseChange]

Premises used: WeierstrassCurve.Jacobian.map_baseChange, WeierstrassCurve.Jacobian.map_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
h : (W'⁄A).Equation P
⊢ ((W'⁄A).map f.toRingHom).Equation ((⇑f.toRingHom : (a : A) → B) ∘ P)

Tactic:
Equation.map f.toRingHom h

Premises used: AlgHom.toRingHom, WeierstrassCurve.Jacobian.Equation.map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
h : (W'⁄A).Equation P
h₁ : W'⁄B = (W'⁄A).map f.toRingHom
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P)

Tactic:
convert! Equation.map f.toRingHom h using 1

Premises used: AlgHom.toRingHom, WeierstrassCurve.Jacobian.Equation.map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
h : (W'⁄A).Equation P
h₁ : W'⁄B = (W'⁄A).map (↑f : A →+* B)
h₂ h₃ : W'⁄B = W'⁄B
⊢ W'⁄B = (W'⁄A).map f.toRingHom

Tactic:
rw [AlgHom.toRingHom_eq_coe, map_baseChange]

Premises used: WeierstrassCurve.Jacobian.map_baseChange, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P
rw₁ :
  (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Equation ((⇑f.toRingHom : (a : A) → B) ∘ P)
rw₂ :
  (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map (↑f : A →+* B)).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₃ rw₄ : (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄B).Equation ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).Equation ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Equation P

Tactic:
rw [← RingHom.coe_coe, ← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]

Premises used: WeierstrassCurve.Jacobian.map_equation, RingHom.coe_coe, WeierstrassCurve.Jacobian.map_baseChange, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX ((W'⁄A).map (↑f : A →+* B)).polynomialX
rw₁ rw₂ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX (W'⁄B).polynomialX
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialX
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialX)

Tactic:
rw [← map_polynomialX, map_baseChange]

Premises used: WeierstrassCurve.Jacobian.map_baseChange, WeierstrassCurve.Jacobian.map_polynomialX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY ((W'⁄A).map (↑f : A →+* B)).polynomialY
rw₁ rw₂ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY (W'⁄B).polynomialY
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialY
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialY)

Tactic:
rw [← map_polynomialY, map_baseChange]

Premises used: WeierstrassCurve.Jacobian.map_baseChange, WeierstrassCurve.Jacobian.map_polynomialY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
rw : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ ((W'⁄A).map (↑f : A →+* B)).polynomialZ
rw₁ rw₂ : Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ (W'⁄B).polynomialZ
⊢ Eq (α := MvPolynomial (Fin 3) B) (W'⁄B).polynomialZ
    (((MvPolynomial.map (↑f : A →+* B) : RingHom.{u, v} (MvPolynomial (Fin 3) A) (MvPolynomial (Fin 3) B)) :
        (a : MvPolynomial (Fin 3) A) → MvPolynomial (Fin 3) B)
      (W'⁄A).polynomialZ)

Tactic:
rw [← map_polynomialZ, map_baseChange]

Premises used: WeierstrassCurve.Jacobian.map_baseChange, WeierstrassCurve.Jacobian.map_polynomialZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
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
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
P : Fin 3 → A
rw : (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P
rw₁ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map f.toRingHom).Nonsingular ((⇑f.toRingHom : (a : A) → B) ∘ P)
rw₂ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔
    ((W'⁄A).map (↑f : A →+* B)).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₃ rw₄ :
  (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) ↔ (W'⁄B).Nonsingular ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).Nonsingular ((⇑f : (a : A) → B) ∘ P) ↔ (W'⁄A).Nonsingular P

Tactic:
rw [← RingHom.coe_coe, ← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Jacobian.map_baseChange, WeierstrassCurve.Jacobian.map_nonsingular, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
X Y Z : R
⊢ W'.negY ![X, Y, Z] = -Y - W'.a₁ * X * Z - W'.a₃ * HPow.hPow (β := ℕ) Z 3

Tactic:
rfl

Premises used: Eq.mpr, WeierstrassCurve.Jacobian.negY, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
simp :
  -(HPow.hPow (β := ℕ) u 3 * P y) - W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (u * P z) -
      W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 3 =
    HPow.hPow (β := ℕ) u 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)
⊢ W'.negY (u • P) = HPow.hPow (β := ℕ) u 3 * W'.negY P

Tactic:
simp only [negY, smul_fin3_ext]

Premises used: WeierstrassCurve.Jacobian.negY, WeierstrassCurve.Jacobian.smul_fin3_ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ -(HPow.hPow (β := ℕ) u 3 * P y) - W'.a₁ * (HPow.hPow (β := ℕ) u 2 * P x) * (u * P z) -
      W'.a₃ * HPow.hPow (β := ℕ) (u * P z) 3 =
    HPow.hPow (β := ℕ) u 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
rw : -P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3 = -P y
rw₁ : -P y - W'.a₁ * P x * 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₂ : -P y - 0 - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₃ : -P y - W'.a₃ * HPow.hPow (α := R) (β := ℕ) 0 3 = -P y
rw₄ : -P y - W'.a₃ * 0 = -P y
rw₅ : -P y - 0 = -P y
rw₆ rw₇ : -P y = -P y
⊢ W'.negY P = -P y

Tactic:
rw [negY, hPz, mul_zero, sub_zero, zero_pow three_ne_zero, mul_zero, sub_zero]

Premises used: sub_zero, WeierstrassCurve.Jacobian.negY, MulZeroClass.mul_zero, three_ne_zero, zero_pow
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
a :
  (-P y - W.a₁ * P x * P z - W.a₃ * HPow.hPow (β := ℕ) (P z) 3) / HPow.hPow (β := ℕ) (P z) 3 +
        (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₃ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
      (-(P y / HPow.hPow (β := ℕ) (P z) 3) - W.toAffine.a₁ * (P x / HPow.hPow (β := ℕ) (P z) 2) - W.toAffine.a₃ +
        (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) + W.a₃ * 1)) =
    0
⊢ W.negY P / HPow.hPow (β := ℕ) (P z) 3 +
        (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₃ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
      (W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) +
        (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) + W.a₃ * 1)) =
    0

Tactic:
rw [negY, Affine.negY]

Premises used: WeierstrassCurve.Jacobian.negY, WeierstrassCurve.Affine.negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (-P y - W.a₁ * P x * P z - W.a₃ * HPow.hPow (β := ℕ) (P z) 3) / HPow.hPow (β := ℕ) (P z) 3 +
        (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₃ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
      (-(P y / HPow.hPow (β := ℕ) (P z) 3) - W.toAffine.a₁ * (P x / HPow.hPow (β := ℕ) (P z) 2) - W.toAffine.a₃ +
        (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) + W.a₃ * 1)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
a :
  W.negY P / HPow.hPow (β := ℕ) (P z) 3 +
        (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * 1 +
          W.a₃ * (HPow.hPow (β := ℕ) (P z) 3 / HPow.hPow (β := ℕ) (P z) 3)) -
      (W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3) +
        (-W.a₁ * P x / HPow.hPow (β := ℕ) (P z) 2 * (P z / P z) + W.a₃ * 1)) =
    0
⊢ W.negY P / HPow.hPow (β := ℕ) (P z) 3 =
    W.toAffine.negY (P x / HPow.hPow (β := ℕ) (P z) 2) (P y / HPow.hPow (β := ℕ) (P z) 3)

Tactic:
linear_combination (norm := (rw [negY, Affine.negY]; ring1))
    -W.a₁ * P x / P z ^ 2 * div_self hPz - W.a₃ * div_self (pow_ne_zero 3 hPz)

Premises used: WeierstrassCurve.Jacobian.negY, pow_ne_zero, WeierstrassCurve.a₃, WeierstrassCurve.Affine.negY, OfNat.ofNat, div_self, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ (P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) *
          (P y * HPow.hPow (β := ℕ) (Q z) 3 -
            (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * HPow.hPow (β := ℕ) (Q z) 3) * HPow.hPow (β := ℕ) (P z) 3) +
        (HPow.hPow (β := ℕ) (Q z) 6 * 0 +
            HPow.hPow (β := ℕ) (P z) 6 *
              (HPow.hPow (β := ℕ) (Q y) 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * HPow.hPow (β := ℕ) (Q z) 3 -
                (HPow.hPow (β := ℕ) (Q x) 3 + W'.a₂ * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                    W'.a₄ * Q x * HPow.hPow (β := ℕ) (Q z) 4 +
                  W'.a₆ * HPow.hPow (β := ℕ) (Q z) 6)) +
          (HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 4 +
                        P x * Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                      HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 4 -
                    W'.a₁ * P y * P z * HPow.hPow (β := ℕ) (Q z) 4 +
                  W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 4 +
                W'.a₂ * Q x * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 2 +
              W'.a₄ * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 4) *
            (Q x * HPow.hPow (β := ℕ) (P z) 2)) -
      (0 +
        (HPow.hPow (β := ℕ) (Q z) 6 *
              (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)) +
            HPow.hPow (β := ℕ) (P z) 6 * 0 +
          (HPow.hPow (β := ℕ) (P x) 2 * HPow.hPow (β := ℕ) (Q z) 4 +
                        P x * Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 +
                      HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 4 -
                    W'.a₁ * P y * P z * HPow.hPow (β := ℕ) (Q z) 4 +
                  W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 4 +
                W'.a₂ * Q x * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 2 +
              W'.a₄ * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 4) *
            (P x * HPow.hPow (β := ℕ) (Q z) 2))) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
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
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 = W'.negY Q * HPow.hPow (β := ℕ) (P z) 3

Tactic:
sub_eq_zero.mp <| (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_left <|
    sub_ne_zero.mpr hy

Premises used: Iff.mpr, sub_eq_zero, sub_ne_zero, Or.resolve_left, mul_eq_zero, WeierstrassCurve.Jacobian.Y_sub_Y_mul_Y_sub_negY, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
hy : P y * HPow.hPow (β := ℕ) (Q z) 3 ≠ W'.negY Q * HPow.hPow (β := ℕ) (P z) 3
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 = Q y * HPow.hPow (β := ℕ) (P z) 3

Tactic:
sub_eq_zero.mp <| (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_right <|
    sub_ne_zero.mpr hy

Premises used: Iff.mpr, sub_eq_zero, sub_ne_zero, mul_eq_zero, WeierstrassCurve.Jacobian.Y_sub_Y_mul_Y_sub_negY, Iff.mp, Or.resolve_right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 = W.negY Q * HPow.hPow (β := ℕ) (P z) 3 ↔
    P y / HPow.hPow (β := ℕ) (P z) 3 =
      W.toAffine.negY (Q x / HPow.hPow (β := ℕ) (Q z) 2) (Q y / HPow.hPow (β := ℕ) (Q z) 3)

Tactic:
negY_of_Z_ne_zero hQz ▸ (div_eq_div_iff (pow_ne_zero 3 hPz) (pow_ne_zero 3 hQz)).symm

Premises used: WeierstrassCurve.Jacobian.negY_of_Z_ne_zero, pow_ne_zero, Eq.rec, div_eq_div_iff, OfNat.ofNat, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
a :
  P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
          (P y * HPow.hPow (β := ℕ) (Q z) 3 -
            (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * HPow.hPow (β := ℕ) (Q z) 3) * HPow.hPow (β := ℕ) (P z) 3) +
        -W'.a₁ * P z * Q z * (Q x * HPow.hPow (β := ℕ) (P z) 2) -
      ((P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) * HPow.hPow (β := ℕ) (Q z) 3 +
        -W'.a₁ * P z * Q z * (P x * HPow.hPow (β := ℕ) (Q z) 2)) =
    0
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
          (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) +
        -W'.a₁ * P z * Q z * (Q x * HPow.hPow (β := ℕ) (P z) 2) -
      ((P y - W'.negY P) * HPow.hPow (β := ℕ) (Q z) 3 + -W'.a₁ * P z * Q z * (P x * HPow.hPow (β := ℕ) (Q z) 2)) =
    0

Tactic:
rw [negY, negY]

Premises used: WeierstrassCurve.Jacobian.negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
          (P y * HPow.hPow (β := ℕ) (Q z) 3 -
            (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * HPow.hPow (β := ℕ) (Q z) 3) * HPow.hPow (β := ℕ) (P z) 3) +
        -W'.a₁ * P z * Q z * (Q x * HPow.hPow (β := ℕ) (P z) 2) -
      ((P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)) * HPow.hPow (β := ℕ) (Q z) 3 +
        -W'.a₁ * P z * Q z * (P x * HPow.hPow (β := ℕ) (Q z) 2)) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
a :
  P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
          (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) +
        -W'.a₁ * P z * Q z * (Q x * HPow.hPow (β := ℕ) (P z) 2) -
      ((P y - W'.negY P) * HPow.hPow (β := ℕ) (Q z) 3 + -W'.a₁ * P z * Q z * (P x * HPow.hPow (β := ℕ) (Q z) 2)) =
    0
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3 +
      (P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3) =
    (P y - W'.negY P) * HPow.hPow (β := ℕ) (Q z) 3

Tactic:
linear_combination (norm := (rw [negY, negY]; ring1)) -W'.a₁ * P z * Q z * hx

Premises used: WeierstrassCurve.Jacobian.negY, OfNat.ofNat, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
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
⊢ P y * HPow.hPow (β := ℕ) (Q z) 3 - W'.negY Q * HPow.hPow (β := ℕ) (P z) 3 = 0

Tactic:
have hy' : P y * Q z ^ 3 - W'.negY Q * P z ^ 3 = 0 :=
    (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_left <| sub_ne_zero_of_ne hy