no goals
C : Type u₁
inst✝² : Category C
X Y : C
f : X ⟶ Y
inst✝¹ : IsSplitMono f
inst✝ : Epi f
⊢ f ≫ retraction f = 𝟙 X
simp
no goals
C : Type u₁
inst✝² : Category C
X Y : C
f : X ⟶ Y
inst✝¹ : IsSplitMono f
inst✝ : Epi f
⊢ retraction f ≫ f = 𝟙 Y
simp [← cancel_epi f]