no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
E : Type u₃
inst✝¹ : Category E
F G : C ⥤ D
X Y : C
α : F ⟶ G
f : X ⟶ Y
inst✝ : IsIso (α.app X)
⊢ inv (α.app X) ≫ F.map f ≫ α.app Y = G.map f
simp