Theorem: Model.Field.is_singular_point_singular_point
Proof state before:
case neg.refine_1
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 + 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.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) * e.a1 *
              (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) *
            ((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)) +
        ((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)) *
            e.a3 *
          ((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)) -
      ((18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 3 +
            ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) * e.a2 *
              (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 2 +
          ((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)) *
              e.a4 *
            (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 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)) *
            ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
          e.a6) =
    0
Tactic:
rw [← mul_zero (e.a1^6 + 12*e.a1^4*e.a2 + 48*e.a1^2*e.a2^2 - 36*e.a1^3*e.a3 + 64*e.a2^3
  - 144*e.a1*e.a2*e.a3 - 72*e.a1^2*e.a4 + 216*e.a3^2 - 288*e.a2*e.a4 + 864*e.a6),
  ← h, discr_eq_neg_singular]
Proof state after:
case neg.refine_1
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 + 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.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) * e.a1 *
              (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) *
            ((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)) +
        ((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)) *
            e.a3 *
          ((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)) -
      ((18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 3 +
            ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) * e.a2 *
              (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4)) ^ 2 +
          ((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)) *
              e.a4 *
            (18 * (e.a3 * e.a3 + 4 * e.a6) - (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 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)) *
            ((e.a1 * e.a1 + 4 * e.a2) ^ 2 - 24 * (e.a1 * e.a3 + 2 * e.a4)) *
          e.a6) =
    (e.a1 ^ 6 + 12 * e.a1 ^ 4 * e.a2 + 48 * e.a1 ^ 2 * e.a2 ^ 2 - 36 * e.a1 ^ 3 * e.a3 + 64 * e.a2 ^ 3 -
                144 * e.a1 * e.a2 * e.a3 -
              72 * e.a1 ^ 2 * e.a4 +
            216 * e.a3 ^ 2 -
          288 * e.a2 * e.a4 +
        864 * e.a6) *
      -(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)