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.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
⊢ 4 * W.a₂ * W.a₆ = W.a₂ * W.a₆

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

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.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
rw : 16 * HPow.hPow (β := ℕ) W.a₂ 2 = HPow.hPow (β := ℕ) W.a₂ 2
⊢ W.c₄ = HPow.hPow (β := ℕ) W.a₂ 2

Tactic:
rw [c₄_of_isCharThreeJNeZeroNF]

Premises used: WeierstrassCurve.c₄_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
⊢ 16 * HPow.hPow (β := ℕ) W.a₂ 2 = HPow.hPow (β := ℕ) W.a₂ 2

Tactic:
linear_combination 5 * W.a₂ ^ 2 * 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 : -64 * HPow.hPow (β := ℕ) W.a₂ 3 - 864 * W.a₆ = -HPow.hPow (β := ℕ) W.a₂ 3
⊢ W.c₆ = -HPow.hPow (β := ℕ) W.a₂ 3

Tactic:
rw [c₆_of_isCharThreeJNeZeroNF]

Premises used: WeierstrassCurve.c₆_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
⊢ -64 * HPow.hPow (β := ℕ) W.a₂ 3 - 864 * W.a₆ = -HPow.hPow (β := ℕ) W.a₂ 3

Tactic:
linear_combination (-21 * W.a₂ ^ 3 - 288 * W.a₆) * CharP.cast_eq_zero R 3

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:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharThreeJNeZeroNF
inst_2 : CharP R 3
rw : -64 * HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ - 432 * HPow.hPow (β := ℕ) W.a₆ 2 = -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆
⊢ W.Δ = -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆

Tactic:
rw [Δ_of_isCharThreeJNeZeroNF]

Premises used: WeierstrassCurve.Δ_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
⊢ -64 * HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ - 432 * HPow.hPow (β := ℕ) W.a₆ 2 = -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆

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

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.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
⊢ (↑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.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
h : (↑W.Δ' : F) ≠ 0
⊢ -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ ≠ 0

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

Premises used: WeierstrassCurve.coe_Δ', WeierstrassCurve.Δ_of_isCharThreeJNeZeroNF_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.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
h : -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ ≠ 0
rw :
  HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₂ 2) 3 * W.a₆ =
    -HPow.hPow (β := ℕ) W.a₂ 3 * (-HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆)
⊢ W.j = -HPow.hPow (β := ℕ) W.a₂ 3 / W.a₆

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

Premises used: WeierstrassCurve.j, Units.val_inv_eq_inv_val, right_ne_zero_of_mul, div_eq_div_iff, WeierstrassCurve.coe_Δ', div_eq_inv_mul, WeierstrassCurve.c₄_of_isCharThreeJNeZeroNF_of_char_three, WeierstrassCurve.Δ_of_isCharThreeJNeZeroNF_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.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
h : -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ ≠ 0
⊢ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₂ 2) 3 * W.a₆ =
    -HPow.hPow (β := ℕ) W.a₂ 3 * (-HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆)

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.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
rw : -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
⊢ W.j ≠ 0

Tactic:
rw [j_of_isCharThreeJNeZeroNF_of_char_three, div_ne_zero_iff]

Premises used: div_ne_zero_iff, WeierstrassCurve.j_of_isCharThreeJNeZeroNF_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.IsCharThreeJNeZeroNF
inst_3 : CharP F 3
h : (↑W.Δ' : F) ≠ 0
rwa : ∀ (h : W.Δ ≠ 0), -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
rwa₁ : ∀ (h : -HPow.hPow (β := ℕ) W.a₂ 3 * W.a₆ ≠ 0), -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0), -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0
⊢ -HPow.hPow (β := ℕ) W.a₂ 3 ≠ 0 ∧ W.a₆ ≠ 0

