[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f ≫ P.p.f = P.p.f
[PROOFSTEP]
simpa only [hom_ext_iff, comp_f] using P.idem
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi (Karoubi C)
f : P ⟶ Q
⊢ P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f
[PROOFSTEP]
simpa only [hom_ext_iff, comp_f] using p_comm f
[GOAL]
C : Type u_1
inst✝ : Category.{?u.1759, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f ≫ P.p.f = P.p.f
[PROOFSTEP]
simpa only [hom_ext_iff] using P.idem
[GOAL]
C : Type u_1
inst✝ : Category.{?u.1759, u_1} C
X✝ Y✝ : Karoubi (Karoubi C)
f : X✝ ⟶ Y✝
⊢ f.f.f = ((fun P => Karoubi.mk P.X.X P.p.f) X✝).p ≫ f.f.f ≫ ((fun P => Karoubi.mk P.X.X P.p.f) Y✝).p
[PROOFSTEP]
simpa only [hom_ext_iff] using f.comm
[GOAL]
C : Type u_1
inst✝ : Category.{?u.7379, u_1} C
⊢ ∀ (X : Karoubi C), (𝟭 (Karoubi C)).obj X = (toKaroubi (Karoubi C) ⋙ inverse C).obj X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.7379, u_1} C
⊢ ∀ (X Y : Karoubi C) (f : X ⟶ Y),
    (𝟭 (Karoubi C)).map f =
      eqToHom (_ : (𝟭 (Karoubi C)).obj X = (toKaroubi (Karoubi C) ⋙ inverse C).obj X) ≫
        (toKaroubi (Karoubi C) ⋙ inverse C).map f ≫
          eqToHom (_ : (toKaroubi (Karoubi C) ⋙ inverse C).obj Y = (𝟭 (Karoubi C)).obj Y)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11252, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f = ((inverse C ⋙ toKaroubi (Karoubi C)).obj P).X.p ≫ P.p.f ≫ ((𝟭 (Karoubi (Karoubi C))).obj P).X.p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11252, u_1} C
P : Karoubi (Karoubi C)
⊢ Hom.mk P.p.f = ((inverse C ⋙ toKaroubi (Karoubi C)).obj P).p ≫ Hom.mk P.p.f ≫ ((𝟭 (Karoubi (Karoubi C))).obj P).p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11252, u_1} C
P : Karoubi (Karoubi C)
⊢ P.p.f = ((𝟭 (Karoubi (Karoubi C))).obj P).X.p ≫ P.p.f ≫ ((inverse C ⋙ toKaroubi (Karoubi C)).obj P).X.p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.11252, u_1} C
P : Karoubi (Karoubi C)
⊢ Hom.mk P.p.f = ((𝟭 (Karoubi (Karoubi C))).obj P).p ≫ Hom.mk P.p.f ≫ ((inverse C ⋙ toKaroubi (Karoubi C)).obj P).p
[PROOFSTEP]
simp
