no goals
C : Type u₁
inst✝² : Category C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ f ≫ section_ f = 𝟙 X
simp [← cancel_mono f]
no goals
C : Type u₁
inst✝² : Category C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
inst✝ : IsSplitEpi f
⊢ section_ f ≫ f = 𝟙 Y
simp