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.IsCharTwoJNeZeroNF
⊢ HPow.hPow (α := R) (β := ℕ) 1 2 * W.a₆ + 4 * W.a₂ * W.a₆ - HMul.hMul (α := R) 1 0 * 0 +
        W.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 -
      HPow.hPow (α := R) (β := ℕ) 0 2 =
    W.a₆ + 4 * W.a₂ * W.a₆

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
rw : HPow.hPow (β := ℕ) W.b₂ 2 - HMul.hMul (α := R) 24 0 = HPow.hPow (β := ℕ) W.b₂ 2
⊢ W.c₄ = HPow.hPow (β := ℕ) W.b₂ 2

Tactic:
rw [c₄, b₄_of_isCharTwoJNeZeroNF]

Premises used: WeierstrassCurve.c₄, WeierstrassCurve.b₄_of_isCharTwoJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
⊢ HPow.hPow (β := ℕ) W.b₂ 2 - HMul.hMul (α := R) 24 0 = HPow.hPow (β := ℕ) W.b₂ 2

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

Tactic:
rw [c₆, b₄_of_isCharTwoJNeZeroNF, b₆_of_isCharTwoJNeZeroNF]

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

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
inst_2 : CharP R 2
rw : 1 + 4 * W.a₂ = 1
⊢ W.b₂ = 1

Tactic:
rw [b₂_of_isCharTwoJNeZeroNF]

Premises used: WeierstrassCurve.b₂_of_isCharTwoJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
inst_2 : CharP R 2
⊢ 1 + 4 * W.a₂ = 1

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

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.IsCharTwoJNeZeroNF
inst_2 : CharP R 2
rw : 4 * W.a₆ = 0
⊢ W.b₆ = 0

Tactic:
rw [b₆_of_isCharTwoJNeZeroNF]

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

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

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.IsCharTwoJNeZeroNF
inst_2 : CharP R 2
rw : W.a₆ + 4 * W.a₂ * W.a₆ = W.a₆
⊢ W.b₈ = W.a₆

Tactic:
rw [b₈_of_isCharTwoJNeZeroNF]

Premises used: WeierstrassCurve.b₈_of_isCharTwoJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
inst_2 : CharP R 2
⊢ W.a₆ + 4 * W.a₂ * W.a₆ = W.a₆

Tactic:
linear_combination 2 * W.a₂ * W.a₆ * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₂, WeierstrassCurve.a₆, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
inst_2 : CharP R 2
rw : HPow.hPow (α := R) (β := ℕ) 1 2 = 1
⊢ W.c₄ = 1

Tactic:
rw [c₄_of_isCharTwoJNeZeroNF, b₂_of_isCharTwoJNeZeroNF_of_char_two]

Premises used: WeierstrassCurve.c₄_of_isCharTwoJNeZeroNF, WeierstrassCurve.b₂_of_isCharTwoJNeZeroNF_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
inst_2 : CharP R 2
⊢ HPow.hPow (α := R) (β := ℕ) 1 2 = 1

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
inst_2 : CharP R 2
rw : -HPow.hPow (α := R) (β := ℕ) 1 3 - 864 * W.a₆ = 1
⊢ W.c₆ = 1

Tactic:
rw [c₆_of_isCharTwoJNeZeroNF, b₂_of_isCharTwoJNeZeroNF_of_char_two]

Premises used: WeierstrassCurve.c₆_of_isCharTwoJNeZeroNF, WeierstrassCurve.b₂_of_isCharTwoJNeZeroNF_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
inst_2 : CharP R 2
⊢ -HPow.hPow (α := R) (β := ℕ) 1 3 - 864 * W.a₆ = 1

Tactic:
linear_combination (-1 - 432 * W.a₆) * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, HMul.hMul, HSub.hSub, WeierstrassCurve.a₆, OfNat.ofNat, Neg.neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
inst_2 : CharP R 2
rw :
  -HPow.hPow (α := R) (β := ℕ) 1 2 * W.a₆ - 8 * HPow.hPow (α := R) (β := ℕ) 0 3 - 27 * HPow.hPow (α := R) (β := ℕ) 0 2 +
      HMul.hMul (α := R) 9 1 * 0 * 0 =
    W.a₆
