rw [is_local_singular_point_iff]
case intro.refine_2
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
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
⊢ is_local_singular_point evr.valtn (move_singular_point_to_origin_iso evr e) (0, 0)
case intro.refine_2
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
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
⊢ is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (move_singular_point_to_origin_iso evr e))
    (Prod.map ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (0, 0))