rw [← mul_zero (36 : K), ← h, discr_eq_neg_singular]
case neg.refine_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
          (e.a1 *
              ((e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a4 - 2 * e.a2 * e.a3) +
                3 * (e.a1 * (e.a3 ^ 2 - 12 * e.a6) + 8 * e.a3 * e.a4)) -
            2 * e.a2 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4))) -
        3 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 2 -
      e.a4 * ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
        ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) =
    0
case neg.refine_2
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
hc4 : ¬c4 e = 0
⊢ ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
          (e.a1 *
              ((e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a4 - 2 * e.a2 * e.a3) +
                3 * (e.a1 * (e.a3 ^ 2 - 12 * e.a6) + 8 * e.a3 * e.a4)) -
            2 * e.a2 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4))) -
        3 * (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 2 -
      e.a4 * ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
        ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) =
    36 *
      -(e.a1 ^ 4 * e.a2 * e.a3 ^ 2 - e.a1 ^ 5 * e.a3 * e.a4 + e.a1 ^ 6 * e.a6 + 8 * e.a1 ^ 2 * e.a2 ^ 2 * e.a3 ^ 2 -
                                                    e.a1 ^ 3 * e.a3 ^ 3 -
                                                  8 * e.a1 ^ 3 * e.a2 * e.a3 * e.a4 -
                                                e.a1 ^ 4 * e.a4 ^ 2 +
                                              12 * e.a1 ^ 4 * e.a2 * e.a6 +
                                            16 * e.a2 ^ 3 * e.a3 ^ 2 -
                                          36 * e.a1 * e.a2 * e.a3 ^ 3 -
                                        16 * e.a1 * e.a2 ^ 2 * e.a3 * e.a4 +
                                      30 * e.a1 ^ 2 * e.a3 ^ 2 * e.a4 -
                                    8 * e.a1 ^ 2 * e.a2 * e.a4 ^ 2 +
                                  48 * e.a1 ^ 2 * e.a2 ^ 2 * e.a6 -
                                36 * e.a1 ^ 3 * e.a3 * e.a6 +
                              27 * e.a3 ^ 4 -
                            72 * e.a2 * e.a3 ^ 2 * e.a4 -
                          16 * e.a2 ^ 2 * e.a4 ^ 2 +
                        96 * e.a1 * e.a3 * e.a4 ^ 2 +
                      64 * e.a2 ^ 3 * e.a6 -
                    144 * e.a1 * e.a2 * e.a3 * e.a6 -
                  72 * e.a1 ^ 2 * e.a4 * e.a6 +
                64 * e.a4 ^ 3 +
              216 * e.a3 ^ 2 * e.a6 -
            288 * e.a2 * e.a4 * e.a6 +
          432 * e.a6 ^ 2)