awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
rw :
  ![W'.addX (u • P) (v • Q), W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₁ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, W'.addY (u • P) (v • Q), W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₂ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q, W'.addZ (u • P) (v • Q)] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₃ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q
rw₄ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q x, HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q y,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
rw₅ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q y,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
rw₆ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addXYZ P Q z]
rw₇ rw₈ :
  ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q] =
    ![HPow.hPow (β := ℕ) (u * v) 2 * W'.addX P Q, HPow.hPow (β := ℕ) (u * v) 2 * W'.addY P Q,
      HPow.hPow (β := ℕ) (u * v) 2 * W'.addZ P Q]
⊢ W'.addXYZ (u • P) (v • Q) = HPow.hPow (β := ℕ) (u * v) 2 • W'.addXYZ P Q

Tactic:
rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]

Premises used: WeierstrassCurve.Projective.addY_smul, WeierstrassCurve.Projective.addX_smul, WeierstrassCurve.Projective.addZ_smul, WeierstrassCurve.Projective.smul_fin3, WeierstrassCurve.Projective.addXYZ_X, WeierstrassCurve.Projective.addXYZ_Z, WeierstrassCurve.Projective.addXYZ_Y, WeierstrassCurve.Projective.addXYZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
P : Fin 3 → R
rw : ![W'.addX P P, W'.addY P P, W'.addZ P P] = ![0, 0, 0]
rw₁ : ![0, W'.addY P P, W'.addZ P P] = ![0, 0, 0]
rw₂ : ![0, 0, W'.addZ P P] = ![0, 0, 0]
rw₃ rw₄ : Eq.{r + 1} (α := Fin 3 → R) ![0, 0, 0] ![0, 0, 0]
⊢ W'.addXYZ P P = ![0, 0, 0]

Tactic:
rw [addXYZ, addX_self, addY_self, addZ_self]

Premises used: WeierstrassCurve.Projective.addZ_self, WeierstrassCurve.Projective.addY_self, WeierstrassCurve.Projective.addXYZ, WeierstrassCurve.Projective.addX_self
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
inst : CommRing R
W' : Projective R
inst_1 : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
rw : ![W'.addX P Q, W'.addY P Q, W'.addZ P Q] = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
rw₁ : ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, W'.addY P Q, W'.addZ P Q] = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
rw₂ :
  ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y, W'.addZ P Q] =
    (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
rw₃ :
  ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y,
      HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z] =
    (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q
rw₄ rw₅ :
  ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y,
      HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z] =
    ![HPow.hPow (β := ℕ) (P y) 2 * Q z * Q x, HPow.hPow (β := ℕ) (P y) 2 * Q z * Q y,
      HPow.hPow (β := ℕ) (P y) 2 * Q z * Q z]
⊢ W'.addXYZ P Q = (HPow.hPow (β := ℕ) (P y) 2 * Q z) • Q

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

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

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

Premises used: WeierstrassCurve.Projective.addZ_of_Z_eq_zero_right, WeierstrassCurve.Projective.smul_fin3, WeierstrassCurve.Projective.addY_of_Z_eq_zero_right, WeierstrassCurve.Projective.addXYZ, WeierstrassCurve.Projective.addX_of_Z_eq_zero_right
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
erw : ![W.addX P Q, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₁ : ![0, W.addY P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₂ : ![0, addU P Q, W.addZ P Q] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₃ : ![0, addU P Q, 0] = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]
erw₄ : ![0, addU P Q, 0] = ![addU P Q * ![0, 1, 0] x, addU P Q * ![0, 1, 0] y, addU P Q * ![0, 1, 0] z]
erw₅ : ![0, addU P Q, 0] = ![0, addU P Q * ![0, 1, 0] y, 0]
erw₆ erw₇ : ![0, addU P Q, 0] = ![0, addU P Q, 0]
⊢ W.addXYZ P Q = HSMul.hSMul (β := Fin (Nat.succ 0).succ.succ → F) (addU P Q) ![0, 1, 0]

Tactic:
erw [addXYZ, addX_of_X_eq hP hQ hPz hQz hx, addY_of_X_eq hP hQ hPz hQz hx,
    addZ_of_X_eq hP hQ hPz hQz hx, smul_fin3, mul_zero, mul_one]

Premises used: WeierstrassCurve.Projective.addY_of_X_eq, WeierstrassCurve.Projective.addX_of_X_eq, MulZeroClass.mul_zero, WeierstrassCurve.Projective.smul_fin3, mul_one, WeierstrassCurve.Projective.addXYZ, WeierstrassCurve.Projective.addZ_of_X_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
inst : Field F
W : Projective F
inst_1 : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ IsUnit (W.addZ P Q)

Tactic:
have hZ : IsUnit <| W.addZ P Q := isUnit_addZ_of_X_ne hP hQ hx
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective 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 -
      (W'.map f).a₃ * ((⇑f : (a : R) → S) ∘ P) z =
    (f : (a : R) → S) (-P y - W'.a₁ * P x - W'.a₃ * P z)
⊢ (W'.map f).negY ((⇑f : (a : R) → S) ∘ P) = (f : (a : R) → S) (W'.negY P)

Tactic:
simp only [negY]

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

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Projective F
f : F →+* K
P : Fin 3 → F
simp :
  HPow.hPow (β := ℕ)
        ((W.map f).a₁ * ((⇑f : (a : F) → K) ∘ P) y * ((⇑f : (a : F) → K) ∘ P) z -
          (3 * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) x) 2 +
              2 * (W.map f).a₂ * ((⇑f : (a : F) → K) ∘ P) x * ((⇑f : (a : F) → K) ∘ P) z +
            (W.map f).a₄ * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) z) 2))
        3 /
      HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) z) 2 =
    (f : (a : F) → K)
      (HPow.hPow (β := ℕ)
          (W.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
          3 /
        HPow.hPow (β := ℕ) (P z) 2)
⊢ (W.map f).dblU ((⇑f : (a : F) → K) ∘ P) = (f : (a : F) → K) (W.dblU P)

Tactic:
simp only [dblU_eq]

Premises used: WeierstrassCurve.Projective.dblU_eq
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Projective F
f : F →+* K
P : Fin 3 → F
⊢ HPow.hPow (β := ℕ)
        ((W.map f).a₁ * ((⇑f : (a : F) → K) ∘ P) y * ((⇑f : (a : F) → K) ∘ P) z -
          (3 * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) x) 2 +
              2 * (W.map f).a₂ * ((⇑f : (a : F) → K) ∘ P) x * ((⇑f : (a : F) → K) ∘ P) z +
            (W.map f).a₄ * HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) z) 2))
        3 /
      HPow.hPow (α := K) (β := ℕ) (((⇑f : (a : F) → K) ∘ P) z) 2 =
    (f : (a : F) → K)
      (HPow.hPow (β := ℕ)
          (W.a₁ * P y * P z -
            (3 * HPow.hPow (β := ℕ) (P x) 2 + 2 * W.a₂ * P x * P z + W.a₄ * HPow.hPow (β := ℕ) (P z) 2))
          3 /
        HPow.hPow (β := ℕ) (P z) 2)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
