diff --git a/src/category_theory/grothendieck.lean b/src/category_theory/grothendieck.lean
index 8320cb4343efb..e472d592b97fd 100644
--- a/src/category_theory/grothendieck.lean
+++ b/src/category_theory/grothendieck.lean
@@ -146,22 +146,31 @@ end
 universe w
 variables (G : C ⥤ Type w)
 
+/-- Auxiliary definition for `grothendieck_Type_to_Cat`, to speed up elaboration. -/
+@[simps]
+def grothendieck_Type_to_Cat_functor : grothendieck (G ⋙ Type_to_Cat) ⥤ G.elements :=
+{ obj := λ X, ⟨X.1, X.2⟩,
+  map := λ X Y f, ⟨f.1, f.2.1.1⟩ }
+
+/-- Auxiliary definition for `grothendieck_Type_to_Cat`, to speed up elaboration. -/
+@[simps]
+def grothendieck_Type_to_Cat_inverse : G.elements ⥤ grothendieck (G ⋙ Type_to_Cat) :=
+{ obj := λ X, ⟨X.1, X.2⟩,
+  map := λ X Y f, ⟨f.1, ⟨⟨f.2⟩⟩⟩ }
+
 /--
 The Grothendieck construction applied to a functor to `Type`
 (thought of as a functor to `Cat` by realising a type as a discrete category)
 is the same as the 'category of elements' construction.
 -/
+@[simps]
 def grothendieck_Type_to_Cat : grothendieck (G ⋙ Type_to_Cat) ≌ G.elements :=
-{ functor :=
-  { obj := λ X, ⟨X.1, X.2⟩,
-    map := λ X Y f, ⟨f.1, f.2.1.1⟩ },
-  inverse :=
-  { obj := λ X, ⟨X.1, X.2⟩,
-    map := λ X Y f, ⟨f.1, ⟨⟨f.2⟩⟩⟩ },
+{ functor := grothendieck_Type_to_Cat_functor G,
+  inverse := grothendieck_Type_to_Cat_inverse G,
   unit_iso := nat_iso.of_components (λ X, by { cases X, exact iso.refl _, })
-    (by { rintro ⟨⟩ ⟨⟩ ⟨base, ⟨⟨f⟩⟩⟩, dsimp at *, subst f, simp, }),
+    (by { rintro ⟨⟩ ⟨⟩ ⟨base, ⟨⟨f⟩⟩⟩, dsimp at *, subst f, ext, simp, }),
   counit_iso := nat_iso.of_components (λ X, by { cases X, exact iso.refl _, })
-    (by { rintro ⟨⟩ ⟨⟩ ⟨f, e⟩, dsimp at *, subst e, simp }),
+    (by { rintro ⟨⟩ ⟨⟩ ⟨f, e⟩, dsimp at *, subst e, ext, simp }),
   functor_unit_iso_comp' := by { rintro ⟨⟩, dsimp, simp, refl, } }
 
 end grothendieck