rw [is_singular_point, weierstrass_map, dweierstrass_dx_map, dweierstrass_dy_map, is_local_singular_point]
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
P : R × R
⊢ is_local_singular_point evr.valtn e P ↔
    is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
      (Prod.map (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) P)
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
P : R × R
⊢ SurjVal.v evr.valtn (weierstrass e P) > 0 ∧
      SurjVal.v evr.valtn (dweierstrass_dx e P) > 0 ∧ SurjVal.v evr.valtn (dweierstrass_dy e P) > 0 ↔
    ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (weierstrass e P) = 0 ∧
      ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (dweierstrass_dx e P) = 0 ∧
        ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (dweierstrass_dy e P) = 0