awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
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
⊢ {
      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 := ⋯ } =
    τ
have 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 := sorry }
      X =
    τ.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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
⊢ { 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
have simp : P.p.f i ≫ P.X.d i j = 0
Tactic: simp only [hom_eq_zero_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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 ≫ (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
have dsimp : P.p.f i ≫ P.p.f i ≫ P.X.d i j = P.X.d i j ≫ P.p.f j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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)
⊢ (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' := ⋯ }
have 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' := sorry :
              (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' := sorry } n
Tactic: ext n
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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 : ι
⊢ ((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
have h : P.p.f n ≫ P.p.f n ≫ P.p.f n = P.p.f n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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
⊢ 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) φ
have h : ∀ (i : ι),
  (CategoryTheory.Functor.map (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) φ ≫
            {
              f :=
                { f := fun (n : ι) ↦ Q.p.f n, comm' := sorry :
                  (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q).X.Hom
                    (CategoryTheory.Functor.obj (functor ⋙ inverse) Q).X },
              comm := sorry :
              (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' := sorry :
                (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X.Hom
                  (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X },
            comm := sorry :
            (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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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 : ι
⊢ (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
have h : φ.f.f i ≫ Q.p.f i = P.p.f i ≫ φ.f.f i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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 ≫ (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
have dsimp : P.p.f i ≫ P.X.d i j = (P.p.f i ≫ P.X.d i j) ≫ P.p.f j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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)
⊢ (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' := ⋯ }
have h : ∀ (n : ι),
  ((CategoryTheory.Functor.obj (functor ⋙ inverse) P).p ≫
          { f := fun (n : ι) ↦ P.p.f n, comm' := sorry :
              (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' := sorry } n
Tactic: ext n
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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 : ι
⊢ ((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
have h : P.p.f n ≫ P.p.f n ≫ P.p.f n = P.p.f n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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
⊢ 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))) φ
have h : ∀ (i : ι),
  (CategoryTheory.Functor.map (functor ⋙ inverse) φ ≫
            {
              f :=
                { f := fun (n : ι) ↦ Q.p.f n, comm' := sorry :
                  (CategoryTheory.Functor.obj (functor ⋙ inverse) Q).X.Hom
                    (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) Q).X },
              comm := sorry :
              (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' := sorry :
                (CategoryTheory.Functor.obj (functor ⋙ inverse) P).X.Hom
                  (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) P).X },
            comm := sorry :
            (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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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 : ι
⊢ (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
have h : φ.f.f i ≫ Q.p.f i = P.p.f i ≫ φ.f.f i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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 ι
⊢ Eq (α :=
    Quiver.Hom (V :=
      Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c) ⥤ Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))
      (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))))
    (CategoryStruct.comp (Y := functor ⋙ inverse)
      {
        app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
          { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
        naturality := ⋯ }
      {
        app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
          { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
        naturality := ⋯ })
    (𝟙 (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))))
have w : ∀ (x : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) (i : ι),
  Eq (α :=
    (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) x).X.X i ⟶
      (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) x).X.X i)
    (HomologicalComplex.Hom.f
      (Hom.f
        (NatTrans.app
          (CategoryStruct.comp (Y := functor ⋙ inverse)
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := sorry }, comm := sorry },
              naturality := sorry }
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := sorry }, comm := sorry },
              naturality := sorry })
          x))
      i)
    (HomologicalComplex.Hom.f (Hom.f (NatTrans.app (𝟙 (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)))) x)) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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 ι
x : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
i : ι
⊢ Eq (α :=
    (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) x).X.X i ⟶
      (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) x).X.X i)
    (HomologicalComplex.Hom.f
      (Hom.f
        (NatTrans.app
          (CategoryStruct.comp (Y := functor ⋙ inverse)
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
              naturality := ⋯ }
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
              naturality := ⋯ })
          x))
      i)
    (HomologicalComplex.Hom.f (Hom.f (NatTrans.app (𝟙 (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)))) x)) i)
