Theorem: Model.discr_in_jacobian_ideal
Proof state before:
R : Type u
inst✝ : CommRing R
e : Model R
P : R × R
⊢ -(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) =
    -((48 * P.fst * P.snd * e.a2 ^ 2 + 24 * e.a1 * e.a2 * e.a6 + 216 * P.snd * e.a6 + P.snd * e.a1 ^ 6 +
                                                        11 * P.snd * e.a1 ^ 4 * e.a2 +
                                                      P.fst * e.a1 ^ 4 * e.a3 +
                                                    38 * P.fst * e.a1 ^ 2 * e.a2 * e.a3 +
                                                  8 * e.a1 ^ 2 * e.a2 ^ 2 * e.a3 +
                                                e.a1 ^ 4 * e.a2 * e.a3 +
                                              40 * P.snd * e.a1 ^ 2 * e.a2 ^ 2 +
                                            32 * P.snd * e.a2 ^ 3 +
                                          24 * P.fst * P.snd * e.a1 * e.a3 +
                                        30 * P.fst ^ 2 * e.a2 * e.a3 +
                                      3 * P.fst * e.a1 ^ 3 * e.a4 +
                                    60 * P.fst ^ 2 * e.a1 * e.a4 +
                                  30 * P.fst ^ 2 * e.a1 ^ 2 * e.a3 +
                                31 * e.a1 ^ 2 * e.a3 * e.a4 +
                              144 * P.snd ^ 2 * e.a3 +
                            198 * P.snd * e.a3 ^ 2 +
                          27 * e.a3 ^ 3 +
                        60 * e.a1 * e.a4 ^ 2 +
                      36 * P.fst * e.a1 * e.a6 +
                    76 * P.fst * e.a2 ^ 2 * e.a3 +
                  16 * e.a2 ^ 3 * e.a3 +
                84 * P.fst * e.a1 * e.a2 * e.a4 -
              (36 * e.a3 * e.a6 + P.fst ^ 2 * e.a1 ^ 5 + P.fst * e.a1 ^ 5 * e.a2 + P.fst * P.snd * e.a1 ^ 4 +
                                                      9 * P.fst ^ 2 * e.a1 ^ 3 * e.a2 +
                                                    10 * P.fst * e.a1 ^ 3 * e.a2 ^ 2 +
                                                  e.a1 ^ 5 * e.a4 +
                                                6 * P.snd ^ 2 * e.a1 ^ 3 +
                                              8 * P.fst * P.snd * e.a1 ^ 2 * e.a2 +
                                            24 * P.fst ^ 2 * e.a1 * e.a2 ^ 2 +
                                          32 * P.fst * e.a1 * e.a2 ^ 3 +
                                        35 * P.snd * e.a1 ^ 3 * e.a3 +
                                      e.a1 ^ 3 * e.a3 ^ 2 +
                                    9 * e.a1 ^ 3 * e.a2 * e.a4 +
                                  48 * P.snd ^ 2 * e.a1 * e.a2 +
                                134 * P.snd * e.a1 * e.a2 * e.a3 +
                              27 * P.fst * e.a1 * e.a3 ^ 2 +
                            36 * e.a1 * e.a2 * e.a3 ^ 2 +
                          58 * P.snd * e.a1 ^ 2 * e.a4 +
                        24 * e.a1 * e.a2 ^ 2 * e.a4 +
                      144 * P.fst * P.snd * e.a4 +
                    120 * P.snd * e.a2 * e.a4 +
                  168 * P.fst * e.a3 * e.a4 +
                34 * e.a2 * e.a3 * e.a4)) *
            dweierstrass_dy e P +
          (e.a1 ^ 2 * e.a3 ^ 2 + 12 * e.a1 ^ 2 * e.a6 + 16 * e.a2 ^ 2 * e.a4 + 32 * P.fst * e.a2 ^ 3 + e.a1 ^ 4 * e.a4 +
                                      144 * P.fst * e.a6 +
                                    48 * e.a2 * e.a6 +
                                  P.fst * e.a1 ^ 4 * e.a2 +
                                84 * P.fst * e.a3 ^ 2 +
                              56 * P.snd * e.a1 * e.a4 +
                            8 * e.a1 ^ 2 * e.a2 * e.a4 +
                          28 * P.snd * e.a1 ^ 2 * e.a3 +
                        52 * P.snd * e.a2 * e.a3 +
                      96 * P.fst * P.snd * e.a3 +
                    8 * P.fst * e.a1 ^ 2 * e.a2 ^ 2 +
                  38 * e.a2 * e.a3 ^ 2 +
                32 * P.fst ^ 2 * e.a2 ^ 2 -
              (2 * P.fst * e.a1 ^ 3 * e.a3 + 112 * P.fst * e.a2 * e.a4 + e.a1 ^ 3 * e.a2 * e.a3 +
                                  36 * e.a1 * e.a3 * e.a4 +
                                96 * P.fst ^ 2 * e.a4 +
                              32 * P.fst * P.snd * e.a1 * e.a2 +
                            32 * P.snd * e.a1 * e.a2 ^ 2 +
                          64 * e.a4 ^ 2 +
                        4 * P.fst * P.snd * e.a1 ^ 3 +
                      10 * P.snd * e.a1 ^ 3 * e.a2 +
                    P.snd * e.a1 ^ 5 +
                  8 * e.a1 * e.a2 ^ 2 * e.a3 +
                46 * P.fst * e.a1 * e.a2 * e.a3)) *
            dweierstrass_dx e P +
        (60 * e.a1 ^ 2 * e.a4 + 288 * P.fst * e.a4 + 240 * e.a2 * e.a4 + 12 * P.snd * e.a1 ^ 3 + 36 * e.a1 ^ 3 * e.a3 +
                96 * P.snd * e.a1 * e.a2 +
              168 * e.a1 * e.a2 * e.a3 -
            (432 * e.a6 + e.a1 ^ 6 + 288 * P.snd * e.a3 + 252 * e.a3 ^ 2 + 12 * e.a1 ^ 4 * e.a2 +
                  48 * e.a1 ^ 2 * e.a2 ^ 2 +
                96 * P.fst * e.a2 ^ 2 +
              64 * e.a2 ^ 3)) *
          weierstrass e P)
