feat: port CategoryTheory.Opposites (#2195)

- [x] depends on: #1287
~~- [x] depends on tactic tidy?~~


Co-authored-by: Henrik Böving <hargonix@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

Mathlib.lean

@@ -231,6 +231,7 @@ import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Iso
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
+import Mathlib.CategoryTheory.Opposites
 import Mathlib.CategoryTheory.Sigma.Basic
 import Mathlib.CategoryTheory.Thin
 import Mathlib.CategoryTheory.Whiskering

Mathlib/CategoryTheory/Iso.lean

@@ -140,6 +140,8 @@ def refl (X : C) : X ≅ X where
 
 instance : Inhabited (X ≅ X) := ⟨Iso.refl X⟩
 
+theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) := ⟨default⟩ 
+
 @[simp]
 theorem refl_symm (X : C) : (Iso.refl X).symm = Iso.refl X := rfl
 #align category_theory.iso.refl_symm CategoryTheory.Iso.refl_symm