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

State before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 1728 * discr e = c4 e ^ 3 - c6 e ^ 2
Tactic:
simp only [c4, c6, discr, mul_sub, mul_add]
State after:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 1728 * (-b2 e * b2 e * b8 e) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) + 1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2

State before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 1728 * (-b2 e * b2 e * b8 e) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) + 1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2
Tactic:
rw [(by ring : 1728 * (-e.b2 * e.b2 * e.b8) = -432 * e.b2 * e.b2 * (4 * e.b8))]
State after:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ -432 * b2 e * b2 e * (4 * b8 e) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) +
      1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2

State before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ -432 * b2 e * b2 e * (4 * b8 e) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) +
      1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2
Tactic:
rw [b8_identity]
State after:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ -432 * b2 e * b2 e * (b2 e * b6 e - b4 e ^ 2) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) +
      1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2

State before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ -432 * b2 e * b2 e * (b2 e * b6 e - b4 e ^ 2) - 1728 * (8 * b4 e ^ 3) - 1728 * (27 * b6 e * b6 e) +
      1728 * (9 * b2 e * b4 e * b6 e) =
    (b2 e ^ 2 - 24 * b4 e) ^ 3 - (-b2 e ^ 3 + 36 * b2 e * b4 e - 216 * b6 e) ^ 2
Tactic:
ring
State after:
no goals

State before:
R : Type u
inst✝ : CommRing R
e : Model R
⊢ 1728 * (-b2 e * b2 e * b8 e) = -432 * b2 e * b2 e * (4 * b8 e)
Tactic:
ring
State after:
no goals