simp only [mul_zero, zero_mul, add_zero, neg_zero, sub_self, zero_add, one_mul, zero_sub, neg_eq_zero]
  at hdisc
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
hdisc :
  -(0 * 0 + 0 * 0 * e.a2) * (0 * 0 + 0 * 0 * e.a2) *
            (0 * 0 * e.a6 - 0 * e.a3 * e.a4 + 0 * 0 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4) -
          0 * (0 * 0) * (0 * e.a3 + 0 * e.a4) ^ 3 -
        (0 * 13 + 1) * (e.a3 * e.a3 + 0 * 0 * e.a6) * (e.a3 * e.a3 + 0 * 0 * e.a6) +
      9 * (0 * 0 + 0 * 0 * e.a2) * (0 * e.a3 + 0 * e.a4) * (e.a3 * e.a3 + 0 * 0 * e.a6) =
    0
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
⊢ e.a3 = 0
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
e : Model K
h : ringChar K = 2
ha1 : e.a1 = 0
hchar' : ↑(ringChar K) = 2
hchar'' : 2 = 0
hdisc : e.a3 * e.a3 * (e.a3 * e.a3) = 0
⊢ e.a3 = 0