awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ :
  obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) F ⟶
    obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) G
X : C
w :
  τ.app X ≫
      G.map
        (𝟙
          { X := Karoubi.X.{v_1, u_1} (obj (toKaroubi C) X), p := 𝟙 (Karoubi.X.{v_1, u_1} (obj (toKaroubi C) X)),
            idem := ⋯ : Karoubi.{v_1, u_1} C }) =
    τ.app X
⊢ F.map (decompId_i (obj (toKaroubi C) X)) ≫ τ.app X ≫ G.map (decompId_p (obj (toKaroubi C) X)) = τ.app X

Tactic:
rw [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi,
      Functor.map_id, Category.id_comp]

Premises used: CategoryTheory.Idempotents.Karoubi.decompId_i_toKaroubi, CategoryTheory.Functor.map_id, CategoryTheory.Idempotents.Karoubi.decompId_p_toKaroubi, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ :
  obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) F ⟶
    obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) G
X : C
w : τ.app X ≫ G.map (𝟙 (obj (toKaroubi C) X)) = τ.app X
⊢ τ.app X ≫
      G.map
        (𝟙
          { X := Karoubi.X.{v_1, u_1} (obj (toKaroubi C) X), p := 𝟙 (Karoubi.X.{v_1, u_1} (obj (toKaroubi C) X)),
            idem := ⋯ : Karoubi.{v_1, u_1} C }) =
    τ.app X

Tactic:
change _ ≫ G.map (𝟙 _) = _

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ :
  obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) F ⟶
    obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) G
X : C
⊢ τ.app X ≫ G.map (𝟙 (obj (toKaroubi C) X)) = τ.app X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : F ⟶ G
w :
  ∀ (X : Karoubi.{v_1, u_1} C),
    NatTrans.app
        {
          app := fun (P : Karoubi.{v_1, u_1} C) ↦
            F.map P.decompId_i ≫
              NatTrans.app (map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ) P.X ≫
                G.map P.decompId_p,
          naturality := ⋯ }
        X =
      τ.app X
⊢ {
      app := fun (P : Karoubi.{v_1, u_1} C) ↦
        F.map P.decompId_i ≫
          NatTrans.app (map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ) P.X ≫ G.map P.decompId_p,
      naturality := ⋯ } =
    τ

Tactic:
ext X

Premises used: CategoryTheory.Idempotents.Karoubi.X
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : F ⟶ G
X : Karoubi.{v_1, u_1} C
⊢ NatTrans.app
      {
        app := fun (P : Karoubi.{v_1, u_1} C) ↦
          F.map P.decompId_i ≫
            NatTrans.app (map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ) P.X ≫
              G.map P.decompId_p,
        naturality := ⋯ }
      X =
    τ.app X

Tactic:
(natTrans_eq _ _).symm

Premises used: CategoryTheory.Idempotents.natTrans_eq, Eq.symm
-- Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : F ⟶ G
X : Karoubi.{v_1, u_1} C
⊢ NatTrans.app
      {
        app := fun (P : Karoubi.{v_1, u_1} C) ↦
          F.map P.decompId_i ≫
            NatTrans.app (map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ) P.X ≫
              G.map P.decompId_p,
        naturality := ⋯ }
      X =
    τ.app X

Tactic:
exact (natTrans_eq _ _).symm

Premises used: CategoryTheory.Idempotents.natTrans_eq, Eq.symm
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
f : P ⟶ Q
n : ι
⊢ P.p.f n ≫ f.f.f n = f.f.f n

Tactic:
HomologicalComplex.congr_hom (p_comp f) n

Premises used: CategoryTheory.Idempotents.Karoubi.p_comp, HomologicalComplex.congr_hom
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
f : P ⟶ Q
n : ι
⊢ f.f.f n ≫ Q.p.f n = f.f.f n

Tactic:
HomologicalComplex.congr_hom (comp_p f) n