Tactic:
rwa [coe_Δ', Δ_of_isCharThreeJNeZeroNF_of_char_three, mul_ne_zero_iff] at h

Premises used: WeierstrassCurve.coe_Δ', WeierstrassCurve.Δ_of_isCharThreeJNeZeroNF_of_char_three, mul_ne_zero_iff
-- 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.IsCharThreeNF

Tactic:
IsCharThreeNF.of_j_ne_zero

Premises used: WeierstrassCurve.IsCharThreeNF.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.IsShortNF
⊢ W.IsCharThreeNF

Tactic:
IsCharThreeNF.of_j_eq_zero

Premises used: WeierstrassCurve.IsCharThreeNF.of_j_eq_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.IsCharThreeNF
of_j_ne_zero : ∀ [W.IsCharThreeJNeZeroNF], W.IsCharNeTwoNF
of_j_eq_zero : ∀ [W.IsShortNF], W.IsCharNeTwoNF
⊢ W.IsCharNeTwoNF

Tactic:
cases ‹W.IsCharThreeNF›

Premises used: WeierstrassCurve.IsCharThreeNF
-- 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:
infer_instance
-- 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:
infer_instance
-- 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 : CharP R 3
inst_3 : CharP F 3
⊢ HMul.hMul (α := R) 2 2 = 1

Tactic:
linear_combination CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
simp_rw :
  HPow.hPow (α := R) (β := ℕ) 1 2 *
      (W.a₂ - 2 * -W.a₁ * W.a₁ + HMul.hMul (α := R) 3 0 - HPow.hPow (β := ℕ) (2 * -W.a₁) 2) =
    HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂
⊢ (HSMul.hSMul (α := VariableChange R) W.toShortNFOfCharThree W).a₂ = W.b₂

Tactic:
simp_rw [toShortNFOfCharThree, toCharNeTwoNF, variableChange_a₂, inv_one, Units.val_one, b₂]

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

Tactic:
linear_combination (-W.a₂ - W.a₁ ^ 2) * CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, HSub.hSub, WeierstrassCurve.a₂, HPow.hPow, OfNat.ofNat, Neg.neg, WeierstrassCurve.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
hb₂ : W.b₂ = 0
⊢ HMul.hMul (α := R) 2 2 = 1

Tactic:
linear_combination CharP.cast_eq_zero R 3

Premises used: CharP.cast_eq_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
hb₂ : W.b₂ = 0
⊢ HMul.hMul (α := R) 2 2 = 1

Tactic:
have h : (2 : R) * 2 = 1 := by linear_combination CharP.cast_eq_zero R 3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
hb₂ : W.b₂ = 0
h : HMul.hMul (α := R) 2 2 = 1
this : Invertible (α := R) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).IsCharNeTwoNF

Tactic:
have H := W.toCharNeTwoNF_spec
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
hb₂ : W.b₂ = 0
h : HMul.hMul (α := R) 2 2 = 1
this : Invertible (α := R) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
H : (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).IsCharNeTwoNF
⊢ (HSMul.hSMul (α := VariableChange R) W.toShortNFOfCharThree W).IsShortNF

Tactic:
⟨H.a₁, hb₂ ▸ W.toShortNFOfCharThree_a₂, H.a₃⟩

Premises used: WeierstrassCurve.IsShortNF.mk, Eq.rec, WeierstrassCurve.toShortNFOfCharThree_a₂, WeierstrassCurve.IsCharNeTwoNF.a₃, WeierstrassCurve.IsCharNeTwoNF.a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : CharP R 3
hb₂ : W.b₂ = 0
h : HMul.hMul (α := R) 2 2 = 1
this : Invertible (α := R) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
H : (HSMul.hSMul (α := VariableChange R) W.toCharNeTwoNF W).IsCharNeTwoNF
⊢ (HSMul.hSMul (α := VariableChange R) W.toShortNFOfCharThree W).IsShortNF

Tactic:
exact ⟨H.a₁, hb₂ ▸ W.toShortNFOfCharThree_a₂, H.a₃⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
⊢ HMul.hMul (α := F) 2 2 = 1

