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]
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)
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