C : Type u_1
inst✝ : Category C
P : Karoubi C
⊢ (eqToHom (_ : P = P)).f = P.p ≫ eqToHom (_ : P.X = P.X)
C : Type u_1
inst✝ : Category C
P Q : Karoubi C
h : P = Q
⊢ (eqToHom h).f = P.p ≫ eqToHom (_ : P.X = Q.X)
subst h
no goals
C : Type u_1
inst✝ : Category C
P : Karoubi C
⊢ (eqToHom (_ : P = P)).f = P.p ≫ eqToHom (_ : P.X = P.X)
simp only [eqToHom_refl, Karoubi.id_eq, comp_id]