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

State before:
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
h : is_local_singular_point evr.valtn e (0, 0)
⊢ 0 < SurjVal.v evr.valtn e.a6
Tactic:
simpa [is_local_singular_point, weierstrass] using h.1
State after:
no goals