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

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h : SurjVal.v evr.valtn (discr e) > 0
⊢ ∃ P, is_local_singular_point evr.valtn e P
Tactic:
sorry
State after:
no goals