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

State before:
K : Type u
inst✝ : Field K
e : Model K
r t : K
P : K × K
h : is_singular_point e P
⊢ is_singular_point (rst_iso r 0 t e) (var_change (-r) 0 (-t) P)
Tactic:
rw [is_singular_point, weierstrass_iso_eq_var_change,
  dweierstrass_dx_iso_eq_var_change, zero_mul, add_zero,
  dweierstrass_dy_iso_eq_var_change, var_change_comp]
State after:
K : Type u
inst✝ : Field K
e : Model K
r t : K
P : K × K
h : is_singular_point e P
⊢ weierstrass e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0 ∧
    dweierstrass_dx e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0 ∧
      dweierstrass_dy e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0

State before:
K : Type u
inst✝ : Field K
e : Model K
r t : K
P : K × K
h : is_singular_point e P
⊢ weierstrass e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0 ∧
    dweierstrass_dx e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0 ∧
      dweierstrass_dy e (var_change (r + -r) (0 + 0) (t + -t + 0 * -r) P) = 0
Tactic:
simpa
State after:
no goals