have hb4 : e.b4 = 0 := b4_zero_of_b2_zero_of_disc_zero_of_char_three e hchar h hb2
case pos.h_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝ : ℕ
heq✝ : ringChar K = 3
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : b2 e = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0
case pos.h_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : c4 e = 0
hc6 : c6 e = 0
x✝ : ℕ
heq✝ : ringChar K = 3
hchar : ringChar K = 3
hcharne : ringChar K ≠ 0
hchar' : ↑(ringChar K) = 3
hchar'' : 3 = 0
hb2 : b2 e = 0
hb4 : b4 e = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
    dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0 ∧
      dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0