⊢ W.Δ = W.a₆

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

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.b₆_of_isCharTwoJNeZeroNF_of_char_two, WeierstrassCurve.b₈_of_isCharTwoJNeZeroNF_of_char_two, WeierstrassCurve.b₂_of_isCharTwoJNeZeroNF_of_char_two, WeierstrassCurve.b₄_of_isCharTwoJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
inst_2 : CharP R 2
⊢ -HPow.hPow (α := R) (β := ℕ) 1 2 * W.a₆ - 8 * HPow.hPow (α := R) (β := ℕ) 0 3 - 27 * HPow.hPow (α := R) (β := ℕ) 0 2 +
      HMul.hMul (α := R) 9 1 * 0 * 0 =
    W.a₆

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

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₆, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
rw₁ : (↑W.Δ' : F)⁻¹ * HPow.hPow (β := ℕ) W.c₄ 3 = 1 / W.a₆
rw₂ : HPow.hPow (β := ℕ) W.c₄ 3 / (↑W.Δ' : F) = 1 / W.a₆
rw₃ : HPow.hPow (β := ℕ) W.c₄ 3 / W.Δ = 1 / W.a₆
rw₄ : HPow.hPow (α := F) (β := ℕ) 1 3 / W.Δ = 1 / W.a₆
rw₅ : HPow.hPow (α := F) (β := ℕ) 1 3 / W.a₆ = 1 / W.a₆
rw₆ rw₇ : 1 / W.a₆ = 1 / W.a₆
⊢ W.j = 1 / W.a₆

Tactic:
rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharTwoJNeZeroNF_of_char_two, Δ_of_isCharTwoJNeZeroNF_of_char_two, one_pow]

Premises used: one_pow, WeierstrassCurve.j, Units.val_inv_eq_inv_val, WeierstrassCurve.coe_Δ', WeierstrassCurve.Δ_of_isCharTwoJNeZeroNF_of_char_two, div_eq_inv_mul, WeierstrassCurve.c₄_of_isCharTwoJNeZeroNF_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
rw : Ne.{u_2 + 1} (α := F) 1 0 ∧ W.a₆ ≠ 0
⊢ W.j ≠ 0

Tactic:
rw [j_of_isCharTwoJNeZeroNF_of_char_two, div_ne_zero_iff]

Premises used: div_ne_zero_iff, WeierstrassCurve.j_of_isCharTwoJNeZeroNF_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
⊢ (↑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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
h : (↑W.Δ' : F) ≠ 0
⊢ W.a₆ ≠ 0

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

Premises used: WeierstrassCurve.coe_Δ', WeierstrassCurve.Δ_of_isCharTwoJNeZeroNF_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
h : W.a₆ ≠ 0
⊢ Ne.{u_2 + 1} (α := F) 1 0 ∧ W.a₆ ≠ 0

Tactic:
⟨one_ne_zero, h⟩

Premises used: And.intro, one_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.IsCharTwoJNeZeroNF
inst_3 : CharP F 2
h : W.a₆ ≠ 0
⊢ Ne.{u_2 + 1} (α := F) 1 0 ∧ W.a₆ ≠ 0

Tactic:
exact ⟨one_ne_zero, h⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
⊢ W.a₁ = 0

Tactic:
IsCharTwoJEqZeroNF.a₁

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

Tactic:
IsCharTwoJEqZeroNF.a₂

Premises used: WeierstrassCurve.IsCharTwoJEqZeroNF.a₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
rw : HPow.hPow (α := R) (β := ℕ) 0 2 + HMul.hMul (α := R) 4 0 = 0
⊢ W.b₂ = 0

Tactic:
rw [b₂, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]

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

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
rw : 2 * W.a₄ + 0 * W.a₃ = 2 * W.a₄
⊢ W.b₄ = 2 * W.a₄

Tactic:
rw [b₄, a₁_of_isCharTwoJEqZeroNF]

Premises used: WeierstrassCurve.b₄, WeierstrassCurve.a₁_of_isCharTwoJEqZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
⊢ 2 * W.a₄ + 0 * W.a₃ = 2 * W.a₄

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
rw :
  HPow.hPow (α := R) (β := ℕ) 0 2 * W.a₆ + HMul.hMul (α := R) 4 0 * W.a₆ - 0 * W.a₃ * W.a₄ +
        0 * HPow.hPow (β := ℕ) W.a₃ 2 -
      HPow.hPow (β := ℕ) W.a₄ 2 =
    -HPow.hPow (β := ℕ) W.a₄ 2
⊢ W.b₈ = -HPow.hPow (β := ℕ) W.a₄ 2

Tactic:
rw [b₈, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]

Premises used: WeierstrassCurve.b₈, WeierstrassCurve.a₁_of_isCharTwoJEqZeroNF, WeierstrassCurve.a₂_of_isCharTwoJEqZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
⊢ HPow.hPow (α := R) (β := ℕ) 0 2 * W.a₆ + HMul.hMul (α := R) 4 0 * W.a₆ - 0 * W.a₃ * W.a₄ +
        0 * HPow.hPow (β := ℕ) W.a₃ 2 -
      HPow.hPow (β := ℕ) W.a₄ 2 =
    -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.IsCharTwoJEqZeroNF
rw : HPow.hPow (α := R) (β := ℕ) 0 2 - 24 * (2 * W.a₄) = -48 * W.a₄
⊢ W.c₄ = -48 * W.a₄

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

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

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
rw : -HPow.hPow (α := R) (β := ℕ) 0 3 + HMul.hMul (α := R) 36 0 * (2 * W.a₄) - 216 * W.b₆ = -216 * W.b₆
⊢ W.c₆ = -216 * W.b₆

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

Premises used: WeierstrassCurve.c₆, WeierstrassCurve.b₄_of_isCharTwoJEqZeroNF, WeierstrassCurve.b₂_of_isCharTwoJEqZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
⊢ -HPow.hPow (α := R) (β := ℕ) 0 3 + HMul.hMul (α := R) 36 0 * (2 * W.a₄) - 216 * W.b₆ = -216 * W.b₆

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
rw :
  -HPow.hPow (α := R) (β := ℕ) 0 2 * W.b₈ - 8 * HPow.hPow (β := ℕ) (2 * W.a₄) 3 - 27 * HPow.hPow (β := ℕ) W.b₆ 2 +
      HMul.hMul (α := R) 9 0 * (2 * W.a₄) * W.b₆ =
    -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2)
⊢ W.Δ = -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2)

Tactic:
rw [Δ, b₂_of_isCharTwoJEqZeroNF, b₄_of_isCharTwoJEqZeroNF]

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.b₄_of_isCharTwoJEqZeroNF, WeierstrassCurve.b₂_of_isCharTwoJEqZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
⊢ -HPow.hPow (α := R) (β := ℕ) 0 2 * W.b₈ - 8 * HPow.hPow (β := ℕ) (2 * W.a₄) 3 - 27 * HPow.hPow (β := ℕ) W.b₆ 2 +
      HMul.hMul (α := R) 9 0 * (2 * W.a₄) * W.b₆ =
    -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2)

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