Premises used: CategoryTheory.Idempotents.Karoubi.comp_p, HomologicalComplex.congr_hom
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
f : P ⟶ Q
n : ι
⊢ P.p.f n ≫ f.f.f n = f.f.f n ≫ Q.p.f n

Tactic:
HomologicalComplex.congr_hom (p_comm f) n

Premises used: HomologicalComplex.congr_hom, CategoryTheory.Idempotents.Karoubi.p_comm
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
n : ι
⊢ P.p.f n ≫ P.p.f n = P.p.f n

Tactic:
HomologicalComplex.congr_hom P.idem n

Premises used: CategoryTheory.Idempotents.Karoubi.idem, HomologicalComplex.congr_hom
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
n : ι
⊢ P.p.f n ≫ P.p.f n = P.p.f n

Tactic:
simpa only [HomologicalComplex.comp_f] using HomologicalComplex.congr_hom P.idem n

Premises used: HomologicalComplex.comp_f, CategoryTheory.Idempotents.Karoubi.idem, HomologicalComplex.congr_hom
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
i j : ι
hij : ¬c.Rel i j
simp : P.p.f i ≫ P.X.d i j = 0
⊢ { f := P.p.f i ≫ P.X.d i j, comm := ⋯ :
      { X := P.X.X i, p := P.p.f i, idem := ⋯ : Karoubi.{v_1, u_1} C }.Hom
        { X := P.X.X j, p := P.p.f j, idem := ⋯ : Karoubi.{v_1, u_1} C } } =
    0

Tactic:
simp only [hom_eq_zero_iff]

Premises used: CategoryTheory.Idempotents.Karoubi.hom_eq_zero_iff
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex (Karoubi.{v_1, u_1} C) c
i j k : ι
h : c.Rel i j
h_1 : c.Rel j k
⊢ (K.d i j).f ≫ (K.d j k).f = 0

Tactic:
simpa only [comp_f] using hom_eq_zero_iff.mp (K.d_comp_d i j k)

Premises used: CategoryTheory.Idempotents.Karoubi.hom_eq_zero_iff, CategoryTheory.Idempotents.Karoubi.comp_f, Iff.mp, HomologicalComplex.d_comp_d
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex (Karoubi.{v_1, u_1} C) c
f : K ⟶ L
i j : ι
hij : c.Rel i j
⊢ (f.f i).f ≫ (obj L).X.d i j = (obj K).X.d i j ≫ (f.f j).f

