cases hp with
| inl p2 =>
  rw [(show (12 : R) = 2 * 6 by norm_num)]
  apply val_mul_ge_of_left_ge
  rw [←p2]
  exact le_of_eq (valp.v_uniformizer).symm
| inr p3 =>
  rw [(show (12 : R) = 3 * 4 by norm_num)]
  apply val_mul_ge_of_left_ge
  rw [←p3]
  exact le_of_eq (valp.v_uniformizer).symm
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
hp : p = 2 ∨ p = 3
valp : SurjVal p
⊢ v valp 12 ≥ 1
no goals