C : Type u
inst✝² : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ IsPullback a a f f
C : Type u
inst✝² : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ IsKernelPair f a a
change IsPullback _ _ _ _
case h.e'_8
C : Type u
inst✝² : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ a = a ≫ 𝟙 X

case h.e'_9
C : Type u
inst✝² : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ f = 𝟙 X ≫ f
C : Type u
inst✝² : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ IsPullback a a f f
convert (IsPullback.of_horiz_isIso ⟨(rfl : a ≫ 𝟙 X = _ )⟩).paste_vert (IsKernelPair.id_of_mono f)
no goals
case h.e'_8
C : Type u
inst✝² : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ a = a ≫ 𝟙 X

case h.e'_9
C : Type u
inst✝² : Category C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ f = 𝟙 X ≫ f
all_goals { simp }