case hom_inv_id
C : Type u₁
inst : Category C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ f.op ≫ (inv f).op = 𝟙 (op Y)
C : Type u₁
inst✝¹ : Category C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (inv f).op = inv f.op
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.op ≫ (inv f).op = 𝟙 (op Y)
rw [← op_comp, IsIso.inv_hom_id, op_id]