Tactic:
rw [b₄_of_isCharTwoJEqZeroNF]

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

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

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.IsCharTwoJEqZeroNF
inst_2 : CharP R 2
rw : -HPow.hPow (β := ℕ) W.a₄ 2 = HPow.hPow (β := ℕ) W.a₄ 2
⊢ W.b₈ = HPow.hPow (β := ℕ) W.a₄ 2

Tactic:
rw [b₈_of_isCharTwoJEqZeroNF]

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

Tactic:
linear_combination -W.a₄ ^ 2 * CharP.cast_eq_zero R 2

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.IsCharTwoJEqZeroNF
inst_2 : CharP R 2
rw : -48 * W.a₄ = 0
⊢ W.c₄ = 0

Tactic:
rw [c₄_of_isCharTwoJEqZeroNF]

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

Tactic:
linear_combination -24 * W.a₄ * CharP.cast_eq_zero R 2

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.IsCharTwoJEqZeroNF
inst_2 : CharP R 2
rw : -216 * W.b₆ = 0
⊢ W.c₆ = 0

Tactic:
rw [c₆_of_isCharTwoJEqZeroNF]

Premises used: WeierstrassCurve.c₆_of_isCharTwoJEqZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
inst_2 : CharP R 2
⊢ -216 * W.b₆ = 0

Tactic:
linear_combination -108 * W.b₆ * CharP.cast_eq_zero R 2

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

Tactic:
rw [Δ_of_isCharTwoJEqZeroNF, b₆_of_char_two]

Premises used: WeierstrassCurve.Δ_of_isCharTwoJEqZeroNF, WeierstrassCurve.b₆_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJEqZeroNF
inst_2 : CharP R 2
⊢ -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₃ 2) 2) = HPow.hPow (β := ℕ) W.a₃ 4

Tactic:
linear_combination (-32 * W.a₄ ^ 3 - 14 * W.a₃ ^ 4) * CharP.cast_eq_zero R 2

Premises used: CharP.cast_eq_zero, HMul.hMul, HSub.hSub, WeierstrassCurve.a₃, HPow.hPow, 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.IsCharTwoJEqZeroNF
⊢ (↑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.IsCharTwoJEqZeroNF
h : (↑W.Δ' : F) ≠ 0
⊢ -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2) ≠ 0

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

Premises used: WeierstrassCurve.Δ_of_isCharTwoJEqZeroNF, 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.IsCharTwoJEqZeroNF
h : -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2) ≠ 0
rw :
  HPow.hPow (β := ℕ) (-48 * W.a₄) 3 * (64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2) =
    110592 * HPow.hPow (β := ℕ) W.a₄ 3 * -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2)
⊢ W.j = 110592 * HPow.hPow (β := ℕ) W.a₄ 3 / (64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2)

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

