no goals
C : Type u
inst✝ : Category C
I : C
h : ∀ (A : C) (f : I ⟶ A), IsIso f
I' A : C
f : I' ⟶ A
hI' : IsTerminal I'
this : IsIso (IsTerminal.from hI' I ≫ f)
⊢ (inv (IsTerminal.from hI' I ≫ f) ≫ IsTerminal.from hI' I) ≫ f = 𝟙 A
rw [assoc, IsIso.inv_hom_id]