awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hPz : P z = 0
rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = (P x * Q z) • Q
rw₁ : ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, W'.addY P Q, addZ P Q] = (P x * Q z) • Q
rw₂ : ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y, addZ P Q] = (P x * Q z) • Q
rw₃ :
  ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y, P x * Q z * Q z] = (P x * Q z) • Q
rw₄ rw₅ :
  ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y, P x * Q z * Q z] =
    ![HPow.hPow (β := ℕ) (P x * Q z) 2 * Q x, HPow.hPow (β := ℕ) (P x * Q z) 3 * Q y, P x * Q z * Q z]
⊢ W'.addXYZ P Q = (P x * Q z) • Q

Tactic:
rw [addXYZ, addX_of_Z_eq_zero_left hPz, addY_of_Z_eq_zero_left hP hPz, addZ_of_Z_eq_zero_left hPz,
    smul_fin3]

Premises used: WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_left, WeierstrassCurve.Jacobian.addXYZ, WeierstrassCurve.Jacobian.addY_of_Z_eq_zero_left, WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_left
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
inst : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
rw : ![W'.addX P Q, W'.addY P Q, addZ P Q] = -(Q x * P z) • P
rw₁ : ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, W'.addY P Q, addZ P Q] = -(Q x * P z) • P
rw₂ :
  ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y, addZ P Q] = -(Q x * P z) • P
rw₃ :
  ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y, -(Q x * P z) * P z] =
    -(Q x * P z) • P
rw₄ rw₅ :
  ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y, -(Q x * P z) * P z] =
    ![HPow.hPow (β := ℕ) (-(Q x * P z)) 2 * P x, HPow.hPow (β := ℕ) (-(Q x * P z)) 3 * P y, -(Q x * P z) * P z]
⊢ W'.addXYZ P Q = -(Q x * P z) • P

Tactic:
rw [addXYZ, addX_of_Z_eq_zero_right hQz, addY_of_Z_eq_zero_right hQ hQz,
    addZ_of_Z_eq_zero_right hQz, smul_fin3]

Premises used: WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_right, WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.addXYZ, WeierstrassCurve.Jacobian.addY_of_Z_eq_zero_right, WeierstrassCurve.Jacobian.addX_of_Z_eq_zero_right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * HPow.hPow (β := ℕ) (Q z) 2 = Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![1, 1, 0]

Tactic:
simp [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx, addZ_of_X_eq hx,
    smul_fin3]

Premises used: WeierstrassCurve.Jacobian.smul_fin3, WeierstrassCurve.Jacobian.addX_of_X_eq, WeierstrassCurve.Jacobian.addXYZ, WeierstrassCurve.Jacobian.addZ_of_X_eq, WeierstrassCurve.Jacobian.addY_of_X_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
inst : Field F
W : Jacobian 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 * HPow.hPow (β := ℕ) (Q z) 2 ≠ Q x * HPow.hPow (β := ℕ) (P z) 2
⊢ ∀ {n : ℕ}, IsUnit (addZ P Q ^ n)

