[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4011, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ HomologicalComplex.Hom.f P.p n ≫ HomologicalComplex.Hom.f P.p n = HomologicalComplex.Hom.f P.p n
[PROOFSTEP]
simpa only [HomologicalComplex.comp_f] using HomologicalComplex.congr_hom P.idem n
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4011, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ (fun i j => Hom.mk (HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.d P.X i j)) i j = 0
[PROOFSTEP]
simp only [hom_eq_zero_iff, P.X.shape i j hij, Limits.comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4011, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.d P.X i j = 0
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.12005, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex (Karoubi C) c
i j k : ι
x✝¹ : ComplexShape.Rel c i j
x✝ : ComplexShape.Rel c j k
⊢ (fun i j => (HomologicalComplex.d K i j).f) i j ≫ (fun i j => (HomologicalComplex.d K i j).f) j k = 0
[PROOFSTEP]
simpa only [comp_f] using hom_eq_zero_iff.mp (K.d_comp_d i j k)
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.17622, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex (Karoubi C) c
f : K ⟶ L
i j : ι
hij : ComplexShape.Rel c i j
⊢ (fun n => (HomologicalComplex.Hom.f f n).f) i ≫ HomologicalComplex.d (obj L).X i j =
    HomologicalComplex.d (obj K).X i j ≫ (fun n => (HomologicalComplex.Hom.f f n).f) j
[PROOFSTEP]
simpa only [comp_f] using hom_ext_iff.mp (f.comm' i j hij)
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.22640, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : HomologicalComplex (Karoubi C) c
⊢ ((inverse ⋙ functor).obj P).X = ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P).X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.22640, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : HomologicalComplex (Karoubi C) c
⊢ ∀ (i j : ι),
    ComplexShape.Rel c i j →
      HomologicalComplex.d ((inverse ⋙ functor).obj P) i j ≫
          eqToHom
            (_ :
              HomologicalComplex.X ((inverse ⋙ functor).obj P) j =
                HomologicalComplex.X ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P) j) =
        eqToHom
            (_ :
              HomologicalComplex.X ((inverse ⋙ functor).obj P) i =
                HomologicalComplex.X ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P) i) ≫
          HomologicalComplex.d ((𝟭 (HomologicalComplex (Karoubi C) c)).obj P) i j
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.22640, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ ∀ (X Y : HomologicalComplex (Karoubi C) c) (f : X ⟶ Y),
    (inverse ⋙ functor).map f =
      eqToHom (_ : (inverse ⋙ functor).obj X = (𝟭 (HomologicalComplex (Karoubi C) c)).obj X) ≫
        (𝟭 (HomologicalComplex (Karoubi C) c)).map f ≫
          eqToHom (_ : (𝟭 (HomologicalComplex (Karoubi C) c)).obj Y = (inverse ⋙ functor).obj Y)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun n => HomologicalComplex.Hom.f P.p n) i ≫ HomologicalComplex.d ((functor ⋙ inverse).obj P).X i j =
    HomologicalComplex.d ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).X i j ≫
      (fun n => HomologicalComplex.Hom.f P.p n) j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.d P.X i j =
    HomologicalComplex.d P.X i j ≫ HomologicalComplex.Hom.f P.p j
[PROOFSTEP]
simp only [HomologicalComplex.Hom.comm, HomologicalComplex.Hom.comm_assoc, HomologicalComplex.p_idem]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
⊢ (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) =
    ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p ≫
      (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) ≫ ((functor ⋙ inverse).obj P).p
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ HomologicalComplex.Hom.f (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) n =
    HomologicalComplex.Hom.f
      (((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p ≫
        (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) ≫ ((functor ⋙ inverse).obj P).p)
      n
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ HomologicalComplex.Hom.f P.p n =
    HomologicalComplex.Hom.f P.p n ≫ HomologicalComplex.Hom.f P.p n ≫ HomologicalComplex.Hom.f P.p n
[PROOFSTEP]
simp only [HomologicalComplex.p_idem]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
⊢ (𝟭 (Karoubi (HomologicalComplex C c))).map φ ≫
      (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) Q =
    (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) P ≫ (functor ⋙ inverse).map φ
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
i✝ : ι
⊢ HomologicalComplex.Hom.f
      ((𝟭 (Karoubi (HomologicalComplex C c))).map φ ≫
          (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) Q).f
      i✝ =
    HomologicalComplex.Hom.f
      ((fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) P ≫
          (functor ⋙ inverse).map φ).f
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
i✝ : ι
⊢ HomologicalComplex.Hom.f φ.f i✝ ≫ HomologicalComplex.Hom.f Q.p i✝ =
    HomologicalComplex.Hom.f P.p i✝ ≫ HomologicalComplex.Hom.f φ.f i✝
[PROOFSTEP]
simp only [comp_f, HomologicalComplex.comp_f, HomologicalComplex.comp_p_d, Inverse.map_f_f, Functor.map_f_f,
  HomologicalComplex.p_comp_d]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun n => HomologicalComplex.Hom.f P.p n) i ≫
      HomologicalComplex.d ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).X i j =
    HomologicalComplex.d ((functor ⋙ inverse).obj P).X i j ≫ (fun n => HomologicalComplex.Hom.f P.p n) j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.d P.X i j =
    (HomologicalComplex.Hom.f P.p i ≫ HomologicalComplex.d P.X i j) ≫ HomologicalComplex.Hom.f P.p j
