no goals
C : Type u₁
inst✝ : Category C
X✝ Y✝ X Y : C
f : X ≅ Y
⊢ unop (Iso.op f) = f
(ext; rfl)
case w
C : Type u₁
inst✝ : Category C
X✝ Y✝ X Y : C
f : X ≅ Y
⊢ (unop (Iso.op f)).hom = f.hom
C : Type u₁
inst✝ : Category C
X✝ Y✝ X Y : C
f : X ≅ Y
⊢ unop (Iso.op f) = f
ext
no goals
case w
C : Type u₁
inst✝ : Category C
X✝ Y✝ X Y : C
f : X ≅ Y
⊢ (unop (Iso.op f)).hom = f.hom
rfl