case hom_inv_id
C : Type u
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)
C : Type u
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map (inv f) = inv (F.map f)
apply eq_inv_of_hom_inv_id
no goals
case hom_inv_id
C : Type u
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map f ≫ F.map (inv f) = 𝟙 (F.obj X)
simp [← F.map_comp]