case hom_inv_id
C : Type u₁
inst : Category C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso f
⊢ f.unop ≫ (inv f).unop = 𝟙 Y.unop
C : Type u₁
inst✝¹ : Category C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : IsIso f
⊢ (inv f).unop = inv f.unop
aesop_cat_nonterminal
no goals
case hom_inv_id
C : Type u₁
inst : Category C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso f
⊢ f.unop ≫ (inv f).unop = 𝟙 Y.unop
rw [← unop_comp, IsIso.inv_hom_id, unop_id]