no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
ϖ : R
hϖ : Irreducible ϖ
⊢ ↑(addVal R) ϖ = 1
simpa only [one_mul, eq_self_iff_true, Units.val_one, pow_one, forall_true_left, Nat.cast_one]
  using addVal_def ϖ 1 hϖ 1