rw [show (3 : K) = 2 * 2 - 1 by norm_num]
case pos.h_1.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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 = 3 * e.a4
case pos.h_1.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 = 2
hchar : ringChar K = 2
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hcharne : ringChar K ≠ 0
ha1 : e.a1 = 0
ha3 : e.a3 = 0
⊢ -e.a4 = (2 * 2 - 1) * e.a4