no goals
C : Type u₁
inst✝¹ : Category C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f ≫ hf.section_ = hf.section_
simp
no goals
C : Type u₁
inst✝¹ : Category C
X Y : C
f : X ⟶ Y
hf : SplitEpi f
inst✝ : Epi hf.section_
⊢ hf.section_ ≫ f = 𝟙 Y
simp