awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
rw :
  HPow.hPow (α := R) (β := ℕ) 0 2 * W.a₆ + 4 * W.a₂ * W.a₆ - HMul.hMul (α := R) 0 0 * W.a₄ +
        W.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 -
      HPow.hPow (β := ℕ) W.a₄ 2 =
    4 * W.a₂ * W.a₆ - HPow.hPow (β := ℕ) W.a₄ 2
⊢ W.b₈ = 4 * W.a₂ * W.a₆ - HPow.hPow (β := ℕ) W.a₄ 2

Tactic:
rw [b₈, a₁_of_isCharNeTwoNF, a₃_of_isCharNeTwoNF]

Premises used: WeierstrassCurve.a₁_of_isCharNeTwoNF, WeierstrassCurve.a₃_of_isCharNeTwoNF, WeierstrassCurve.b₈
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ HPow.hPow (α := R) (β := ℕ) 0 2 * W.a₆ + 4 * W.a₂ * W.a₆ - HMul.hMul (α := R) 0 0 * W.a₄ +
        W.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 -
      HPow.hPow (β := ℕ) W.a₄ 2 =
    4 * W.a₂ * W.a₆ - HPow.hPow (β := ℕ) W.a₄ 2

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
rw : HPow.hPow (β := ℕ) (4 * W.a₂) 2 - 24 * (2 * W.a₄) = 16 * HPow.hPow (β := ℕ) W.a₂ 2 - 48 * W.a₄
⊢ W.c₄ = 16 * HPow.hPow (β := ℕ) W.a₂ 2 - 48 * W.a₄

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

Premises used: WeierstrassCurve.b₂_of_isCharNeTwoNF, WeierstrassCurve.c₄, WeierstrassCurve.b₄_of_isCharNeTwoNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ HPow.hPow (β := ℕ) (4 * W.a₂) 2 - 24 * (2 * W.a₄) = 16 * HPow.hPow (β := ℕ) W.a₂ 2 - 48 * W.a₄

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
rw :
  -HPow.hPow (β := ℕ) (4 * W.a₂) 3 + 36 * (4 * W.a₂) * (2 * W.a₄) - 216 * (4 * W.a₆) =
    -64 * HPow.hPow (β := ℕ) W.a₂ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆
⊢ W.c₆ = -64 * HPow.hPow (β := ℕ) W.a₂ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆

Tactic:
rw [c₆, b₂_of_isCharNeTwoNF, b₄_of_isCharNeTwoNF, b₆_of_isCharNeTwoNF]

Premises used: WeierstrassCurve.b₂_of_isCharNeTwoNF, WeierstrassCurve.b₆_of_isCharNeTwoNF, WeierstrassCurve.c₆, WeierstrassCurve.b₄_of_isCharNeTwoNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ -HPow.hPow (β := ℕ) (4 * W.a₂) 3 + 36 * (4 * W.a₂) * (2 * W.a₄) - 216 * (4 * W.a₆) =
    -64 * HPow.hPow (β := ℕ) W.a₂ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
rw :
  -HPow.hPow (β := ℕ) (4 * W.a₂) 2 * (4 * W.a₂ * W.a₆ - HPow.hPow (β := ℕ) W.a₄ 2) -
          8 * HPow.hPow (β := ℕ) (2 * W.a₄) 3 -
        27 * HPow.hPow (β := ℕ) (4 * W.a₆) 2 +
      9 * (4 * W.a₂) * (2 * W.a₄) * (4 * W.a₆) =
    -64 * HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ + 16 * HPow.hPow (β := ℕ) W.a₂ 2 * HPow.hPow (β := ℕ) W.a₄ 2 -
          64 * HPow.hPow (β := ℕ) W.a₄ 3 -
        432 * HPow.hPow (β := ℕ) W.a₆ 2 +
      288 * W.a₂ * W.a₄ * W.a₆
