no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasInitial C
h : ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f
I A : C
f : A ⟶ I
hI : IsInitial I
this : IsIso (f ≫ IsInitial.to hI (⊥_ C))
⊢ f ≫ IsInitial.to hI (⊥_ C) ≫ inv (f ≫ IsInitial.to hI (⊥_ C)) = 𝟙 A
rw [← assoc, IsIso.hom_inv_id]