Theorem: Model.discr_of_pi_scaling (ECTate/Algebra/EllipticCurve/LocalEC.lean)

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ discr (pi_scaling evr e) = ENatValRing.sub_val evr 12 (discr e)
Tactic:
simp only [discr, b2_of_pi_scaling evr e h1 h2, b4_of_pi_scaling evr e h1 h3 h4,
  b6_of_pi_scaling evr e h3 h6, b8_of_pi_scaling evr e h1 h2 h3 h4 h6]
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ -ENatValRing.sub_val evr 2 (b2 e) * ENatValRing.sub_val evr 2 (b2 e) * ENatValRing.sub_val evr 8 (b8 e) -
          8 * ENatValRing.sub_val evr 4 (b4 e) ^ 3 -
        27 * ENatValRing.sub_val evr 6 (b6 e) * ENatValRing.sub_val evr 6 (b6 e) +
      9 * ENatValRing.sub_val evr 2 (b2 e) * ENatValRing.sub_val evr 4 (b4 e) * ENatValRing.sub_val evr 6 (b6 e) =
    ENatValRing.sub_val evr 12 (-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
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ -ENatValRing.sub_val evr 2 (b2 e) * ENatValRing.sub_val evr 2 (b2 e) * ENatValRing.sub_val evr 8 (b8 e) -
          8 * ENatValRing.sub_val evr 4 (b4 e) ^ 3 -
        27 * ENatValRing.sub_val evr 6 (b6 e) * ENatValRing.sub_val evr 6 (b6 e) +
      9 * ENatValRing.sub_val evr 2 (b2 e) * ENatValRing.sub_val evr 4 (b4 e) * ENatValRing.sub_val evr 6 (b6 e) =
    ENatValRing.sub_val evr 12 (-b2 e * b2 e * b8 e - 8 * b4 e ^ 3 - 27 * b6 e * b6 e + 9 * b2 e * b4 e * b6 e)
Tactic:
exact (pi_scaling_of_discr evr e (val_b2_of_val_a12 evr e h1 h2)
  (val_b4_of_val_a134 evr e h1 h3 h4) (val_b6_of_val_a36 evr e h3 h6)
  (val_b8_of_val_ai evr e h1 h2 h3 h4 h6)).symm
State after:
no goals