⊢ W.Δ =
    -64 * HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ + 16 * HPow.hPow (β := ℕ) W.a₂ 2 * HPow.hPow (β := ℕ) W.a₄ 2 -
          64 * HPow.hPow (β := ℕ) W.a₄ 3 -
        432 * HPow.hPow (β := ℕ) W.a₆ 2 +
      288 * W.a₂ * W.a₄ * W.a₆

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

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.b₈_of_isCharNeTwoNF, WeierstrassCurve.b₂_of_isCharNeTwoNF, WeierstrassCurve.b₆_of_isCharNeTwoNF, WeierstrassCurve.b₄_of_isCharNeTwoNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharNeTwoNF
⊢ -HPow.hPow (β := ℕ) (4 * W.a₂) 2 * (4 * W.a₂ * W.a₆ - HPow.hPow (β := ℕ) W.a₄ 2) -
          8 * HPow.hPow (β := ℕ) (2 * W.a₄) 3 -
        27 * HPow.hPow (β := ℕ) (4 * W.a₆) 2 +
      9 * (4 * W.a₂) * (2 * W.a₄) * (4 * W.a₆) =
    -64 * HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ + 16 * HPow.hPow (β := ℕ) W.a₂ 2 * HPow.hPow (β := ℕ) W.a₄ 2 -
          64 * HPow.hPow (β := ℕ) W.a₄ 3 -
        432 * HPow.hPow (β := ℕ) W.a₆ 2 +
      288 * W.a₂ * W.a₄ * W.a₆

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
a₁ : (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₁ = 0
a₃ : (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₃ = 0
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).IsCharNeTwoNF

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₁ = 0

Tactic:
simp [variableChange_a₁, variableChange_a₃]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.variableChange_a₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₃ = 0

Tactic:
simp [variableChange_a₁, variableChange_a₃]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.variableChange_a₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Invertible (α := R) 2
⊢ ∃ (C : VariableChange R), (C • W).IsCharNeTwoNF

Tactic:
⟨_, W.toCharNeTwoNF_spec⟩

Premises used: WeierstrassCurve.toCharNeTwoNF_spec, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : W.IsShortNF
⊢ W.IsCharNeTwoNF

Tactic:
⟨IsShortNF.a₁, IsShortNF.a₃⟩

Premises used: WeierstrassCurve.IsShortNF.a₃, WeierstrassCurve.IsCharNeTwoNF.mk, WeierstrassCurve.IsShortNF.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
⊢ W.a₁ = 0

Tactic:
IsShortNF.a₁

Premises used: WeierstrassCurve.IsShortNF.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
⊢ W.a₂ = 0

Tactic:
IsShortNF.a₂

Premises used: WeierstrassCurve.IsShortNF.a₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
⊢ W.a₃ = 0

Tactic:
IsShortNF.a₃

Premises used: WeierstrassCurve.IsShortNF.a₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
⊢ W.b₂ = 0

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
⊢ W.b₄ = 2 * W.a₄

Tactic:
W.b₄_of_isCharNeTwoNF

Premises used: WeierstrassCurve.b₄_of_isCharNeTwoNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
⊢ W.b₆ = 4 * W.a₆

Tactic:
W.b₆_of_isCharNeTwoNF

Premises used: WeierstrassCurve.b₆_of_isCharNeTwoNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
⊢ W.b₈ = -HPow.hPow (β := ℕ) W.a₄ 2

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
⊢ W.c₄ = -48 * W.a₄

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
⊢ W.c₆ = -864 * W.a₆

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
rw :
  -64 * HPow.hPow (α := R) (β := ℕ) 0 3 * W.a₆ + 16 * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) W.a₄ 2 -
          64 * HPow.hPow (β := ℕ) W.a₄ 3 -
        432 * HPow.hPow (β := ℕ) W.a₆ 2 +
      HMul.hMul (α := R) 288 0 * W.a₄ * W.a₆ =
    -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2)
⊢ W.Δ = -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2)

Tactic:
rw [Δ_of_isCharNeTwoNF, a₂_of_isShortNF]

Premises used: WeierstrassCurve.Δ_of_isCharNeTwoNF, WeierstrassCurve.a₂_of_isShortNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
⊢ -64 * HPow.hPow (α := R) (β := ℕ) 0 3 * W.a₆ + 16 * HPow.hPow (α := R) (β := ℕ) 0 2 * HPow.hPow (β := ℕ) W.a₄ 2 -
          64 * HPow.hPow (β := ℕ) W.a₄ 3 -
        432 * HPow.hPow (β := ℕ) W.a₆ 2 +
      HMul.hMul (α := R) 288 0 * W.a₄ * W.a₆ =
    -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
rw : 2 * W.a₄ = -W.a₄
⊢ W.b₄ = -W.a₄

Tactic:
rw [b₄_of_isShortNF]

Premises used: WeierstrassCurve.b₄_of_isShortNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
⊢ 2 * W.a₄ = -W.a₄

Tactic:
linear_combination W.a₄ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₄, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
rw : 4 * W.a₆ = W.a₆
⊢ W.b₆ = W.a₆

Tactic:
rw [b₆_of_isShortNF]

Premises used: WeierstrassCurve.b₆_of_isShortNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
⊢ 4 * W.a₆ = W.a₆

