awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Jacobian F
f : F →+* K
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
h : ¬P ≈ Q
neg : (W.map f).addXYZ ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q
neg₁ : (W.map f).addXYZ ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.addXYZ P Q
neg₂ neg₃ : Eq.{v + 1} (α := Fin 3 → K) ((⇑f : (a : F) → K) ∘ W.addXYZ P Q) ((⇑f : (a : F) → K) ∘ W.addXYZ P Q)
⊢ (W.map f).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ W.add P Q

Tactic:
rw [add_of_not_equiv <| h.comp (comp_equiv_comp f hP hQ).mp, add_of_not_equiv h, map_addXYZ]

Premises used: WeierstrassCurve.Jacobian.comp_equiv_comp, Function.comp, Iff.mp, WeierstrassCurve.Jacobian.add_of_not_equiv, WeierstrassCurve.Jacobian.map_addXYZ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (⇑(↑f : A →+* B) : (a : A) → B) ∘ (W'⁄A).neg P
rw₁ :
  (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) =
    ((W'⁄A).map (↑f : A →+* B)).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
rw₂ rw₃ : (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P) = (W'⁄B).neg ((⇑(↑f : A →+* B) : (a : A) → B) ∘ P)
⊢ (W'⁄B).neg ((⇑f : (a : A) → B) ∘ P) = (⇑f : (a : A) → B) ∘ (W'⁄A).neg P

Tactic:
rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_neg, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Jacobian.map_baseChange, WeierstrassCurve.Jacobian.map_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
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' : Jacobian 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 Q : Fin 3 → F
hP : (W'⁄F).Nonsingular P
hQ : (W'⁄F).Nonsingular Q
rw :
  (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
    (⇑(↑f : F →+* K) : (a : F) → K) ∘ (W'⁄F).add P Q
rw₁ :
  (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
    ((W'⁄F).map (↑f : F →+* K)).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q)
rw₂ rw₃ :
  (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q) =
    (W'⁄K).add ((⇑(↑f : F →+* K) : (a : F) → K) ∘ P) ((⇑(↑f : F →+* K) : (a : F) → K) ∘ Q)
⊢ (W'⁄K).add ((⇑f : (a : F) → K) ∘ P) ((⇑f : (a : F) → K) ∘ Q) = (⇑f : (a : F) → K) ∘ (W'⁄F).add P Q

Tactic:
rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_add _ hP hQ, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Jacobian.map_add, WeierstrassCurve.Jacobian.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
rw :
  HPow.hPow (β := ℕ)
        (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
          HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
        2 -
      24 *
        (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) +
          HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
            (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) =
    0
⊢ (ofJ0 R).c₄ = 0

Tactic:
rw [ofJ0, c₄, b₂, b₄]

Premises used: WeierstrassCurve.c₄, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.ofJ0
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
⊢ HPow.hPow (β := ℕ)
        (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
          HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
        2 -
      24 *
        (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) +
          HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
            (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) =
    0

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
rw :
  -HPow.hPow (β := ℕ)
                (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
                    2 +
                  HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
                2 *
            (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 *
                      a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } +
                    HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) *
                      a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } -
                  HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
                      (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) *
                    a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } +
                a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } *
                  HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
                    2 -
              HPow.hPow (α := R) (β := ℕ) (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2) -
          8 *
            HPow.hPow (β := ℕ)
              (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) +
                HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
                  (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
              3 -
        27 *
          HPow.hPow (β := ℕ)
            (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
              HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
            2 +
      9 *
            (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
              HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) *
          (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) +
            HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
              (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) *
        (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
          HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) =
    -27
⊢ (ofJ0 R).Δ = -27

Tactic:
rw [ofJ0, Δ, b₂, b₄, b₆, b₈]

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.b₈, WeierstrassCurve.ofJ0, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
⊢ -HPow.hPow (β := ℕ)
                (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
                    2 +
                  HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
                2 *
            (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 *
                      a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } +
                    HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) *
                      a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } -
                  HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
                      (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) *
                    a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } +
                a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R } *
                  HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
                    2 -
              HPow.hPow (α := R) (β := ℕ) (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2) -
          8 *
            HPow.hPow (β := ℕ)
              (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) +
                HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
                  (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
              3 -
        27 *
          HPow.hPow (β := ℕ)
            (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
              HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }))
            2 +
      9 *
            (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
              HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) *
          (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) +
            HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })
              (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) *
        (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R }) 2 +
          HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 1, a₄ := 0, a₆ := 0 : WeierstrassCurve R })) =
    -27

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
rw :
  HPow.hPow (β := ℕ)
        (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
          HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
        2 -
      24 *
        (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) +
          HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
            (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) =
    -48
⊢ (ofJ1728 R).c₄ = -48

Tactic:
rw [ofJ1728, c₄, b₂, b₄]

Premises used: WeierstrassCurve.ofJ1728, WeierstrassCurve.c₄, WeierstrassCurve.b₂, WeierstrassCurve.b₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
⊢ HPow.hPow (β := ℕ)
        (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
          HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
        2 -
      24 *
        (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) +
          HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
            (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) =
    -48

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
rw :
  -HPow.hPow (β := ℕ)
                (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
                    2 +
                  HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
                2 *
            (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 *
                      a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } +
                    HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) *
                      a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } -
                  HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
                      (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) *
                    a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } +
                a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } *
                  HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
                    2 -
              HPow.hPow (α := R) (β := ℕ) (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2) -
          8 *
            HPow.hPow (β := ℕ)
              (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) +
                HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
                  (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
              3 -
        27 *
          HPow.hPow (β := ℕ)
            (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
              HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
            2 +
      9 *
            (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
              HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) *
          (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) +
            HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
              (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) *
        (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
          HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) =
    -64
⊢ (ofJ1728 R).Δ = -64

Tactic:
rw [ofJ1728, Δ, b₂, b₄, b₆, b₈]

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.ofJ1728, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.b₈, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
⊢ -HPow.hPow (β := ℕ)
                (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
                    2 +
                  HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
                2 *
            (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 *
                      a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } +
                    HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) *
                      a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } -
                  HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
                      (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) *
                    a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } +
                a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R } *
                  HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
                    2 -
              HPow.hPow (α := R) (β := ℕ) (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2) -
          8 *
            HPow.hPow (β := ℕ)
              (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) +
                HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
                  (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
              3 -
        27 *
          HPow.hPow (β := ℕ)
            (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
              HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }))
            2 +
      9 *
            (HPow.hPow (α := R) (β := ℕ) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
              HMul.hMul (α := R) 4 (a₂ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) *
          (HMul.hMul (α := R) 2 (a₄ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) +
            HMul.hMul (α := R) (a₁ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })
              (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) *
        (HPow.hPow (α := R) (β := ℕ) (a₃ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R }) 2 +
          HMul.hMul (α := R) 4 (a₆ { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 1, a₆ := 0 : WeierstrassCurve R })) =
    -64

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
j : R
simp :
  HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (j - 1728) 2 + HMul.hMul (α := R) 4 0) 2 -
      24 * (2 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) + (j - 1728) * 0) =
    j * HPow.hPow (β := ℕ) (j - 1728) 3
