chore: remove note about non-instance (#29525)

The linked issue has been closed, let's see if this is okay now.

Author: kim-em

Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean

@@ -140,15 +140,9 @@ theorem exists_eq_pow_p_mul' (a : 𝕎 k) (ha : a ≠ 0) :
   have hb₀ : b.coeff 0 = b₀ := rfl
   exact ⟨m, mkUnit hb₀, h₂⟩
 
-/-
-Note: The following lemma should be an instance, but it seems to cause some
-exponential blowups in certain typeclass resolution problems.
-See the following Lean4 issue as well as the zulip discussion linked there:
-https://github.com/leanprover/lean4/issues/1102
--/
 /-- The ring of Witt Vectors of a perfect field of positive characteristic is a DVR.
 -/
-theorem isDiscreteValuationRing : IsDiscreteValuationRing (𝕎 k) :=
+instance isDiscreteValuationRing : IsDiscreteValuationRing (𝕎 k) :=
   IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization (by
     refine ⟨p, irreducible p, fun {x} hx => ?_⟩
     obtain ⟨n, b, hb⟩ := exists_eq_pow_p_mul' x hx