Tactic:
linear_combination W.a₆ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₆, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
rw : -48 * W.a₄ = 0
⊢ W.c₄ = 0

Tactic:
rw [c₄_of_isShortNF]

Premises used: WeierstrassCurve.c₄_of_isShortNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
⊢ -48 * W.a₄ = 0

Tactic:
linear_combination -16 * W.a₄ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₄, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
rw : -864 * W.a₆ = 0
⊢ W.c₆ = 0

Tactic:
rw [c₆_of_isShortNF]

Premises used: WeierstrassCurve.c₆_of_isShortNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
⊢ -864 * W.a₆ = 0

Tactic:
linear_combination -288 * W.a₆ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₆, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
rw : -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2) = -HPow.hPow (β := ℕ) W.a₄ 3
⊢ W.Δ = -HPow.hPow (β := ℕ) W.a₄ 3

Tactic:
rw [Δ_of_isShortNF]

Premises used: WeierstrassCurve.Δ_of_isShortNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsShortNF
inst_2 : CharP R 3
⊢ -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2) = -HPow.hPow (β := ℕ) W.a₄ 3

Tactic:
linear_combination (-21 * W.a₄ ^ 3 - 144 * W.a₆ ^ 2) * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, HMul.hMul, HSub.hSub, HPow.hPow, WeierstrassCurve.a₆, WeierstrassCurve.a₄, OfNat.ofNat, Neg.neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsShortNF
⊢ (↑W.Δ' : F) ≠ 0

Tactic:
have h := W.Δ'.ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsShortNF
h : (↑W.Δ' : F) ≠ 0
⊢ -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2) ≠ 0

Tactic:
rw [coe_Δ', Δ_of_isShortNF] at h

Premises used: WeierstrassCurve.Δ_of_isShortNF, WeierstrassCurve.coe_Δ'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsShortNF
h : -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2) ≠ 0
rw :
  HPow.hPow (β := ℕ) (-48 * W.a₄) 3 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2) =
    6912 * HPow.hPow (β := ℕ) W.a₄ 3 * (-16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2))
⊢ W.j = 6912 * HPow.hPow (β := ℕ) W.a₄ 3 / (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2)

Tactic:
rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isShortNF, Δ_of_isShortNF, div_eq_div_iff h (right_ne_zero_of_mul h)]

Premises used: WeierstrassCurve.j, Units.val_inv_eq_inv_val, WeierstrassCurve.Δ_of_isShortNF, right_ne_zero_of_mul, div_eq_div_iff, WeierstrassCurve.c₄_of_isShortNF, WeierstrassCurve.coe_Δ', div_eq_inv_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsShortNF
h : -16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2) ≠ 0
⊢ HPow.hPow (β := ℕ) (-48 * W.a₄) 3 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2) =
    6912 * HPow.hPow (β := ℕ) W.a₄ 3 * (-16 * (4 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.a₆ 2))

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsShortNF
inst_3 : CharP F 3
rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (α := F) (β := ℕ) 0 3 = 0
⊢ W.j = 0

Tactic:
rw [j, c₄_of_isShortNF_of_char_three]

