Theorem: Model.discr_eq_neg_singular (ECTate/Algebra/EllipticCurve/Model.lean)

State before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ discr e =
    -(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)
Tactic:
simp only [discr, weierstrass, dweierstrass_dx, dweierstrass_dy, b2, b4, b6, b8]
State after:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ -(e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a1 + 4 * e.a2) *
            (e.a1 * e.a1 * e.a6 - e.a1 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4) -
          8 * (e.a1 * e.a3 + 2 * e.a4) ^ 3 -
        27 * (e.a3 * e.a3 + 4 * e.a6) * (e.a3 * e.a3 + 4 * e.a6) +
      9 * (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4) * (e.a3 * e.a3 + 4 * 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)

State before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ -(e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a1 + 4 * e.a2) *
            (e.a1 * e.a1 * e.a6 - e.a1 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4) -
          8 * (e.a1 * e.a3 + 2 * e.a4) ^ 3 -
        27 * (e.a3 * e.a3 + 4 * e.a6) * (e.a3 * e.a3 + 4 * e.a6) +
      9 * (e.a1 * e.a1 + 4 * e.a2) * (e.a1 * e.a3 + 2 * e.a4) * (e.a3 * e.a3 + 4 * 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)
Tactic:
ring
State after:
no goals