`(m : @Isomorphic C s d) D (F G : Functor C D) (T : NaturalTransformation F G) : (G _1 m)^-1 o (T d o F _1 m) = T s := @path_components_of_isisomorphism _ _ _ m m D F G T.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import NaturalTransformation.Composition.Core. Require Import Functor.Composition.Core. Require Import Category.Morphisms. Require Import FunctorCategory.Core. Require Import NaturalTransformation.Paths. Require Import Basics.Tactics.