Theorem: Model.Field.move_singular_point_to_origin (ECTate/Algebra/EllipticCurve/Model.lean)

State before:
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)
Tactic:
rw [move_singular_point_to_origin_iso, rst_triple, move_singular_point_to_origin_triple]
State after:
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)

State before:
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)
Tactic:
convert move_singular_point e (singular_point e).fst (singular_point e).snd
  (is_singular_point_singular_point e h) using 2 <;> simp [var_change]
State after:
no goals