Theorem: Model.b8_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
⊢ b8 (pi_scaling evr e) = ENatValRing.sub_val evr 8 (b8 e)
Tactic:
simp only [b8, pi_scaling]
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 1 e.a1 * ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 6 e.a6 -
            ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 4 e.a4 +
          4 * ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 6 e.a6 +
        ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 -
      ENatValRing.sub_val evr 4 e.a4 * ENatValRing.sub_val evr 4 e.a4 =
    ENatValRing.sub_val evr 8
      (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)

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 1 e.a1 * ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 6 e.a6 -
            ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 4 e.a4 +
          4 * ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 6 e.a6 +
        ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 -
      ENatValRing.sub_val evr 4 e.a4 * ENatValRing.sub_val evr 4 e.a4 =
    ENatValRing.sub_val evr 8
      (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)
Tactic:
exact (pi_scaling_of_b8 evr e h1 h2 h3 h4 h6).symm
State after:
no goals