simp :
  ((⇑f : (a : R) → S) ∘ P) z *
      HPow.hPow (β := ℕ)
        (((⇑f : (a : R) → S) ∘ P) y -
          (-((⇑f : (a : R) → S) ∘ P) y - (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) x -
            (W'.map f).a₃ * ((⇑f : (a : R) → S) ∘ P) z))
        3 =
    (f : (a : R) → S) (P z * HPow.hPow (β := ℕ) (P y - (-P y - W'.a₁ * P x - W'.a₃ * 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.Projective.negY, WeierstrassCurve.Projective.dblZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ ((⇑f : (a : R) → S) ∘ P) z *
      HPow.hPow (β := ℕ)
        (((⇑f : (a : R) → S) ∘ P) y -
          (-((⇑f : (a : R) → S) ∘ P) y - (W'.map f).a₁ * ((⇑f : (a : R) → S) ∘ P) x -
            (W'.map f).a₃ * ((⇑f : (a : R) → S) ∘ P) z))
        3 =
    (f : (a : R) → S) (P z * HPow.hPow (β := ℕ) (P y - (-P y - W'.a₁ * P x - W'.a₃ * P z)) 3)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
simp :
  HSub.hSub (α := S) (-(f : (a : R) → S) (W'.negDblY P) : S)
        (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.dblX P) : S)) -
      HMul.hMul (β := S) (W'.map f).a₃ ((f : (a : R) → S) (W'.dblZ P) : S) =
    (f : (a : R) → S) (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P)
⊢ (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.Projective.map_dblZ, WeierstrassCurve.Projective.negY_eq, WeierstrassCurve.Projective.dblY, WeierstrassCurve.Projective.map_negDblY, WeierstrassCurve.Projective.map_dblX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective R
f : R →+* S
P : Fin 3 → R
⊢ HSub.hSub (α := S) (-(f : (a : R) → S) (W'.negDblY P) : S)
        (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.dblX P) : S)) -
      HMul.hMul (β := S) (W'.map f).a₃ ((f : (a : R) → S) (W'.dblZ P) : S) =
    (f : (a : R) → S) (-W'.negDblY P - W'.a₁ * W'.dblX P - W'.a₃ * W'.dblZ P)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective 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.Projective.map_dblZ, WeierstrassCurve.Projective.dblXYZ, WeierstrassCurve.Projective.map_dblY, WeierstrassCurve.Projective.comp_fin3, WeierstrassCurve.Projective.map_dblX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
simp :
  -HPow.hPow (β := ℕ)
          (HMul.hMul (α := K) (((⇑f : (a : F) → K) ∘ P) y) (((⇑f : (a : F) → K) ∘ Q) z) -
            HMul.hMul (α := K) (((⇑f : (a : F) → K) ∘ Q) y) (((⇑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) (-HPow.hPow (β := ℕ) (P y * Q z - Q y * 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.Projective.addU
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
f : F →+* K
P Q : Fin 3 → F
⊢ -HPow.hPow (β := ℕ)
          (HMul.hMul (α := K) (((⇑f : (a : F) → K) ∘ P) y) (((⇑f : (a : F) → K) ∘ Q) z) -
            HMul.hMul (α := K) (((⇑f : (a : F) → K) ∘ Q) y) (((⇑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) (-HPow.hPow (β := ℕ) (P y * Q z - Q y * P z) 3 / (P z * Q z))

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

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective 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) (W'.map f).a₁ ((f : (a : R) → S) (W'.addX P Q) : S)) -
      HMul.hMul (β := S) (W'.map f).a₃ ((f : (a : R) → S) (W'.addZ P Q) : S) =
    (f : (a : R) → S) (-W'.negAddY P Q - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q)
⊢ (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.Projective.negY_eq, WeierstrassCurve.Projective.map_negAddY, WeierstrassCurve.Projective.map_addX, WeierstrassCurve.Projective.map_addZ, WeierstrassCurve.Projective.addY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective R
f : R →+* S
P Q : Fin 3 → R
⊢ HSub.hSub (α := S) (-(f : (a : R) → S) (W'.negAddY P Q) : S)
        (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) (W'.addX P Q) : S)) -
      HMul.hMul (β := S) (W'.map f).a₃ ((f : (a : R) → S) (W'.addZ P Q) : S) =
    (f : (a : R) → S) (-W'.negAddY P Q - W'.a₁ * W'.addX P Q - W'.a₃ * W'.addZ P Q)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Projective 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.Projective.map_addY, WeierstrassCurve.Projective.comp_fin3, WeierstrassCurve.Projective.map_addX, WeierstrassCurve.Projective.map_addZ, WeierstrassCurve.Projective.addXYZ
-- 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).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: RingHom.coe_coe, WeierstrassCurve.Projective.map_baseChange, WeierstrassCurve.Projective.map_negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
Goal:
R : Type r
S : Type s
F : Type u
K : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field F
inst_3 : Field K
W' : Projective R
inst_4 : Algebra R S
inst_5 : Algebra R F
inst_6 : Algebra S F
inst_7 : IsScalarTower R S F
inst_8 : Algebra R K
inst_9 : Algebra S K
inst_10 : IsScalarTower R S K
f : F →ₐ[S] K
P : Fin 3 → F
rw : (W'⁄K).dblU ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) = ((↑f : F →+* K) : (a : F) → K) ((W'⁄F).dblU P)
rw₁ :
  (W'⁄K).dblU ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) =
    ((W'⁄F).map (↑f : F →+* K)).dblU ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P)
rw₂ rw₃ : (W'⁄K).dblU ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) = (W'⁄K).dblU ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P)
⊢ (W'⁄K).dblU ((⇑f : (a : F) → K) ∘ P) = (f : (a : F) → K) ((W'⁄F).dblU P)

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

Premises used: RingHom.coe_coe, WeierstrassCurve.Projective.map_dblU, 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).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: WeierstrassCurve.Projective.map_dblZ, 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 : 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: RingHom.coe_coe, WeierstrassCurve.Projective.map_baseChange, WeierstrassCurve.Projective.map_dblX