Theorem: Model.is_local_singular_point_iff (ECTate/Algebra/EllipticCurve/LocalEC.lean)

State before:
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)
Tactic:
rw [is_singular_point, weierstrass_map, dweierstrass_dx_map, dweierstrass_dy_map, is_local_singular_point]
State after:
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

State before:
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
Tactic:
simp [Ideal.Quotient.eq_zero_iff_mem]
State after:
no goals