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 Y)
⊢ α.app X ≫ G.map f ≫ inv (α.app Y) = F.map f
rw [← Category.assoc, ← naturality, Category.assoc, IsIso.hom_inv_id, Category.comp_id]