Theorem: Model.discr_eq_zero_of_singular (ECTate/Algebra/EllipticCurve/Model.lean)

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

State before:
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
Tactic:
rw [discr_in_jacobian_ideal, h₁, h₂, h₃, mul_zero,
  mul_zero, mul_zero, add_zero, add_zero, neg_eq_zero]
State after:
no goals