Tactic:
linear_combination CharP.cast_eq_zero F 3

Premises used: CharP.cast_eq_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
⊢ HMul.hMul (α := F) 2 2 = 1

Tactic:
have h : (2 : F) * 2 = 1 := by linear_combination CharP.cast_eq_zero F 3
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
rw :
  (HSMul.hSMul (α := VariableChange F)
      { u := 1,
        r :=
          (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W).a₄ /
            (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W).a₂,
        s := 0, t := 0 : VariableChange F }
      (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W)).IsCharThreeJNeZeroNF
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeJNeZeroNF

Tactic:
rw [toCharThreeNF, mul_smul]

Premises used: WeierstrassCurve.toCharThreeNF, SemigroupAction.mul_smul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
set :
  let W' := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W;
  (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F }
      W').IsCharThreeJNeZeroNF
⊢ (HSMul.hSMul (α := VariableChange F)
      { u := 1,
        r :=
          (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W).a₄ /
            (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W).a₂,
        s := 0, t := 0 : VariableChange F }
      (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W)).IsCharThreeJNeZeroNF

Tactic:
set W' := W.toShortNFOfCharThree • W

Premises used: WeierstrassCurve.toShortNFOfCharThree
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
⊢ W'.IsCharNeTwoNF

Tactic:
haveI : W'.IsCharNeTwoNF := W.toCharNeTwoNF_spec
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this_1 : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
this : W'.IsCharNeTwoNF
a₁ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₁ = 0
a₃ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₃ = 0
a₄ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₄ = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F }
      W').IsCharThreeJNeZeroNF

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this_1 : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
this : W'.IsCharNeTwoNF
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₁ = 0

Tactic:
simp [variableChange_a₁]

Premises used: WeierstrassCurve.variableChange_a₁
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this_1 : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
this : W'.IsCharNeTwoNF
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₃ = 0

Tactic:
simp [variableChange_a₃]

Premises used: WeierstrassCurve.variableChange_a₃
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this_1 : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
this : W'.IsCharNeTwoNF
⊢ W'.a₂ ≠ 0

Tactic:
have ha₂ : W'.a₂ ≠ 0 := W.toShortNFOfCharThree_a₂ ▸ hb₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this_1 : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
this : W'.IsCharNeTwoNF
ha₂ : W'.a₂ ≠ 0
a₄ : W'.a₄ * (HPow.hPow (β := ℕ) W'.a₂ 2 * HAdd.hAdd (α := F) 1 2 + W'.a₄ * 3) = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 : VariableChange F } W').a₄ = 0

Tactic:
simp [field, variableChange_a₄, -mul_eq_zero]

Premises used: mul_eq_zero, WeierstrassCurve.variableChange_a₄
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : HMul.hMul (α := F) 2 2 = 1
this_1 : Invertible (α := F) 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W
this : W'.IsCharNeTwoNF
ha₂ : W'.a₂ ≠ 0
⊢ W'.a₄ * (HPow.hPow (β := ℕ) W'.a₂ 2 * HAdd.hAdd (α := F) 1 2 + W'.a₄ * 3) = 0

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

Premises used: CharP.cast_eq_zero, HMul.hMul, WeierstrassCurve.a₂, HPow.hPow, HAdd.hAdd, WeierstrassCurve.a₄, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
rw : (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W).IsShortNF
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsShortNF

Tactic:
rw [toCharThreeNF, toShortNFOfCharThree_a₂, hb₂, div_zero, ← VariableChange.one_def, one_mul]

Premises used: WeierstrassCurve.VariableChange.one_def, WeierstrassCurve.toShortNFOfCharThree_a₂, WeierstrassCurve.toCharThreeNF, div_zero, one_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W).IsShortNF

Tactic:
W.toShortNFOfCharThree_spec hb₂

Premises used: WeierstrassCurve.toShortNFOfCharThree_spec
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toShortNFOfCharThree W).IsShortNF

