rw [move_singular_point_to_origin_iso, rst_triple, move_singular_point_to_origin_triple]
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
⊢ is_singular_point (move_singular_point_to_origin_iso e) (0, 0)
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
h : discr e = 0
⊢ is_singular_point
    (rst_iso ((singular_point e).fst, 0, (singular_point e).snd).fst
      ((singular_point e).fst, 0, (singular_point e).snd).snd.fst
      ((singular_point e).fst, 0, (singular_point e).snd).snd.snd e)
    (0, 0)