Tactic:
simpa only [comp_f] using hom_ext_iff.mp (f.comm' i j hij)

Premises used: CategoryTheory.Idempotents.Karoubi.comp_f, Iff.mp, HomologicalComplex.Hom.comm', CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : HomologicalComplex (Karoubi.{v_1, u_1} C) c
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  (CategoryTheory.Functor.obj (inverse ⋙ functor) P).X =
    (CategoryTheory.Functor.obj (𝟭 (HomologicalComplex (Karoubi.{v_1, u_1} C) c)) P).X
⊢ (CategoryTheory.Functor.obj (inverse ⋙ functor) P).X =
    (CategoryTheory.Functor.obj (𝟭 (HomologicalComplex (Karoubi.{v_1, u_1} C) c)) P).X

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : HomologicalComplex (Karoubi.{v_1, u_1} C) c
⊢ ∀ (i j : ι),
    c.Rel i j →
      (CategoryTheory.Functor.obj (inverse ⋙ functor) P).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ (CategoryTheory.Functor.obj (𝟭 (HomologicalComplex (Karoubi.{v_1, u_1} C) c)) P).d i j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
i j : ι
h : c.Rel i j
dsimp : P.p.f i ≫ P.p.f i ≫ P.X.d i j = P.X.d i j ≫ P.p.f j
⊢ P.p.f i ≫ (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X.d i j =
    (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X.d i j ≫ P.p.f j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
i j : ι
h : c.Rel i j
⊢ P.p.f i ≫ P.p.f i ≫ P.X.d i j = P.X.d i j ≫ P.p.f j

Tactic:
simp only [HomologicalComplex.Hom.comm, HomologicalComplex.Hom.comm_assoc,
                  HomologicalComplex.p_idem]

Premises used: CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem, HomologicalComplex.Hom.comm_assoc, HomologicalComplex.Hom.comm
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
h :
  ∀ (n : ι),
    ((CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).p ≫
            { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
                (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X.Hom
                  (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X } ≫
              (CategoryTheory.Functor.obj (functor ⋙ inverse) P).p).f
        n =
      HomologicalComplex.Hom.f { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ } n
⊢ (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).p ≫
      { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
          (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X.Hom
            (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X } ≫
        (CategoryTheory.Functor.obj (functor ⋙ inverse) P).p =
    { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }

Tactic:
ext n
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
n : ι
h : P.p.f n ≫ P.p.f n ≫ P.p.f n = P.p.f n
⊢ ((CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).p ≫
          { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
              (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X.Hom
                (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X } ≫
            (CategoryTheory.Functor.obj (functor ⋙ inverse) P).p).f
      n =
    HomologicalComplex.Hom.f { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ } n

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
n : ι
⊢ P.p.f n ≫ P.p.f n ≫ P.p.f n = P.p.f n

Tactic:
simp only [HomologicalComplex.p_idem]

Premises used: CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : P ⟶ Q
h :
  ∀ (i : ι),
    (CategoryTheory.Functor.map (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) φ ≫
              {
                f :=
                  { f := fun (n : ι) ↦ Q.p.f n, comm' := ⋯ :
                    (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q).X.Hom
                      (CategoryTheory.Functor.obj (functor ⋙ inverse) Q).X },
                comm := ⋯ :
                (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q).Hom
                  (CategoryTheory.Functor.obj (functor ⋙ inverse) Q) }).f.f
        i =
      HomologicalComplex.Hom.f
        (Hom.f
          ({
              f :=
                { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
                  (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X.Hom
                    (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X },
              comm := ⋯ :
              (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).Hom
                (CategoryTheory.Functor.obj (functor ⋙ inverse) P) } ≫
            CategoryTheory.Functor.map (functor ⋙ inverse) φ))
        i
⊢ CategoryTheory.Functor.map (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) φ ≫
      {
        f :=
          { f := fun (n : ι) ↦ Q.p.f n, comm' := ⋯ :
            (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q).X.Hom
              (CategoryTheory.Functor.obj (functor ⋙ inverse) Q).X },
        comm := ⋯ :
        (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q).Hom
          (CategoryTheory.Functor.obj (functor ⋙ inverse) Q) } =
    {
        f :=
          { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
            (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X.Hom
              (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X },
        comm := ⋯ :
        (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).Hom
          (CategoryTheory.Functor.obj (functor ⋙ inverse) P) } ≫
      CategoryTheory.Functor.map (functor ⋙ inverse) φ

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : P ⟶ Q
i : ι
h : φ.f.f i ≫ Q.p.f i = P.p.f i ≫ φ.f.f i
⊢ (CategoryTheory.Functor.map (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) φ ≫
            {
              f :=
                { f := fun (n : ι) ↦ Q.p.f n, comm' := ⋯ :
                  (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q).X.Hom
                    (CategoryTheory.Functor.obj (functor ⋙ inverse) Q).X },
              comm := ⋯ :
              (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q).Hom
                (CategoryTheory.Functor.obj (functor ⋙ inverse) Q) }).f.f
      i =
    HomologicalComplex.Hom.f
      (Hom.f
        ({
            f :=
              { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
                (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X.Hom
                  (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X },
            comm := ⋯ :
            (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).Hom
              (CategoryTheory.Functor.obj (functor ⋙ inverse) P) } ≫
          CategoryTheory.Functor.map (functor ⋙ inverse) φ))
      i

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : P ⟶ Q
i : ι
⊢ φ.f.f i ≫ Q.p.f i = P.p.f i ≫ φ.f.f i

Tactic:
simp only [HomologicalComplex.comp_p_d,
          HomologicalComplex.p_comp_d]

Premises used: CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
i j : ι
h : c.Rel i j
dsimp : P.p.f i ≫ P.X.d i j = (P.p.f i ≫ P.X.d i j) ≫ P.p.f j
⊢ P.p.f i ≫ (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X.d i j =
    (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X.d i j ≫ P.p.f j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
i j : ι
h : c.Rel i j
⊢ P.p.f i ≫ P.X.d i j = (P.p.f i ≫ P.X.d i j) ≫ P.p.f j

Tactic:
simp only [HomologicalComplex.Hom.comm, assoc, HomologicalComplex.p_idem]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem, HomologicalComplex.Hom.comm
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
h :
  ∀ (n : ι),
    ((CategoryTheory.Functor.obj (functor ⋙ inverse) P).p ≫
            { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
                (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X.Hom
                  (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X } ≫
              (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).p).f
        n =
      HomologicalComplex.Hom.f { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ } n
⊢ (CategoryTheory.Functor.obj (functor ⋙ inverse) P).p ≫
      { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
          (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X.Hom
            (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X } ≫
        (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).p =
    { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }

Tactic:
ext n
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
n : ι
h : P.p.f n ≫ P.p.f n ≫ P.p.f n = P.p.f n
⊢ ((CategoryTheory.Functor.obj (functor ⋙ inverse) P).p ≫
          { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
              (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X.Hom
                (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X } ≫
            (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).p).f
      n =
    HomologicalComplex.Hom.f { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ } n

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : P ⟶ Q
h :
  ∀ (i : ι),
    (CategoryTheory.Functor.map (functor ⋙ inverse) φ ≫
              {
                f :=
                  { f := fun (n : ι) ↦ Q.p.f n, comm' := ⋯ :
                    (CategoryTheory.Functor.obj (functor ⋙ inverse) Q).X.Hom
                      (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q).X },
                comm := ⋯ :
                (CategoryTheory.Functor.obj (functor ⋙ inverse) Q).Hom
                  (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q) }).f.f
        i =
      HomologicalComplex.Hom.f
        (Hom.f
          ({
              f :=
                { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
                  (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X.Hom
                    (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X },
              comm := ⋯ :
              (CategoryTheory.Functor.obj (functor ⋙ inverse) P).Hom
                (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P) } ≫
            CategoryTheory.Functor.map (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) φ))
        i
⊢ CategoryTheory.Functor.map (functor ⋙ inverse) φ ≫
      {
        f :=
          { f := fun (n : ι) ↦ Q.p.f n, comm' := ⋯ :
            (CategoryTheory.Functor.obj (functor ⋙ inverse) Q).X.Hom
              (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q).X },
        comm := ⋯ :
        (CategoryTheory.Functor.obj (functor ⋙ inverse) Q).Hom
          (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q) } =
    {
        f :=
          { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
            (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X.Hom
              (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X },
        comm := ⋯ :
        (CategoryTheory.Functor.obj (functor ⋙ inverse) P).Hom
          (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P) } ≫
      CategoryTheory.Functor.map (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) φ

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : P ⟶ Q
i : ι
h : φ.f.f i ≫ Q.p.f i = P.p.f i ≫ φ.f.f i
⊢ (CategoryTheory.Functor.map (functor ⋙ inverse) φ ≫
            {
              f :=
                { f := fun (n : ι) ↦ Q.p.f n, comm' := ⋯ :
                  (CategoryTheory.Functor.obj (functor ⋙ inverse) Q).X.Hom
                    (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q).X },
              comm := ⋯ :
              (CategoryTheory.Functor.obj (functor ⋙ inverse) Q).Hom
                (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q) }).f.f
      i =
    HomologicalComplex.Hom.f
      (Hom.f
        ({
            f :=
              { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ :
                (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X.Hom
                  (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X },
            comm := ⋯ :
            (CategoryTheory.Functor.obj (functor ⋙ inverse) P).Hom
              (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P) } ≫
          CategoryTheory.Functor.map (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) φ))
      i

Tactic:
dsimp