Premises used: WeierstrassCurve.Δ_of_isCharTwoJEqZeroNF, WeierstrassCurve.j, Units.val_inv_eq_inv_val, div_eq_div_iff, WeierstrassCurve.coe_Δ', Iff.mp, neg_ne_zero, WeierstrassCurve.c₄_of_isCharTwoJEqZeroNF, 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.IsCharTwoJEqZeroNF
h : -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2) ≠ 0
⊢ HPow.hPow (β := ℕ) (-48 * W.a₄) 3 * (64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 2) =
    110592 * HPow.hPow (β := ℕ) W.a₄ 3 * -(64 * HPow.hPow (β := ℕ) W.a₄ 3 + 27 * HPow.hPow (β := ℕ) W.b₆ 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.IsCharTwoJEqZeroNF
inst_3 : CharP F 2
rw : (↑W.Δ'⁻¹ : F) * HPow.hPow (α := F) (β := ℕ) 0 3 = 0
⊢ W.j = 0

Tactic:
rw [j, c₄_of_isCharTwoJEqZeroNF_of_char_two]

Premises used: WeierstrassCurve.j, WeierstrassCurve.c₄_of_isCharTwoJEqZeroNF_of_char_two
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
W : WeierstrassCurve F
inst_1 : W.IsElliptic
inst_2 : W.IsCharTwoJEqZeroNF
inst_3 : CharP F 2
⊢ (↑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 : W.IsCharTwoJNeZeroNF
⊢ W.IsCharTwoNF

Tactic:
IsCharTwoNF.of_j_ne_zero

Premises used: WeierstrassCurve.IsCharTwoNF.of_j_ne_zero
-- 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.IsCharTwoJEqZeroNF
⊢ W.IsCharTwoNF

Tactic:
IsCharTwoNF.of_j_eq_zero

Premises used: WeierstrassCurve.IsCharTwoNF.of_j_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
ha₁ : W.a₁ = 0
a₁ : (HSMul.hSMul (α := VariableChange R) W.toCharTwoJEqZeroNF W).a₁ = 0
a₂ : (HSMul.hSMul (α := VariableChange R) W.toCharTwoJEqZeroNF W).a₂ = 0
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharTwoJEqZeroNF W).IsCharTwoJEqZeroNF

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
ha₁ : W.a₁ = 0
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharTwoJEqZeroNF W).a₁ = 0

Tactic:
simp [toCharTwoJEqZeroNF, ha₁, variableChange_a₁]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.toCharTwoJEqZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
ha₁ : W.a₁ = 0
a₂ : HPow.hPow (α := R) (β := ℕ) 1 2 * (W.a₂ - 0 * W.a₁ + 3 * W.a₂ - HPow.hPow (α := R) (β := ℕ) 0 2) = 0
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharTwoJEqZeroNF W).a₂ = 0

Tactic:
simp_rw [toCharTwoJEqZeroNF, variableChange_a₂, inv_one, Units.val_one]

Premises used: inv_one, WeierstrassCurve.variableChange_a₂, WeierstrassCurve.toCharTwoJEqZeroNF, Units.val_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 2
ha₁ : W.a₁ = 0
⊢ HPow.hPow (α := R) (β := ℕ) 1 2 * (W.a₂ - 0 * W.a₁ + 3 * W.a₂ - HPow.hPow (α := R) (β := ℕ) 0 2) = 0

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

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₂, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
a₁ : (W.toCharTwoJNeZeroNF ha₁ • W).a₁ = 1
a₃ : (W.toCharTwoJNeZeroNF ha₁ • W).a₃ = 0
a₄ : (W.toCharTwoJNeZeroNF ha₁ • W).a₄ = 0
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoJNeZeroNF

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).a₁ = 1

Tactic:
simp [toCharTwoJNeZeroNF, ha₁, variableChange_a₁]

Premises used: WeierstrassCurve.variableChange_a₁, WeierstrassCurve.toCharTwoJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
a₃ :
  HPow.hPow (β := ℕ) W.a₁ 3 * W.a₃ * HAdd.hAdd (α := F) 1 1 +
      2 * (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₄ + HPow.hPow (β := ℕ) W.a₃ 2) =
    0
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).a₃ = 0

Tactic:
simp [field, toCharTwoJNeZeroNF, variableChange_a₃, -mul_eq_zero]

Premises used: WeierstrassCurve.toCharTwoJNeZeroNF, WeierstrassCurve.variableChange_a₃, mul_eq_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ HPow.hPow (β := ℕ) W.a₁ 3 * W.a₃ * HAdd.hAdd (α := F) 1 1 +
      2 * (HPow.hPow (β := ℕ) W.a₁ 2 * W.a₄ + HPow.hPow (β := ℕ) W.a₃ 2) =
    0

Tactic:
linear_combination (W.a₃ * W.a₁ ^ 3 + W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) * CharP.cast_eq_zero F 2

Premises used: CharP.cast_eq_zero, HMul.hMul, WeierstrassCurve.a₃, HPow.hPow, HAdd.hAdd, WeierstrassCurve.a₄, OfNat.ofNat, WeierstrassCurve.a₁