Theorem: ValidModel.ofN_val_discr_to_nat (ECTate/Algebra/EllipticCurve/LocalEC.lean)

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
⊢ ↑(val_discr_to_nat valp e) = v valp (Model.discr e.toModel)
Tactic:
simp only [val_discr_to_nat, coe_toNat_eq_self, ne_eq, v_eq_top_iff_zero]
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
⊢ ¬Model.discr e.toModel = 0

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
⊢ ¬Model.discr e.toModel = 0
Tactic:
exact e.discr_not_zero
State after:
no goals