Theorem: SurjVal.p_non_zero (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ ¬p = 0
Tactic:
rw [←nav.v_eq_top_iff_zero, nav.v_uniformizer]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ ¬1 = ⊤

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
⊢ ¬1 = ⊤
Tactic:
simp
State after:
no goals