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
⊢ (∃ P, is_singular_point e P) → is_singular_point (move_singular_point_to_origin_iso e) (0, 0)
Tactic:
rintro ⟨P, hP⟩
State after:
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)

State before:
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)
Tactic:
have hd := discr_eq_zero_of_singular e hP
State after:
case intro
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
P : K × K
hP : is_singular_point e P
hd : discr e = 0
⊢ is_singular_point (move_singular_point_to_origin_iso e) (0, 0)

State before:
case intro
K : Type u
inst✝¹ : Field K
inst✝ : ECTate.PerfectRing K
e : Model K
P : K × K
hP : is_singular_point e P
hd : discr e = 0
⊢ is_singular_point (move_singular_point_to_origin_iso e) (0, 0)
Tactic:
exact move_singular_point_to_origin e hd
State after:
no goals