case hom_inv_id
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
inst✝ : IsIso α
X : C
⊢ α.app X ≫ (inv α).app X = 𝟙 (F.obj X)
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
inst✝ : IsIso α
X : C
⊢ (inv α).app X = inv (α.app X)
apply IsIso.eq_inv_of_hom_inv_id
case hom_inv_id
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
inst✝ : IsIso α
X : C
⊢ (α ≫ inv α).app X = 𝟙 (F.obj X)
case hom_inv_id
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
inst✝ : IsIso α
X : C
⊢ α.app X ≫ (inv α).app X = 𝟙 (F.obj X)
rw [← NatTrans.comp_app]
no goals
case hom_inv_id
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
inst✝ : IsIso α
X : C
⊢ (α ≫ inv α).app X = 𝟙 (F.obj X)
simp