have h3 : (3 : K) ≠ 0 := fun hh => hn3 (ringChar_eq_of_Prime hh (by norm_num))
case pos.h_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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
    dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
      dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0
case pos.h_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✝ : ℕ
hn2 : ringChar K = 2 → False
hn3 : ringChar K = 3 → False
h2 : 2 ≠ 0
h3 : 3 ≠ 0
⊢ weierstrass e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
    dweierstrass_dx e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0 ∧
      dweierstrass_dy e (-b2 e / 12, -(-e.a1 * b2 e / 12 + e.a3) / 2) = 0