∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (X : CategoryTheory.Subobject B) (f : A ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (h : X = CategoryTheory.Subobject.mk f),
  (X.isoOfEqMk f h).inv = CategoryTheory.Subobject.ofMkLE f X ⋯