C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso
    (IsLimit.conePointUniqueUpToIso (IsPullback.isLimit (_ : IsKernelPair f (𝟙 X) (𝟙 X))) (IsPullback.isLimit h)).inv
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso a
rw [←
  show _ = a from
    (Category.comp_id _).symm.trans
      ((IsKernelPair.id_of_mono f).isLimit.conePointUniqueUpToIso_inv_comp h.isLimit
        WalkingCospan.left)]
no goals
C : Type u
inst✝¹ : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso
    (IsLimit.conePointUniqueUpToIso (IsPullback.isLimit (_ : IsKernelPair f (𝟙 X) (𝟙 X))) (IsPullback.isLimit h)).inv
infer_instance