case h
C : Type u_1
inst✝ : Category C
P : Karoubi C
⊢ ((toKaroubi C).map P.p).f = (decompId_p P ≫ decompId_i P).f
C : Type u_1
inst✝ : Category C
P : Karoubi C
⊢ (toKaroubi C).map P.p = decompId_p P ≫ decompId_i P
ext
no goals
case h
C : Type u_1
inst✝ : Category C
P : Karoubi C
⊢ ((toKaroubi C).map P.p).f = (decompId_p P ≫ decompId_i P).f
simp only [comp_f, decompId_p_f, decompId_i_f, P.idem, toKaroubi_map_f]