rw [←p2]
case inl.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 1 ≤ v valp 2
case inl.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 1 ≤ v valp p