Theorem: Model.b4_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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ b4 (pi_scaling evr e) = ENatValRing.sub_val evr 4 (b4 e)
Tactic:
simp only [b4, 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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 + 2 * ENatValRing.sub_val evr 4 e.a4 =
    ENatValRing.sub_val evr 4 (e.a1 * e.a3 + 2 * 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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 + 2 * ENatValRing.sub_val evr 4 e.a4 =
    ENatValRing.sub_val evr 4 (e.a1 * e.a3 + 2 * e.a4)
Tactic:
exact (pi_scaling_of_b4 evr e h1 h3 h4).symm
State after:
no goals