diff --git a/Mathlib/CategoryTheory/Localization/Construction.lean b/Mathlib/CategoryTheory/Localization/Construction.lean
index 66419db1524e1e..c4722f9c7d0740 100644
--- a/Mathlib/CategoryTheory/Localization/Construction.lean
+++ b/Mathlib/CategoryTheory/Localization/Construction.lean
@@ -330,9 +330,7 @@ def unitIso : 𝟭 (W.Localization ⥤ D) ≅ functor W D ⋙ inverse W D :=
     (by
       refine Functor.ext (fun G => ?_) fun G₁ G₂ τ => ?_
       · apply uniq
-        dsimp [Functor]
-        erw [fac]
-        rfl
+        simp [functor, inverse, fac]
       · apply natTrans_hcomp_injective
         ext X
         simp)