fix

Author: kim-em

Mathlib/CategoryTheory/GlueData.lean

@@ -443,7 +443,7 @@ def GlueData'.t'' (D : GlueData' C) (i j k : D.J) :
   else
     haveI := Ne.symm hij
     pullback.map _ _ _ _ (eqToHom (by aesop)) (eqToHom (by rw [dif_neg hik]))
-        (eqToHom (by aesop)) (by aesop) (by delta f'; aesop) ≫
+        (eqToHom (by aesop)) (by delta f'; aesop) (by delta f'; aesop) ≫
       D.t' i j k hij hik hjk ≫
       pullback.map _ _ _ _ (eqToHom (by aesop)) (eqToHom (by aesop)) (eqToHom (by aesop))
         (by delta f'; aesop) (by delta f'; aesop)