-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem toCharThreeNF_spec_of_b₂_ne_zero (hb₂ : W.b₂ ≠ 0) :
    (W.variableChange W.toCharThreeNF).IsCharThreeJNeZeroNF

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
⊢ (W.variableChange W.toCharThreeNF).IsCharThreeJNeZeroNF

Tactic:
letI : Invertible (2 : F) := ⟨2, h, h⟩

Result:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ (W.variableChange W.toCharThreeNF).IsCharThreeJNeZeroNF

Proof state:
case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).a₄ = 0

Tactic:
have ha₂ : W'.a₂ ≠ 0 := W.toShortNFOfCharThree_a₂ ▸ hb₂

Result:
case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
ha₂ : W'.a₂ ≠ 0
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).a₄ = 0

Proof state:
case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
ha₂ : W'.a₂ ≠ 0
⊢ (W'.a₄ + 2 * W'.a₄) * W'.a₂ ^ 2 + 3 * W'.a₄ ^ 2 = 0

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

Result:
no goals

Proof state:
case a₃
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).a₃ = 0

Tactic:
simp

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ (W.variableChange W.toCharThreeNF).IsCharThreeJNeZeroNF

Tactic:
rw [toCharThreeNF, variableChange_comp]

Result:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ ((W.variableChange W.toShortNFOfCharThree).variableChange
      { u := 1, r := (W.variableChange W.toShortNFOfCharThree).a₄ / (W.variableChange W.toShortNFOfCharThree).a₂,
        s := 0, t := 0 }).IsCharThreeJNeZeroNF

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
⊢ ((W.variableChange W.toShortNFOfCharThree).variableChange
      { u := 1, r := (W.variableChange W.toShortNFOfCharThree).a₄ / (W.variableChange W.toShortNFOfCharThree).a₂,
        s := 0, t := 0 }).IsCharThreeJNeZeroNF

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

Result:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).IsCharThreeJNeZeroNF

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
⊢ (W.variableChange W.toCharThreeNF).IsCharThreeJNeZeroNF

Tactic:
have h : (2 : F) * 2 = 1 := by linear_combination CharP.cast_eq_zero F 3

Result:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
⊢ (W.variableChange W.toCharThreeNF).IsCharThreeJNeZeroNF

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
⊢ 2 * 2 = 1

Tactic:
linear_combination CharP.cast_eq_zero F 3

Result:
no goals

Proof state:
case a₁
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).a₁ = 0

Tactic:
simp

Result:
no goals

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).IsCharThreeJNeZeroNF

Tactic:
constructor

Result:
case a₁
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).a₁ = 0

case a₃
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).a₃ = 0

case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).a₄ = 0

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).IsCharThreeJNeZeroNF

Tactic:
haveI : W'.IsCharNeTwoNF := W.toCharNeTwoNF_spec

Result:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).IsCharThreeJNeZeroNF

Proof state:
case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
ha₂ : W'.a₂ ≠ 0
⊢ (W'.variableChange { u := 1, r := W'.a₄ / W'.a₂, s := 0, t := 0 }).a₄ = 0

Tactic:
field_simp [ha₂]

Result:
case a₄
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ ≠ 0
h : 2 * 2 = 1
this✝ : Invertible 2 := { invOf := 2, invOf_mul_self := h, mul_invOf_self := h }
W' : WeierstrassCurve F := W.variableChange W.toShortNFOfCharThree
this : W'.IsCharNeTwoNF
ha₂ : W'.a₂ ≠ 0
⊢ (W'.a₄ + 2 * W'.a₄) * W'.a₂ ^ 2 + 3 * W'.a₄ ^ 2 = 0