case h.e'_1.h.e'_3.h
C : Type u
inst✝¹ : Category C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f = f ≫ 𝟙 Y
C : Type u
inst✝¹ : Category C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f ≫ h = f ↔ h = 𝟙 Y
convert cancel_epi f
no goals
case h.e'_1.h.e'_3.h
C : Type u
inst✝¹ : Category C
X Y Z : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f = f ≫ 𝟙 Y
simp