simpa
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
no goals