rintro ⟨P, h⟩
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
⊢ (∃ P, is_local_singular_point evr.valtn e P) →
    is_local_singular_point evr.valtn (move_singular_point_to_origin_iso evr e) (0, 0)
case intro
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
⊢ is_local_singular_point evr.valtn (move_singular_point_to_origin_iso evr e) (0, 0)