sorry
case h.e'_3.h
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)
e_2✝ : Ideal.Quotient.commRing (SurjVal.ideal evr.valtn) = EuclideanDomain.toCommRing
⊢ map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn))
      (rst_triple e ((singular_point_on_special evr e).fst, 0, (singular_point_on_special evr e).snd)) =
    rst_triple (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
      ((Field.singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)).fst, 0,
        (Field.singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)).snd)
no goals