diff --git a/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean b/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
index 3c4643a34b4abe..bfb94a90719cfa 100644
--- a/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
+++ b/Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
@@ -197,14 +197,13 @@ lemma isCardinalFiltered_preorder (J : Type w) [Preorder J]
       { app a := homOfLE (hj a)
         naturality _ _ _ := rfl }⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular] :
     IsCardinalFiltered κ.ord.ToType κ :=
   isCardinalFiltered_preorder _ _ (fun ι f hs ↦ by
-    have h : Function.Surjective (fun i ↦ (⟨f i, i, rfl⟩ : Set.range f)) := fun _ ↦ by aesop
     contrapose! hs
     rw [← hκ.out.cof_ord, ← Ordinal.cof_toType]
-    refine (Order.cof_le fun j ↦ ?_).trans (Cardinal.mk_le_of_surjective h)
+    refine (Order.cof_le fun j ↦ ?_).trans
+      (Cardinal.mk_le_of_surjective (Set.rangeFactorization_surjective (f := f)))
     obtain ⟨k, hk⟩ := hs j
     exact ⟨_, Set.mem_range_self k, hk.le⟩)