Theorem: Model.b2_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
⊢ b2 (pi_scaling evr e) = ENatValRing.sub_val evr 2 (b2 e)
Tactic:
simp only [b2, 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
⊢ ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 1 e.a1 + 4 * ENatValRing.sub_val evr 2 e.a2 =
    ENatValRing.sub_val evr 2 (e.a1 * e.a1 + 4 * e.a2)

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
⊢ ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 1 e.a1 + 4 * ENatValRing.sub_val evr 2 e.a2 =
    ENatValRing.sub_val evr 2 (e.a1 * e.a1 + 4 * e.a2)
Tactic:
exact (pi_scaling_of_b2 evr e h1 h2).symm
State after:
no goals