feat(category_theory/opposites): Add is_iso_op (#9319)

Co-authored-by: erd1 <the.erd.one@gmail.com>
Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>

src/category_theory/opposites.lean

@@ -78,6 +78,11 @@ def op_op_equivalence : Cᵒᵖᵒᵖ ≌ C :=
 
 end
 
+/-- If `f` is an isomorphism, so is `f.op` -/
+instance is_iso_op {X Y : C} (f : X ⟶ Y) [is_iso f] : is_iso f.op :=
+⟨⟨(inv f).op,
+  ⟨quiver.hom.unop_inj (by tidy), quiver.hom.unop_inj (by tidy)⟩⟩⟩
+
 /--
 If `f.op` is an isomorphism `f` must be too.
 (This cannot be an instance as it would immediately loop!)
@@ -86,6 +91,9 @@ lemma is_iso_of_op {X Y : C} (f : X ⟶ Y) [is_iso f.op] : is_iso f :=
 ⟨⟨(inv (f.op)).unop,
   ⟨quiver.hom.op_inj (by simp), quiver.hom.op_inj (by simp)⟩⟩⟩
 
+@[simp] lemma op_inv {X Y : C} (f : X ⟶ Y) [f_iso : is_iso f] : (inv f).op = inv f.op :=
+by { ext, rw [← op_comp, is_iso.inv_hom_id, op_id] }
+
 namespace functor
 
 section