Tactic:
exact W.toShortNFOfCharThree_spec hb₂

Premises used: WeierstrassCurve.toShortNFOfCharThree_spec
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 3
inst_3 : CharP F 3
W : WeierstrassCurve F
pos : ∀ (hb₂ : W.b₂ = 0), (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF
neg : ∀ (hb₂ : ¬W.b₂ = 0), (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF

Tactic:
by_cases hb₂ : W.b₂ = 0

Premises used: WeierstrassCurve.b₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 3
inst_3 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsShortNF

Tactic:
haveI := W.toCharThreeNF_spec_of_b₂_eq_zero hb₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 3
inst_3 : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
this : (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsShortNF
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 3
inst_3 : CharP F 3
W : WeierstrassCurve F
hb₂ : ¬W.b₂ = 0
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeJNeZeroNF

Tactic:
haveI := W.toCharThreeNF_spec_of_b₂_ne_zero hb₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
F : Type u_2
inst_1 : Field F
W_1 : WeierstrassCurve R
inst_2 : CharP R 3
inst_3 : CharP F 3
W : WeierstrassCurve F
hb₂ : ¬W.b₂ = 0
this : (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeJNeZeroNF
⊢ (HSMul.hSMul (α := VariableChange F) W.toCharThreeNF W).IsCharThreeNF

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
F : Type u_2
inst : Field F
inst_1 : CharP F 3
W : WeierstrassCurve F
⊢ ∃ (C : VariableChange F), (C • W).IsCharThreeNF

Tactic:
⟨_, W.toCharThreeNF_spec⟩

Premises used: WeierstrassCurve.toCharThreeNF_spec, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
⊢ W.a₁ = 1

Tactic:
IsCharTwoJNeZeroNF.a₁

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

Tactic:
IsCharTwoJNeZeroNF.a₃

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

Tactic:
IsCharTwoJNeZeroNF.a₄

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

Tactic:
rw [b₂, a₁_of_isCharTwoJNeZeroNF]

Premises used: WeierstrassCurve.a₁_of_isCharTwoJNeZeroNF, WeierstrassCurve.b₂
-- 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 + 4 * W.a₂ = 1 + 4 * 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 : HMul.hMul (α := R) 2 0 + W.a₁ * 0 = 0
⊢ W.b₄ = 0

Tactic:
rw [b₄, a₃_of_isCharTwoJNeZeroNF, a₄_of_isCharTwoJNeZeroNF]

Premises used: WeierstrassCurve.b₄, WeierstrassCurve.a₄_of_isCharTwoJNeZeroNF, WeierstrassCurve.a₃_of_isCharTwoJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
⊢ HMul.hMul (α := R) 2 0 + W.a₁ * 0 = 0

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 (α := R) (β := ℕ) 0 2 + 4 * W.a₆ = 4 * W.a₆
⊢ W.b₆ = 4 * W.a₆

Tactic:
rw [b₆, a₃_of_isCharTwoJNeZeroNF]

Premises used: WeierstrassCurve.a₃_of_isCharTwoJNeZeroNF, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
Goal:
R : Type u_1
inst : CommRing R
W : WeierstrassCurve R
inst_1 : W.IsCharTwoJNeZeroNF
⊢ HPow.hPow (α := R) (β := ℕ) 0 2 + 4 * W.a₆ = 4 * 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 (α := 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₆
⊢ W.b₈ = W.a₆ + 4 * W.a₂ * W.a₆

Tactic:
rw [b₈, a₁_of_isCharTwoJNeZeroNF, a₃_of_isCharTwoJNeZeroNF, a₄_of_isCharTwoJNeZeroNF]

Premises used: WeierstrassCurve.a₁_of_isCharTwoJNeZeroNF, WeierstrassCurve.b₈, WeierstrassCurve.a₄_of_isCharTwoJNeZeroNF, WeierstrassCurve.a₃_of_isCharTwoJNeZeroNF