have w : x.p.f i ≫ x.p.f i = x.p.f i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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 ι
⊢ Eq (α :=
    Quiver.Hom (V :=
      Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c) ⥤ Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))
      (functor ⋙ inverse) (functor ⋙ inverse))
    (CategoryStruct.comp (Y := 𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)))
      {
        app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
          { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
        naturality := ⋯ }
      {
        app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
          { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
        naturality := ⋯ })
    (𝟙 (functor ⋙ inverse))
have w : ∀ (x : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) (i : ι),
  Eq (α :=
    (CategoryTheory.Functor.obj (functor ⋙ inverse) x).X.X i ⟶ (CategoryTheory.Functor.obj (functor ⋙ inverse) x).X.X i)
    (HomologicalComplex.Hom.f
      (Hom.f
        (NatTrans.app
          (CategoryStruct.comp (Y := 𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)))
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := sorry }, comm := sorry },
              naturality := sorry }
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := sorry }, comm := sorry },
              naturality := sorry })
          x))
      i)
    (HomologicalComplex.Hom.f (Hom.f (NatTrans.app (𝟙 (functor ⋙ inverse)) x)) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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 ι
x : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
i : ι
⊢ Eq (α :=
    (CategoryTheory.Functor.obj (functor ⋙ inverse) x).X.X i ⟶ (CategoryTheory.Functor.obj (functor ⋙ inverse) x).X.X i)
    (HomologicalComplex.Hom.f
      (Hom.f
        (NatTrans.app
          (CategoryStruct.comp (Y := 𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)))
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
              naturality := ⋯ }
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
              naturality := ⋯ })
          x))
      i)
    (HomologicalComplex.Hom.f (Hom.f (NatTrans.app (𝟙 (functor ⋙ inverse)) x)) i)
have w : x.p.f i ≫ x.p.f i = x.p.f i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.HomologicalComplex (goal)
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 ι
α : Type u_3
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete (HomologicalComplex.{v_1, u_1, u_2} C c)
have rw : IsIdempotentComplete (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))
Tactic: rw [isIdempotentComplete_iff_of_equivalence
      ((toKaroubiEquivalence C).mapHomologicalComplex c),
    ← isIdempotentComplete_iff_of_equivalence (karoubiHomologicalComplexEquivalence C c)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
h_X : P.X = Q.X
h_p : P.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ P = Q
have mk : ∀ (X : C) (p : X ⟶ X) (idem : p ≫ p = p) (h_X : { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.X = Q.X)
  (h_p : { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p),
  { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C } = Q
Tactic: cases P
Cleared hypotheses: P, h_X, h_p
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Q : Karoubi.{v_1, u_1} C
X : C
p : X ⟶ X
idem : p ≫ p = p
h_X : { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.X = Q.X
h_p : { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C } = Q
have mk : ∀ (X_1 : C) (p_1 : X_1 ⟶ X_1) (idem_1 : p_1 ≫ p_1 = p_1)
  (h_X :
    { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.X =
      { X := X_1, p := p_1, idem := idem_1 : Karoubi.{v_1, u_1} C }.X)
  (h_p :
    { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.p ≫ eqToHom h_X =
      eqToHom h_X ≫ { X := X_1, p := p_1, idem := idem_1 : Karoubi.{v_1, u_1} C }.p),
  { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C } = { X := X_1, p := p_1, idem := idem_1 }
Tactic: cases Q
Cleared hypotheses: Q, h_X, h_p
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
p : X ⟶ X
idem : p ≫ p = p
X_1 : C
p_1 : X_1 ⟶ X_1
idem_1 : p_1 ≫ p_1 = p_1
h_X : X = X_1
h_p : p ≫ eqToHom h_X = eqToHom h_X ≫ p_1
⊢ { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C } = { X := X_1, p := p_1, idem := idem_1 }
have mk : ∀ (p_2 : X ⟶ X) (idem_2 : p_2 ≫ p_2 = p_2) (h_p : p ≫ eqToHom sorry = eqToHom sorry ≫ p_2),
  { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C } = { X := X, p := p_2, idem := idem_2 }
Tactic: subst h_X
Cleared hypotheses: X_1, p_1, idem_1, h_X, h_p
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
⊢ P.p ≫ 0 ≫ Q.p = 0
have rw : Eq (α := P.X ⟶ Q.X) (P.p ≫ 0) 0
Tactic: rw [zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
rw : Eq (α := P.X ⟶ Q.X) (P.p ≫ 0) 0
⊢ P.p ≫ 0 ≫ Q.p = 0
have rw₁ : Eq.{v_1 + 1} (α := P.X ⟶ Q.X) 0 0
Tactic: rw [zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
⊢ P.p ≫ f.f = f.f
have rw : P.p ≫ P.p ≫ f.f ≫ Q.p = P.p ≫ f.f ≫ Q.p
Tactic: rw [← f.comm, ← assoc, P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Karoubi (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
rw : P.p ≫ P.p ≫ f.f ≫ Q.p = P.p ≫ f.f ≫ Q.p
⊢ P.p ≫ f.f = f.f
have rw₁ : (P.p ≫ P.p) ≫ f.f ≫ Q.p = P.p ≫ f.f ≫ Q.p
Tactic: rw [← f.comm, ← assoc, P.idem]