Premises used: WeierstrassCurve.j, WeierstrassCurve.c₄_of_isShortNF_of_char_three
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsShortNF
inst_3 : CharP F 3
⊢ (↑W.Δ'⁻¹ : F) * HPow.hPow (α := F) (β := ℕ) 0 3 = 0

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
inst_3 : Invertible (α := R) 3
rw :
  (HSMul.hSMul (α := VariableChange R)
      { u := 1,
        r :=
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
            -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
        s := 0, t := 0 : VariableChange R }
      (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).IsShortNF
⊢ (HSMul.hSMul (α := VariableChange R) W.toShortNF W).IsShortNF

Tactic:
rw [toShortNF, mul_smul]

Premises used: SemigroupAction.mul_smul, WeierstrassCurve.toShortNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
inst_3 : Invertible (α := R) 3
a₁ :
  (HSMul.hSMul (α := VariableChange R)
        { u := 1,
          r :=
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
              -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
          s := 0, t := 0 : VariableChange R }
        (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₁ =
    0
a₂ :
  (HSMul.hSMul (α := VariableChange R)
        { u := 1,
          r :=
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
              -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
          s := 0, t := 0 : VariableChange R }
        (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₂ =
    0
a₃ :
  (HSMul.hSMul (α := VariableChange R)
        { u := 1,
          r :=
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
              -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
          s := 0, t := 0 : VariableChange R }
        (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₃ =
    0
⊢ (HSMul.hSMul (α := VariableChange R)
      { u := 1,
        r :=
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
            -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
        s := 0, t := 0 : VariableChange R }
      (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).IsShortNF

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
inst_3 : Invertible (α := R) 3
⊢ (HSMul.hSMul (α := VariableChange R)
        { u := 1,
          r :=
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
              -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
          s := 0, t := 0 : VariableChange R }
        (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₁ =
    0

Tactic:
simp [variableChange_a₁, variableChange_a₂, variableChange_a₃]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.variableChange_a₂, WeierstrassCurve.variableChange_a₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
inst_3 : Invertible (α := R) 3
⊢ (HSMul.hSMul (α := VariableChange R)
        { u := 1,
          r :=
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
              -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
          s := 0, t := 0 : VariableChange R }
        (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₂ =
    0

Tactic:
simp [variableChange_a₁, variableChange_a₂, variableChange_a₃]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.variableChange_a₂, WeierstrassCurve.variableChange_a₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : Invertible (α := R) 2
inst_3 : Invertible (α := R) 3
⊢ (HSMul.hSMul (α := VariableChange R)
        { u := 1,
          r :=
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 3 _ *
              -(HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).a₂,
          s := 0, t := 0 : VariableChange R }
        (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W)).a₃ =
    0

Tactic:
simp [variableChange_a₁, variableChange_a₂, variableChange_a₃]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.variableChange_a₂, WeierstrassCurve.variableChange_a₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Invertible (α := R) 2
inst_2 : Invertible (α := R) 3
⊢ ∃ (C : VariableChange R), (C • W).IsShortNF

Tactic:
⟨_, W.toShortNF_spec⟩

Premises used: WeierstrassCurve.toShortNF_spec, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W : WeierstrassCurve R
inst_2 : W.IsCharThreeJNeZeroNF
⊢ W.IsCharNeTwoNF

Tactic:
⟨IsCharThreeJNeZeroNF.a₁, IsCharThreeJNeZeroNF.a₃⟩

Premises used: WeierstrassCurve.IsCharNeTwoNF.mk, WeierstrassCurve.IsCharThreeJNeZeroNF.a₁, WeierstrassCurve.IsCharThreeJNeZeroNF.a₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
⊢ W.a₁ = 0

Tactic:
IsCharThreeJNeZeroNF.a₁

Premises used: WeierstrassCurve.IsCharThreeJNeZeroNF.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
⊢ W.a₃ = 0

Tactic:
IsCharThreeJNeZeroNF.a₃

Premises used: WeierstrassCurve.IsCharThreeJNeZeroNF.a₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
⊢ W.a₄ = 0

Tactic:
IsCharThreeJNeZeroNF.a₄

Premises used: WeierstrassCurve.IsCharThreeJNeZeroNF.a₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
⊢ W.b₂ = 4 * W.a₂

Tactic:
W.b₂_of_isCharNeTwoNF

Premises used: WeierstrassCurve.b₂_of_isCharNeTwoNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
⊢ W.b₄ = 0

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
⊢ W.b₆ = 4 * W.a₆

Tactic:
W.b₆_of_isCharNeTwoNF

Premises used: WeierstrassCurve.b₆_of_isCharNeTwoNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
⊢ W.b₈ = 4 * W.a₂ * W.a₆

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
⊢ W.c₄ = 16 * HPow.hPow (β := ℕ) W.a₂ 2

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
⊢ W.c₆ = -64 * HPow.hPow (β := ℕ) W.a₂ 3 - 864 * W.a₆

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
⊢ W.Δ = -64 * HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ - 432 * HPow.hPow (β := ℕ) W.a₆ 2

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
rw : 4 * W.a₂ = W.a₂
⊢ W.b₂ = W.a₂

Tactic:
rw [b₂_of_isCharThreeJNeZeroNF]

Premises used: WeierstrassCurve.b₂_of_isCharThreeJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
⊢ 4 * W.a₂ = W.a₂

Tactic:
linear_combination W.a₂ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₂, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
rw : 4 * W.a₆ = W.a₆
⊢ W.b₆ = W.a₆

Tactic:
rw [b₆_of_isCharThreeJNeZeroNF]

Premises used: WeierstrassCurve.b₆_of_isCharThreeJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
⊢ 4 * W.a₆ = W.a₆

Tactic:
linear_combination W.a₆ * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₆, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
rw : 4 * W.a₂ * W.a₆ = W.a₂ * W.a₆
⊢ W.b₈ = W.a₂ * W.a₆

Tactic:
rw [b₈_of_isCharThreeJNeZeroNF]

Premises used: WeierstrassCurve.b₈_of_isCharThreeJNeZeroNF