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