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

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ discr (rst_iso r s t e) = discr e
Tactic:
simp only [discr, rst_b2, rst_b4, rst_b6, rst_b8]
State after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e + 12 * r) * (b2 e + 12 * r) * (b8 e + 3 * r * b6 e + 3 * r * r * b4 e + r * r * r * b2 e + 3 * r * r * r * r) -
          8 * (b4 e + r * (b2 e + 6 * r)) ^ 3 -
        27 * (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) *
          (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) +
      9 * (b2 e + 12 * r) * (b4 e + r * (b2 e + 6 * r)) * (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e + 12 * r) * (b2 e + 12 * r) * (b8 e + 3 * r * b6 e + 3 * r * r * b4 e + r * r * r * b2 e + 3 * r * r * r * r) -
          8 * (b4 e + r * (b2 e + 6 * r)) ^ 3 -
        27 * (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) *
          (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) +
      9 * (b2 e + 12 * r) * (b4 e + r * (b2 e + 6 * r)) * (b6 e + 2 * r * b4 e + r * r * b2 e + 4 * r * r * r) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e
Tactic:
simp only [mul_add]
State after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * b8 e +
                  (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * b6 e) +
                (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * b4 e) +
              (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (r * r * r * b2 e) +
            (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * r * r) -
          8 * (b4 e + (r * b2 e + r * (6 * r))) ^ 3 -
        ((27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * b6 e +
              (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (2 * r * b4 e) +
            (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (r * r * b2 e) +
          (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (4 * r * r * r)) +
      (((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              b6 e +
            ((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              (2 * r * b4 e) +
          ((9 * b2 e + 9 * (12 * r)) * b4 e +
              ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
            (r * r * b2 e) +
        ((9 * b2 e + 9 * (12 * r)) * b4 e +
            ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
          (4 * r * r * r)) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * b8 e +
                  (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * b6 e) +
                (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * b4 e) +
              (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (r * r * r * b2 e) +
            (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * r * r) -
          8 * (b4 e + (r * b2 e + r * (6 * r))) ^ 3 -
        ((27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * b6 e +
              (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (2 * r * b4 e) +
            (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (r * r * b2 e) +
          (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (4 * r * r * r)) +
      (((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              b6 e +
            ((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              (2 * r * b4 e) +
          ((9 * b2 e + 9 * (12 * r)) * b4 e +
              ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
            (r * r * b2 e) +
        ((9 * b2 e + 9 * (12 * r)) * b4 e +
            ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
          (4 * r * r * r)) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e
Tactic:
rw [(by ring : (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * b8 e = -(b2 e ^ 2 * b8 e) + (- (3 * r) * b2 e + -(b2 e + 12 * r) * (3 * r)) * (4 * b8 e))]
State after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e ^ 2 * b8 e) + (-(3 * r) * b2 e + -(b2 e + 12 * r) * (3 * r)) * (4 * b8 e) +
                  (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * b6 e) +
                (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * b4 e) +
              (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (r * r * r * b2 e) +
            (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * r * r) -
          8 * (b4 e + (r * b2 e + r * (6 * r))) ^ 3 -
        ((27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * b6 e +
              (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (2 * r * b4 e) +
            (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (r * r * b2 e) +
          (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (4 * r * r * r)) +
      (((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              b6 e +
            ((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              (2 * r * b4 e) +
          ((9 * b2 e + 9 * (12 * r)) * b4 e +
              ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
            (r * r * b2 e) +
        ((9 * b2 e + 9 * (12 * r)) * b4 e +
            ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
          (4 * r * r * r)) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e ^ 2 * b8 e) + (-(3 * r) * b2 e + -(b2 e + 12 * r) * (3 * r)) * (4 * b8 e) +
                  (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * b6 e) +
                (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * b4 e) +
              (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (r * r * r * b2 e) +
            (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * r * r) -
          8 * (b4 e + (r * b2 e + r * (6 * r))) ^ 3 -
        ((27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * b6 e +
              (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (2 * r * b4 e) +
            (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (r * r * b2 e) +
          (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (4 * r * r * r)) +
      (((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              b6 e +
            ((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              (2 * r * b4 e) +
          ((9 * b2 e + 9 * (12 * r)) * b4 e +
              ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
            (r * r * b2 e) +
        ((9 * b2 e + 9 * (12 * r)) * b4 e +
            ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
          (4 * r * r * r)) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e
Tactic:
rw [b8_identity]
State after:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e ^ 2 * b8 e) + (-(3 * r) * b2 e + -(b2 e + 12 * r) * (3 * r)) * (b2 e * b6 e - b4 e ^ 2) +
                  (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * b6 e) +
                (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * b4 e) +
              (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (r * r * r * b2 e) +
            (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * r * r) -
          8 * (b4 e + (r * b2 e + r * (6 * r))) ^ 3 -
        ((27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * b6 e +
              (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (2 * r * b4 e) +
            (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (r * r * b2 e) +
          (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (4 * r * r * r)) +
      (((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              b6 e +
            ((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              (2 * r * b4 e) +
          ((9 * b2 e + 9 * (12 * r)) * b4 e +
              ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
            (r * r * b2 e) +
        ((9 * b2 e + 9 * (12 * r)) * b4 e +
            ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
          (4 * r * r * r)) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ -(b2 e ^ 2 * b8 e) + (-(3 * r) * b2 e + -(b2 e + 12 * r) * (3 * r)) * (b2 e * b6 e - b4 e ^ 2) +
                  (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * b6 e) +
                (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * b4 e) +
              (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (r * r * r * b2 e) +
            (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * (3 * r * r * r * r) -
          8 * (b4 e + (r * b2 e + r * (6 * r))) ^ 3 -
        ((27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * b6 e +
              (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (2 * r * b4 e) +
            (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (r * r * b2 e) +
          (27 * b6 e + 27 * (2 * r * b4 e) + 27 * (r * r * b2 e) + 27 * (4 * r * r * r)) * (4 * r * r * r)) +
      (((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              b6 e +
            ((9 * b2 e + 9 * (12 * r)) * b4 e +
                ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
              (2 * r * b4 e) +
          ((9 * b2 e + 9 * (12 * r)) * b4 e +
              ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
            (r * r * b2 e) +
        ((9 * b2 e + 9 * (12 * r)) * b4 e +
            ((9 * b2 e + 9 * (12 * r)) * (r * b2 e) + (9 * b2 e + 9 * (12 * r)) * (r * (6 * r)))) *
          (4 * r * r * r)) =
    -b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e
Tactic:
ring
State after:
no goals

State before:
R : Type u
inst✝ : CommRing R
r s t : R
e : Model R
⊢ (-(b2 e + 12 * r) * b2 e + -(b2 e + 12 * r) * (12 * r)) * b8 e =
    -(b2 e ^ 2 * b8 e) + (-(3 * r) * b2 e + -(b2 e + 12 * r) * (3 * r)) * (4 * b8 e)
Tactic:
ring
State after:
no goals