∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] (X : C) ⦃A B : Cᵒᵖ⦄ (f : A ⟶ Opposite.op X) (g : B ⟶ Opposite.op X)
  [inst_3 : CategoryTheory.Mono f] [inst_4 : CategoryTheory.Mono g] (i : A ≅ B),
  CategoryTheory.CategoryStruct.comp i.hom g = f →
    (fun x f x_1 => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop)) A f inst_3 =
      (fun x f x_1 => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop)) B g inst_4