Tactic:
have hZ {n : ℕ} : IsUnit <| addZ P Q ^ n := (isUnit_addZ_of_X_ne hx).pow n
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
simp :
  -((⇑f : (a : R) → S) ∘ P) y - (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) x * ((⇑f : (a : R) → S) ∘ P) z -
      (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 3 =
    (f : (a : R) → S) (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)
⊢ (W'.map f).negY ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.negY P)

Tactic:
simp only [negY]

Premises used: WeierstrassCurve.Jacobian.negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ -((⇑f : (a : R) → S) ∘ P) y - (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) x * ((⇑f : (a : R) → S) ∘ P) z -
      (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 3 =
    (f : (a : R) → S) (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
simp :
  (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) y * ((⇑f : (a : R) → S) ∘ P) z -
      (3 * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) x) 2 +
          2 * (W'.map f).a₂ * ((⇑f : (a : R) → S) ∘ P) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 +
        (W'.map f).a₄ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 4) =
    (f : (a : R) → S)
      (W'.a₁ * P y * P z -
        (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₄ * HPow.hPow (β := ℕ) (P z) 4))
⊢ (W'.map f).dblU ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.dblU P)

Tactic:
simp only [dblU_eq]

Premises used: WeierstrassCurve.Jacobian.dblU_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) y * ((⇑f : (a : R) → S) ∘ P) z -
      (3 * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) x) 2 +
          2 * (W'.map f).a₂ * ((⇑f : (a : R) → S) ∘ P) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 +
        (W'.map f).a₄ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 4) =
    (f : (a : R) → S)
      (W'.a₁ * P y * P z -
        (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W'.a₂ * P x * HPow.hPow (β := ℕ) (P z) 2 +
          W'.a₄ * HPow.hPow (β := ℕ) (P z) 4))

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
simp :
  ((⇑f : (a : R) → S) ∘ P) z *
      (((⇑f : (a : R) → S) ∘ P) y -
        (-((⇑f : (a : R) → S) ∘ P) y - (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) x * ((⇑f : (a : R) → S) ∘ P) z -
          (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 3)) =
    (f : (a : R) → S) (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)))
⊢ (W'.map f).dblZ ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.dblZ P)

Tactic:
simp only [dblZ, negY]

Premises used: WeierstrassCurve.Jacobian.negY, WeierstrassCurve.Jacobian.dblZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ ((⇑f : (a : R) → S) ∘ P) z *
      (((⇑f : (a : R) → S) ∘ P) y -
        (-((⇑f : (a : R) → S) ∘ P) y - (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) x * ((⇑f : (a : R) → S) ∘ P) z -
          (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 3)) =
    (f : (a : R) → S) (P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * HPow.hPow (β := ℕ) (P z) 3)))

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
simp :
  HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (W'.dblU P) : S) 2 -
          HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.dblU P) : S) * ((⇑f : (a : R) → S) ∘ P) z *
            HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S) -
        (W'.map f).a₂ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 *
          HPow.hPow (β := ℕ)
            (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 2 -
      HMul.hMul (α := S) 2 (((⇑f : (a : R) → S) ∘ P) x) *
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 2 =
    (f : (a : R) → S)
      (HPow.hPow (β := ℕ) (W'.dblU P) 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) -
          W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
        2 * P x * HPow.hPow (β := ℕ) (P y - W'.negY P) 2)
⊢ (W'.map f).dblX ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.dblX P)

Tactic:
simp only [dblX, map_dblU, map_negY]

Premises used: WeierstrassCurve.Jacobian.map_negY, WeierstrassCurve.Jacobian.dblX, WeierstrassCurve.Jacobian.map_dblU
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (W'.dblU P) : S) 2 -
          HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.dblU P) : S) * ((⇑f : (a : R) → S) ∘ P) z *
            HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S) -
        (W'.map f).a₂ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 *
          HPow.hPow (β := ℕ)
            (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 2 -
      HMul.hMul (α := S) 2 (((⇑f : (a : R) → S) ∘ P) x) *
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 2 =
    (f : (a : R) → S)
      (HPow.hPow (β := ℕ) (W'.dblU P) 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) -
          W'.a₂ * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (P y - W'.negY P) 2 -
        2 * P x * HPow.hPow (β := ℕ) (P y - W'.negY P) 2)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
simp :
  HMul.hMul (α := S) (-(f : (a : R) → S) (W'.dblU P) : S)
        (HSub.hSub (α := S) ((f : (a : R) → S) (W'.dblX P) : S)
          (((⇑f : (a : R) → S) ∘ P) x *
            HPow.hPow (β := ℕ)
              (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 2)) +
      ((⇑f : (a : R) → S) ∘ P) y *
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 3 =
    (f : (a : R) → S)
      (-W'.dblU P * (W'.dblX P - P x * HPow.hPow (β := ℕ) (P y - W'.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P y - W'.negY P) 3)
⊢ (W'.map f).negDblY ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.negDblY P)

Tactic:
simp only [negDblY, map_dblU, map_dblX, map_negY]

Premises used: WeierstrassCurve.Jacobian.map_dblX, WeierstrassCurve.Jacobian.map_negY, WeierstrassCurve.Jacobian.map_dblU, WeierstrassCurve.Jacobian.negDblY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ HMul.hMul (α := S) (-(f : (a : R) → S) (W'.dblU P) : S)
        (HSub.hSub (α := S) ((f : (a : R) → S) (W'.dblX P) : S)
          (((⇑f : (a : R) → S) ∘ P) x *
            HPow.hPow (β := ℕ)
              (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 2)) +
      ((⇑f : (a : R) → S) ∘ P) y *
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := S) (β := S) (((⇑f : (a : R) → S) ∘ P) y : S) ((f : (a : R) → S) (W'.negY P) : S)) 3 =
    (f : (a : R) → S)
      (-W'.dblU P * (W'.dblX P - P x * HPow.hPow (β := ℕ) (P y - W'.negY P) 2) +
        P y * HPow.hPow (β := ℕ) (P y - W'.negY P) 3)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
simp :
  HSub.hSub (α := S) (-(f : (a : R) → S) (W'.negDblY P) : S)
        (HMul.hMul (β := S) (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.dblX P) : S))
          ((f : (a : R) → S) (W'.dblZ P) : S)) -
      (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (W'.dblZ P) : S) 3 =
    (f : (a : R) → S) (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * HPow.hPow (β := ℕ) (W'.dblZ P) 3)
⊢ (W'.map f).dblY ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.dblY P)

Tactic:
simp only [dblY, negY_eq, map_negDblY, map_dblX, map_dblZ]

Premises used: WeierstrassCurve.Jacobian.map_dblX, WeierstrassCurve.Jacobian.map_negDblY, WeierstrassCurve.Jacobian.negY_eq, WeierstrassCurve.Jacobian.map_dblZ, WeierstrassCurve.Jacobian.dblY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ HSub.hSub (α := S) (-(f : (a : R) → S) (W'.negDblY P) : S)
        (HMul.hMul (β := S) (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.dblX P) : S))
          ((f : (a : R) → S) (W'.dblZ P) : S)) -
      (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (W'.dblZ P) : S) 3 =
    (f : (a : R) → S) (-W'.negDblY P - W'.a₁ * W'.dblX P * W'.dblZ P - W'.a₃ * HPow.hPow (β := ℕ) (W'.dblZ P) 3)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P : Fin 3 → R
⊢ (W'.map f).dblXYZ ((⇑f : (a : R) → S) ∘ P) = (⇑f : (a : R) → S) ∘ W'.dblXYZ P

Tactic:
simp only [dblXYZ, map_dblX, map_dblY, map_dblZ, comp_fin3]

Premises used: WeierstrassCurve.Jacobian.map_dblX, WeierstrassCurve.Jacobian.map_dblZ, WeierstrassCurve.Jacobian.dblXYZ, WeierstrassCurve.Jacobian.map_dblY, WeierstrassCurve.Jacobian.comp_fin3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
simp :
  -((((⇑f : (a : F) → K) ∘ P) y * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ Q) z) 3 -
          ((⇑f : (a : F) → K) ∘ Q) y * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) z) 3) /
        HMul.hMul (α := K) (((⇑f : (a : F) → K) ∘ P) z) (((⇑f : (a : F) → K) ∘ Q) z)) =
    (f : (a : F) → K) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)))
⊢ Eq.{v + 1} (α := K) (addU ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) : K) ((f : (a : F) → K) (addU P Q) : K)

Tactic:
simp only [addU]

Premises used: WeierstrassCurve.Jacobian.addU
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ -((((⇑f : (a : F) → K) ∘ P) y * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ Q) z) 3 -
          ((⇑f : (a : F) → K) ∘ Q) y * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) z) 3) /
        HMul.hMul (α := K) (((⇑f : (a : F) → K) ∘ P) z) (((⇑f : (a : F) → K) ∘ Q) z)) =
    (f : (a : F) → K) (-((P y * HPow.hPow (β := ℕ) (Q z) 3 - Q y * HPow.hPow (β := ℕ) (P z) 3) / (P z * Q z)))

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
P Q : Fin 3 → R
simp :
  ((⇑f : (a : R) → S) ∘ P) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ Q) z) 2 -
      ((⇑f : (a : R) → S) ∘ Q) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 =
    (f : (a : R) → S) (P x * HPow.hPow (β := ℕ) (Q z) 2 - Q x * HPow.hPow (β := ℕ) (P z) 2)
⊢ Eq.{s + 1} (α := S) (addZ ((⇑f : (a : R) → S) ∘ P) ((⇑f : (a : R) → S) ∘ Q) : S) ((f : (a : R) → S) (addZ P Q) : S)

Tactic:
simp only [addZ]

Premises used: WeierstrassCurve.Jacobian.addZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
P Q : Fin 3 → R
⊢ ((⇑f : (a : R) → S) ∘ P) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ Q) z) 2 -
      ((⇑f : (a : R) → S) ∘ Q) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 =
    (f : (a : R) → S) (P x * HPow.hPow (β := ℕ) (Q z) 2 - Q x * HPow.hPow (β := ℕ) (P z) 2)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P Q : Fin 3 → R
⊢ ((⇑f : (a : R) → S) ∘ P) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ Q) x) 2 *
                          HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 -
                        HMul.hMul (α := S) 2 (((⇑f : (a : R) → S) ∘ P) y) * ((⇑f : (a : R) → S) ∘ Q) y *
                            ((⇑f : (a : R) → S) ∘ P) z *
                          ((⇑f : (a : R) → S) ∘ Q) z +
                      HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) x) 2 * ((⇑f : (a : R) → S) ∘ Q) x *
                        HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ Q) z) 2 -
                    (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) x * ((⇑f : (a : R) → S) ∘ Q) y *
                        HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 *
                      ((⇑f : (a : R) → S) ∘ Q) z -
                  (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) y * ((⇑f : (a : R) → S) ∘ Q) x * ((⇑f : (a : R) → S) ∘ P) z *
                    HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ Q) z) 2 +
                2 * (W'.map f).a₂ * ((⇑f : (a : R) → S) ∘ P) x * ((⇑f : (a : R) → S) ∘ Q) x *
                    HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 *
                  HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ Q) z) 2 -
              (W'.map f).a₃ * ((⇑f : (a : R) → S) ∘ Q) y * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 4 *
                ((⇑f : (a : R) → S) ∘ Q) z -
            (W'.map f).a₃ * ((⇑f : (a : R) → S) ∘ P) y * ((⇑f : (a : R) → S) ∘ P) z *
              HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ Q) z) 4 +
          (W'.map f).a₄ * ((⇑f : (a : R) → S) ∘ Q) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 4 *
            HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ Q) z) 2 +
        (W'.map f).a₄ * ((⇑f : (a : R) → S) ∘ P) x * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 2 *
          HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ Q) z) 4 +
      2 * (W'.map f).a₆ * HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ P) z) 4 *
        HPow.hPow (α := S) (β := ℕ) (((⇑f : (a : R) → S) ∘ Q) z) 4 =
    (f : (a : R) → S)
      (P x * HPow.hPow (β := ℕ) (Q x) 2 * HPow.hPow (β := ℕ) (P z) 2 - 2 * P y * Q y * P z * Q z +
                        HPow.hPow (β := ℕ) (P x) 2 * Q x * HPow.hPow (β := ℕ) (Q z) 2 -
                      W'.a₁ * P x * Q y * HPow.hPow (β := ℕ) (P z) 2 * Q z -
                    W'.a₁ * P y * Q x * P z * HPow.hPow (β := ℕ) (Q z) 2 +
                  2 * W'.a₂ * P x * Q x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 2 -
                W'.a₃ * Q y * HPow.hPow (β := ℕ) (P z) 4 * Q z -
              W'.a₃ * P y * P z * HPow.hPow (β := ℕ) (Q z) 4 +
            W'.a₄ * Q x * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 2 +
          W'.a₄ * P x * HPow.hPow (β := ℕ) (P z) 2 * HPow.hPow (β := ℕ) (Q z) 4 +
        2 * W'.a₆ * HPow.hPow (β := ℕ) (P z) 4 * HPow.hPow (β := ℕ) (Q z) 4)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P Q : Fin 3 → R
simp :
  HSub.hSub (α := S) (-(f : (a : R) → S) (W'.negAddY P Q) : S)
        (HMul.hMul (β := S) (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.addX P Q) : S))
          ((f : (a : R) → S) (addZ P Q) : S)) -
      (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (addZ P Q) : S) 3 =
    (f : (a : R) → S) (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * HPow.hPow (β := ℕ) (addZ P Q) 3)
⊢ (W'.map f).addY ((⇑f : (a : R) → S) ∘ P) ((⇑f : (a : R) → S) ∘ Q) = (f : (a : R) → S) (W'.addY P Q)

Tactic:
simp only [addY, negY_eq, map_negAddY, map_addX, map_addZ]

Premises used: WeierstrassCurve.Jacobian.map_addX, WeierstrassCurve.Jacobian.addY, WeierstrassCurve.Jacobian.negY_eq, WeierstrassCurve.Jacobian.map_addZ, WeierstrassCurve.Jacobian.map_negAddY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P Q : Fin 3 → R
⊢ HSub.hSub (α := S) (-(f : (a : R) → S) (W'.negAddY P Q) : S)
        (HMul.hMul (β := S) (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.addX P Q) : S))
          ((f : (a : R) → S) (addZ P Q) : S)) -
      (W'.map f).a₃ * HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (addZ P Q) : S) 3 =
    (f : (a : R) → S) (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * HPow.hPow (β := ℕ) (addZ P Q) 3)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Jacobian R
f : R →+* S
P Q : Fin 3 → R
⊢ (W'.map f).addXYZ ((⇑f : (a : R) → S) ∘ P) ((⇑f : (a : R) → S) ∘ Q) = (⇑f : (a : R) → S) ∘ W'.addXYZ P Q

Tactic:
simp only [addXYZ, map_addX, map_addY, map_addZ, comp_fin3]

Premises used: WeierstrassCurve.Jacobian.map_addX, WeierstrassCurve.Jacobian.map_addZ, WeierstrassCurve.Jacobian.map_addY, WeierstrassCurve.Jacobian.addXYZ, WeierstrassCurve.Jacobian.comp_fin3
-- 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).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negY P)
rw₁ :
  (W'⁄B).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₂ rw₃ : (W'⁄B).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).negY ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).negY ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).negY P)

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

Premises used: WeierstrassCurve.Jacobian.map_negY, 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).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).dblU P)
rw₁ :
  (W'⁄B).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₂ rw₃ : (W'⁄B).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).dblU ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).dblU ((⇑f : (a : A) → B) ∘ P) = (f : (a : A) → B) ((W'⁄A).dblU P)

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

Premises used: RingHom.coe_coe, WeierstrassCurve.Jacobian.map_baseChange, WeierstrassCurve.Jacobian.map_dblU