rintro ⟨P, hP⟩
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
⊢ (∃ P, is_singular_point e P) → is_singular_point (move_singular_point_to_origin_iso e) (0, 0)
case intro
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
P : K × K
hP : is_singular_point e P
⊢ is_singular_point (move_singular_point_to_origin_iso e) (0, 0)