⊢ (ofJNe0Or1728 j).c₄ = j * HPow.hPow (β := ℕ) (j - 1728) 3

Tactic:
simp only [ofJNe0Or1728, c₄, b₂, b₄]

Premises used: WeierstrassCurve.c₄, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.ofJNe0Or1728
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
j : R
⊢ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (j - 1728) 2 + HMul.hMul (α := R) 4 0) 2 -
      24 * (2 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) + (j - 1728) * 0) =
    j * HPow.hPow (β := ℕ) (j - 1728) 3

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
j : R
simp :
  -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (j - 1728) 2 + HMul.hMul (α := R) 4 0) 2 *
            (HPow.hPow (β := ℕ) (j - 1728) 2 * -HPow.hPow (β := ℕ) (j - 1728) 5 +
                    HMul.hMul (α := R) 4 0 * -HPow.hPow (β := ℕ) (j - 1728) 5 -
                  (j - 1728) * 0 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) +
                0 * HPow.hPow (α := R) (β := ℕ) 0 2 -
              HPow.hPow (β := ℕ) (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) 2) -
          8 * HPow.hPow (β := ℕ) (2 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) + (j - 1728) * 0) 3 -
        27 * HPow.hPow (β := ℕ) (HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * -HPow.hPow (β := ℕ) (j - 1728) 5) 2 +
      9 * (HPow.hPow (β := ℕ) (j - 1728) 2 + HMul.hMul (α := R) 4 0) *
          (2 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) + (j - 1728) * 0) *
        (HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * -HPow.hPow (β := ℕ) (j - 1728) 5) =
    HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9
