Theorem: Model.b6_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
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ b6 (pi_scaling evr e) = ENatValRing.sub_val evr 6 (b6 e)
Tactic:
simp only [b6, pi_scaling]
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 + 4 * ENatValRing.sub_val evr 6 e.a6 =
    ENatValRing.sub_val evr 6 (e.a3 * e.a3 + 4 * e.a6)

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 + 4 * ENatValRing.sub_val evr 6 e.a6 =
    ENatValRing.sub_val evr 6 (e.a3 * e.a3 + 4 * e.a6)
Tactic:
exact (pi_scaling_of_b6 evr e h3 h6).symm
State after:
no goals