case h
C : Type u_1
inst✝ : Category C
P : Karoubi C
⊢ (𝟙 P).f = (decompId_i P ≫ decompId_p P).f
C : Type u_1
inst✝ : Category C
P : Karoubi C
⊢ 𝟙 P = decompId_i P ≫ decompId_p P
ext
no goals
case h
C : Type u_1
inst✝ : Category C
P : Karoubi C
⊢ (𝟙 P).f = (decompId_i P ≫ decompId_p P).f
simp only [comp_f, id_eq, P.idem, decompId_i, decompId_p]