⊢ (ofJNe0Or1728 j).Δ = HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9

Tactic:
simp only [ofJNe0Or1728, Δ, b₂, b₄, b₆, b₈]

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.ofJNe0Or1728, WeierstrassCurve.b₈, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
j : R
⊢ -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (j - 1728) 2 + HMul.hMul (α := R) 4 0) 2 *
            (HPow.hPow (β := ℕ) (j - 1728) 2 * -HPow.hPow (β := ℕ) (j - 1728) 5 +
                    HMul.hMul (α := R) 4 0 * -HPow.hPow (β := ℕ) (j - 1728) 5 -
                  (j - 1728) * 0 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) +
                0 * HPow.hPow (α := R) (β := ℕ) 0 2 -
              HPow.hPow (β := ℕ) (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) 2) -
          8 * HPow.hPow (β := ℕ) (2 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) + (j - 1728) * 0) 3 -
        27 * HPow.hPow (β := ℕ) (HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * -HPow.hPow (β := ℕ) (j - 1728) 5) 2 +
      9 * (HPow.hPow (β := ℕ) (j - 1728) 2 + HMul.hMul (α := R) 4 0) *
          (2 * (-36 * HPow.hPow (β := ℕ) (j - 1728) 3) + (j - 1728) * 0) *
        (HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * -HPow.hPow (β := ℕ) (j - 1728) 5) =
    HPow.hPow (β := ℕ) j 2 * HPow.hPow (β := ℕ) (j - 1728) 9

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j : R
inst_1 : W.IsElliptic
hu : Fact (IsUnit.{u_1} (M := R) 3)
rw : IsUnit.{u_1} (M := R) (-27)
⊢ (ofJ0 R).IsElliptic

Tactic:
rw [isElliptic_iff, ofJ0_Δ]

Premises used: WeierstrassCurve.ofJ0_Δ, WeierstrassCurve.isElliptic_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j : R
inst_1 : W.IsElliptic
hu : Fact (IsUnit.{u_1} (M := R) 3)
⊢ IsUnit (-HPow.hPow (α := R) (β := ℕ) 3 3)

Tactic:
(hu.out.pow 3).neg

Premises used: IsUnit.pow, IsUnit.neg, OfNat.ofNat, Fact.out
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j : R
inst_1 : W.IsElliptic
hu : Fact (IsUnit.{u_1} (M := R) 3)
h : 27 = HPow.hPow (α := R) (β := ℕ) 3 3
⊢ IsUnit.{u_1} (M := R) (-27)

Tactic:
convert! (hu.out.pow 3).neg

Premises used: IsUnit.pow, IsUnit.neg, OfNat.ofNat, Fact.out
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j : R
inst_1 : W.IsElliptic
hu : Fact (IsUnit.{u_1} (M := R) 3)
⊢ 27 = HPow.hPow (α := R) (β := ℕ) 3 3

Tactic:
norm_num1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (IsUnit.{u_1} (M := R) 3)
rw : (↑(ofJ0 R).Δ'⁻¹ : R) * HPow.hPow (α := R) (β := ℕ) 0 3 = 0
⊢ (ofJ0 R).j = 0

Tactic:
rw [j, ofJ0_c₄]

Premises used: WeierstrassCurve.j, WeierstrassCurve.ofJ0_c₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fact (IsUnit.{u_1} (M := R) 3)
⊢ (↑(ofJ0 R).Δ'⁻¹ : R) * HPow.hPow (α := R) (β := ℕ) 0 3 = 0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j : R
inst_1 : W.IsElliptic
hu : Fact (IsUnit.{u_1} (M := R) 2)
rw : IsUnit.{u_1} (M := R) (-64)
⊢ (ofJ1728 R).IsElliptic

Tactic:
rw [isElliptic_iff, ofJ1728_Δ]

Premises used: WeierstrassCurve.isElliptic_iff, WeierstrassCurve.ofJ1728_Δ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
j : R
inst_1 : W.IsElliptic
hu : Fact (IsUnit.{u_1} (M := R) 2)
⊢ IsUnit (-HPow.hPow (α := R) (β := ℕ) 2 6)

Tactic:
(hu.out.pow 6).neg

Premises used: IsUnit.pow, IsUnit.neg, OfNat.ofNat, Fact.out