rcases h with ⟨h₁, h₂, h₃⟩
K : Type u
inst✝ : CommRing K
e : Model K
P : K × K
h : is_singular_point e P
⊢ discr e = 0
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