Tactic:
simp only [weierstrass, dweierstrass_dx, dweierstrass_dy]
Proof state after:
R : Type u
inst✝ : CommRing R
e : Model R
P : R × R
⊢ -(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) =
    -((48 * P.fst * P.snd * e.a2 ^ 2 + 24 * e.a1 * e.a2 * e.a6 + 216 * P.snd * e.a6 + P.snd * e.a1 ^ 6 +
                                                        11 * P.snd * e.a1 ^ 4 * e.a2 +
                                                      P.fst * e.a1 ^ 4 * e.a3 +
                                                    38 * P.fst * e.a1 ^ 2 * e.a2 * e.a3 +
                                                  8 * e.a1 ^ 2 * e.a2 ^ 2 * e.a3 +
                                                e.a1 ^ 4 * e.a2 * e.a3 +
                                              40 * P.snd * e.a1 ^ 2 * e.a2 ^ 2 +
                                            32 * P.snd * e.a2 ^ 3 +
                                          24 * P.fst * P.snd * e.a1 * e.a3 +
                                        30 * P.fst ^ 2 * e.a2 * e.a3 +
                                      3 * P.fst * e.a1 ^ 3 * e.a4 +
                                    60 * P.fst ^ 2 * e.a1 * e.a4 +
                                  30 * P.fst ^ 2 * e.a1 ^ 2 * e.a3 +
                                31 * e.a1 ^ 2 * e.a3 * e.a4 +
                              144 * P.snd ^ 2 * e.a3 +
                            198 * P.snd * e.a3 ^ 2 +
                          27 * e.a3 ^ 3 +
                        60 * e.a1 * e.a4 ^ 2 +
                      36 * P.fst * e.a1 * e.a6 +
                    76 * P.fst * e.a2 ^ 2 * e.a3 +
                  16 * e.a2 ^ 3 * e.a3 +
                84 * P.fst * e.a1 * e.a2 * e.a4 -
              (36 * e.a3 * e.a6 + P.fst ^ 2 * e.a1 ^ 5 + P.fst * e.a1 ^ 5 * e.a2 + P.fst * P.snd * e.a1 ^ 4 +
                                                      9 * P.fst ^ 2 * e.a1 ^ 3 * e.a2 +
                                                    10 * P.fst * e.a1 ^ 3 * e.a2 ^ 2 +
                                                  e.a1 ^ 5 * e.a4 +
                                                6 * P.snd ^ 2 * e.a1 ^ 3 +
                                              8 * P.fst * P.snd * e.a1 ^ 2 * e.a2 +
                                            24 * P.fst ^ 2 * e.a1 * e.a2 ^ 2 +
                                          32 * P.fst * e.a1 * e.a2 ^ 3 +
                                        35 * P.snd * e.a1 ^ 3 * e.a3 +
                                      e.a1 ^ 3 * e.a3 ^ 2 +
                                    9 * e.a1 ^ 3 * e.a2 * e.a4 +
                                  48 * P.snd ^ 2 * e.a1 * e.a2 +
                                134 * P.snd * e.a1 * e.a2 * e.a3 +
                              27 * P.fst * e.a1 * e.a3 ^ 2 +
                            36 * e.a1 * e.a2 * e.a3 ^ 2 +
                          58 * P.snd * e.a1 ^ 2 * e.a4 +
                        24 * e.a1 * e.a2 ^ 2 * e.a4 +
                      144 * P.fst * P.snd * e.a4 +
                    120 * P.snd * e.a2 * e.a4 +
                  168 * P.fst * e.a3 * e.a4 +
                34 * e.a2 * e.a3 * e.a4)) *
            (2 * P.snd + e.a1 * P.fst + e.a3) +
          (e.a1 ^ 2 * e.a3 ^ 2 + 12 * e.a1 ^ 2 * e.a6 + 16 * e.a2 ^ 2 * e.a4 + 32 * P.fst * e.a2 ^ 3 + e.a1 ^ 4 * e.a4 +
                                      144 * P.fst * e.a6 +
                                    48 * e.a2 * e.a6 +
                                  P.fst * e.a1 ^ 4 * e.a2 +
                                84 * P.fst * e.a3 ^ 2 +
                              56 * P.snd * e.a1 * e.a4 +
                            8 * e.a1 ^ 2 * e.a2 * e.a4 +
                          28 * P.snd * e.a1 ^ 2 * e.a3 +
                        52 * P.snd * e.a2 * e.a3 +
                      96 * P.fst * P.snd * e.a3 +
                    8 * P.fst * e.a1 ^ 2 * e.a2 ^ 2 +
                  38 * e.a2 * e.a3 ^ 2 +
                32 * P.fst ^ 2 * e.a2 ^ 2 -
              (2 * P.fst * e.a1 ^ 3 * e.a3 + 112 * P.fst * e.a2 * e.a4 + e.a1 ^ 3 * e.a2 * e.a3 +
                                  36 * e.a1 * e.a3 * e.a4 +
                                96 * P.fst ^ 2 * e.a4 +
                              32 * P.fst * P.snd * e.a1 * e.a2 +
                            32 * P.snd * e.a1 * e.a2 ^ 2 +
                          64 * e.a4 ^ 2 +
                        4 * P.fst * P.snd * e.a1 ^ 3 +
                      10 * P.snd * e.a1 ^ 3 * e.a2 +
                    P.snd * e.a1 ^ 5 +
                  8 * e.a1 * e.a2 ^ 2 * e.a3 +
                46 * P.fst * e.a1 * e.a2 * e.a3)) *
            (e.a1 * P.snd - (3 * P.fst ^ 2 + 2 * e.a2 * P.fst + e.a4)) +
        (60 * e.a1 ^ 2 * e.a4 + 288 * P.fst * e.a4 + 240 * e.a2 * e.a4 + 12 * P.snd * e.a1 ^ 3 + 36 * e.a1 ^ 3 * e.a3 +
                96 * P.snd * e.a1 * e.a2 +
              168 * e.a1 * e.a2 * e.a3 -
            (432 * e.a6 + e.a1 ^ 6 + 288 * P.snd * e.a3 + 252 * e.a3 ^ 2 + 12 * e.a1 ^ 4 * e.a2 +
                  48 * e.a1 ^ 2 * e.a2 ^ 2 +
                96 * P.fst * e.a2 ^ 2 +
              64 * e.a2 ^ 3)) *
          (P.snd ^ 2 + e.a1 * P.fst * P.snd + e.a3 * P.snd - (P.fst ^ 3 + e.a2 * P.fst ^ 2 + e.a4 * P.fst + e.a6)))