no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DiscreteValuationRing R
r : R
u : Rˣ
ϖ : R
hϖ : Irreducible ϖ
n : ℕ
hr : r = ↑u * ϖ ^ n
⊢ ↑(addVal R) r = ↑n
rw [addVal, addValuation_apply, hr, eq_of_associated_left
    (associated_of_irreducible R hϖ (Classical.choose_spec (exists_prime R)).irreducible),
  eq_of_associated_right (Associated.symm ⟨u, mul_comm _ _⟩),
  multiplicity_pow_self_of_prime (PrincipalIdealRing.irreducible_iff_prime.1 hϖ)]