. rw [is_local_singular_point_iff]
  simp
  convert this
  simp [move_singular_point_to_origin_iso, Field.move_singular_point_to_origin_iso,
        move_singular_point_to_origin_triple, Field.move_singular_point_to_origin_triple]
  sorry
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_1
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_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
    (Prod.map (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) P)
case intro.refine_1
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_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
    (Prod.map (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) P)