rw [discr_in_jacobian_ideal, h₁, h₂, h₃, mul_zero,
  mul_zero, mul_zero, add_zero, add_zero, neg_eq_zero]
case intro.intro
K : Type u
inst✝ : CommRing K
e : Model K
P : K × K
h₁ : weierstrass e P = 0
h₂ : dweierstrass_dx e P = 0
h₃ : dweierstrass_dy e P = 0
⊢ discr e = 0
no goals