[PROOFSTEP]
simp only [HomologicalComplex.Hom.comm, assoc, HomologicalComplex.p_idem]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
⊢ (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) =
    ((functor ⋙ inverse).obj P).p ≫
      (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) ≫
        ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ HomologicalComplex.Hom.f (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) n =
    HomologicalComplex.Hom.f
      (((functor ⋙ inverse).obj P).p ≫
        (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n) ≫
          ((𝟭 (Karoubi (HomologicalComplex C c))).obj P).p)
      n
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P : Karoubi (HomologicalComplex C c)
n : ι
⊢ HomologicalComplex.Hom.f P.p n =
    HomologicalComplex.Hom.f P.p n ≫ HomologicalComplex.Hom.f P.p n ≫ HomologicalComplex.Hom.f P.p n
[PROOFSTEP]
simp only [HomologicalComplex.p_idem]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
⊢ (functor ⋙ inverse).map φ ≫ (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) Q =
    (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) P ≫
      (𝟭 (Karoubi (HomologicalComplex C c))).map φ
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
i✝ : ι
⊢ HomologicalComplex.Hom.f
      ((functor ⋙ inverse).map φ ≫
          (fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) Q).f
      i✝ =
    HomologicalComplex.Hom.f
      ((fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) P ≫
          (𝟭 (Karoubi (HomologicalComplex C c))).map φ).f
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex C c)
φ : P ⟶ Q
i✝ : ι
⊢ HomologicalComplex.Hom.f φ.f i✝ ≫ HomologicalComplex.Hom.f Q.p i✝ =
    HomologicalComplex.Hom.f P.p i✝ ≫ HomologicalComplex.Hom.f φ.f i✝
[PROOFSTEP]
simp only [comp_f, HomologicalComplex.comp_f, Inverse.map_f_f, Functor.map_f_f, HomologicalComplex.comp_p_d,
  HomologicalComplex.p_comp_d]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ ((NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) ≫
      NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) =
    𝟙 (𝟭 (Karoubi (HomologicalComplex C c)))
[PROOFSTEP]
ext
[GOAL]
case w.h.h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
x✝ : Karoubi (HomologicalComplex C c)
i✝ : ι
⊢ HomologicalComplex.Hom.f
      (NatTrans.app
          ((NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) ≫
            NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n))
          x✝).f
      i✝ =
    HomologicalComplex.Hom.f (NatTrans.app (𝟙 (𝟭 (Karoubi (HomologicalComplex C c)))) x✝).f i✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
x✝ : Karoubi (HomologicalComplex C c)
i✝ : ι
⊢ HomologicalComplex.Hom.f x✝.p i✝ ≫ HomologicalComplex.Hom.f x✝.p i✝ = HomologicalComplex.Hom.f x✝.p i✝
[PROOFSTEP]
simp only [HomologicalComplex.p_idem, comp_f, HomologicalComplex.comp_f, _root_.id_eq]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
⊢ ((NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) ≫
      NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) =
    𝟙 (functor ⋙ inverse)
[PROOFSTEP]
ext
[GOAL]
case w.h.h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
x✝ : Karoubi (HomologicalComplex C c)
i✝ : ι
⊢ HomologicalComplex.Hom.f
      (NatTrans.app
          ((NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n)) ≫
            NatTrans.mk fun P => Hom.mk (HomologicalComplex.Hom.mk fun n => HomologicalComplex.Hom.f P.p n))
          x✝).f
      i✝ =
    HomologicalComplex.Hom.f (NatTrans.app (𝟙 (functor ⋙ inverse)) x✝).f i✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h.h
C : Type u_1
inst✝¹ : Category.{?u.35996, u_1} C
inst✝ : Preadditive C
ι : Type u_2
c : ComplexShape ι
x✝ : Karoubi (HomologicalComplex C c)
i✝ : ι
⊢ HomologicalComplex.Hom.f x✝.p i✝ ≫ HomologicalComplex.Hom.f x✝.p i✝ = HomologicalComplex.Hom.f x✝.p i✝
[PROOFSTEP]
simp only [HomologicalComplex.p_idem, comp_f, HomologicalComplex.comp_f, _root_.id_eq, Inverse.obj_p_f, Functor.obj_X_p]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.61291, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
α : Type u_3
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete (HomologicalComplex C c)
[PROOFSTEP]
rw [isIdempotentComplete_iff_of_equivalence ((toKaroubiEquivalence C).mapHomologicalComplex c), ←
  isIdempotentComplete_iff_of_equivalence (karoubiHomologicalComplexEquivalence C c)]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.61291, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
α : Type u_3
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete (Karoubi (HomologicalComplex C c))
[PROOFSTEP]
infer_instance
