diff --git a/.docker/test.lean b/.docker/test.lean
index a851192..888270c 100644
--- a/.docker/test.lean
+++ b/.docker/test.lean
@@ -88,10 +88,11 @@ instance tada3 (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGr
   letI := Module.compHom (⨁ j, 𝓜 j) (ofZeroRingHom 𝒜)
   exact Dfinsupp.single_injective.module (𝒜 0) (of 𝓜 i) (mylem 𝒜 𝓜 i)
 
+  -- (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
+
 noncomputable def hilbert_function (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
   [DirectSum.GCommRing 𝒜]
-  [DirectSum.Gmodule 𝒜 𝓜] (art: IsArtinianRing (𝒜 0)) (loc : LocalRing (𝒜 0))
-  : ℤ → ℕ∞ := fun i => (length (𝒜 0) (𝓜 i))
+  [DirectSum.Gmodule 𝒜 𝓜] (hilb : ℤ → ℕ∞) := ∀ i, hilb i = (length (𝒜 0) (𝓜 i))
 
 lemma hilbertz (𝒜 : ℤ → Type _) (𝓜 : ℤ → Type _) [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
   [DirectSum.GCommRing 𝒜]