∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} {f : A₁ ⟶ B} {g : A₂ ⟶ B}
  [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g]
  (h : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h) g = f