. rw [weierstrass]
  rw [← hchar, pth_root_pow_char hcharne]
  simp only
  rw [show
    (e.a1 * pth_root (-(e.a3 ^ 2) - e.a6) + e.a3) ^ 2 +
    e.a1 * pth_root (-(e.a3 ^ 2) - e.a6) * (e.a1 * pth_root (-(e.a3 ^ 2) - e.a6) + e.a3) +
    e.a3 * (e.a1 * pth_root (-(e.a3 ^ 2) - e.a6) + e.a3) -
    (-(e.a3 ^ 2) - e.a6 + e.a2 * pth_root (-(e.a3 ^ 2) - e.a6) ^ 2 + e.a4 * pth_root (-(e.a3 ^ 2) - e.a6) + e.a6) =
    (2 * e.a1 ^ 2 - e.a2) * pth_root (-(e.a3 ^ 2) - e.a6) ^ 2 +
    (4 * e.a1 * e.a3 - e.a4) * pth_root (-(e.a3 ^ 2) - e.a6) +
    3 * e.a3 ^ 2
    by ring]
  rw [show 2 * e.a1 ^ 2 - e.a2 = 0 from ?_]
  rw [show 4 * e.a1 * e.a3 - e.a4 = 0 from ?_]
  simp only [zero_mul, add_zero, hchar'']
  . rw [show (2 : K) = -1 by rw [← add_zero (-1), ← hchar'']; norm_num] at hb4
    rw [show (4 : K) = 1 by rw [← add_zero 1, ← hchar'']; norm_num]
    simp only [neg_mul, one_mul] at hb4
    simp [sub_eq_add_neg, hb4]
  . linear_combination (norm := ring_nf <;> simp [hchar'']) -hb2
case pos.h_2.refine_1
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 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ weierstrass e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0

case pos.h_2.refine_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 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0

case pos.h_2.refine_3
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 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 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.refine_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 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ dweierstrass_dx e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0

case pos.h_2.refine_3
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 : e.a1 * e.a1 + 4 * e.a2 = 0
hb4 : e.a1 * e.a3 + 2 * e.a4 = 0
⊢ dweierstrass_dy e (pth_root (-e.a3 ^ 2 - e.a6), e.a1 * pth_root (-e.a3 ^ 2 - e.a6) + e.a3) = 0