diff --git a/Mathlib/Computability/Primrec/Basic.lean b/Mathlib/Computability/Primrec/Basic.lean
index 61c53174774896..f6b05af0e0b160 100644
--- a/Mathlib/Computability/Primrec/Basic.lean
+++ b/Mathlib/Computability/Primrec/Basic.lean
@@ -843,7 +843,7 @@ theorem mem_range_encode : PrimrecPred (fun n => n ∈ Set.range (encode : α 
   this.of_eq fun _ => decode₂_ne_none_iff
 
 instance ulower : Primcodable (ULower α) :=
-  Primcodable.subtype mem_range_encode
+  fast_instance% Primcodable.subtype mem_range_encode
 
 end ULower
 
@@ -886,11 +886,11 @@ theorem option_get {f : α → Option β} {h : ∀ a, (f a).isSome} :
 
 theorem ulower_down : Primrec (ULower.down : α → ULower α) :=
   letI : ∀ a, Decidable (a ∈ Set.range (encode : α → ℕ)) := decidableRangeEncode _
-  subtype_mk .encode
+  subtype_mk .encode (hp := Primcodable.mem_range_encode)
 
 theorem ulower_up : Primrec (ULower.up : ULower α → α) :=
   letI : ∀ a, Decidable (a ∈ Set.range (encode : α → ℕ)) := decidableRangeEncode _
-  option_get (Primrec.decode₂.comp subtype_val)
+  option_get (Primrec.decode₂.comp (subtype_val (hp := Primcodable.mem_range_encode)))
 
 theorem fin_val_iff {n} {f : α → Fin n} : (Primrec fun a => (f a).1) ↔ Primrec f := by
   letI : Primcodable { a // a < n } := Primcodable.subtype (nat_lt.comp .id (const _))
diff --git a/Mathlib/Computability/Primrec/List.lean b/Mathlib/Computability/Primrec/List.lean
index 35be6053f3d64c..1305c4a235f6a9 100644
--- a/Mathlib/Computability/Primrec/List.lean
+++ b/Mathlib/Computability/Primrec/List.lean
@@ -516,7 +516,7 @@ variable {α : Type*} [Primcodable α]
 open Primrec
 
 instance vector {n} : Primcodable (List.Vector α n) :=
-  subtype ((@Primrec.eq ℕ _).comp list_length (const _))
+  fast_instance% subtype ((@Primrec.eq ℕ _).comp list_length (const _))
 
 instance finArrow {n} : Primcodable (Fin n → α) :=
   ofEquiv _ (Equiv.vectorEquivFin _ _).symm
@@ -529,11 +529,11 @@ variable {α : Type*} {β : Type*} {σ : Type*}
 variable [Primcodable α] [Primcodable β] [Primcodable σ]
 
 theorem vector_toList {n} : Primrec (@List.Vector.toList α n) :=
-  subtype_val
+  subtype_val (hp := (@Primrec.eq ℕ _).comp list_length (const _))
 
 theorem vector_toList_iff {n} {f : α → List.Vector β n} :
     (Primrec fun a => (f a).toList) ↔ Primrec f :=
-  subtype_val_iff
+  subtype_val_iff (hp := (@Primrec.eq ℕ _).comp list_length (const _))
 
 theorem vector_cons {n} : Primrec₂ (@List.Vector.cons α n) :=
   vector_toList_iff.1 <| by simpa using list_cons.comp fst (vector_toList_iff.2 snd)