awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h :
  Functor.obj
      (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⋙
        karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
      Y₂ =
    Functor.obj (Functor.obj (Functor.whiskeringRight SimplexCategoryᵒᵖ C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y₂
simp :
  Eq (α := HomologicalComplex.X K[Y₄] n ⟶ HomologicalComplex.X K[Y₄] n)
    (NatTrans.app (natTransPInfty_f (Karoubi.{v_1, u_1} C) n) Y₄ :
      Functor.obj
          (Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
            (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
          Y₄ ⟶
        Functor.obj
          (Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
            (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
          Y₄)
    (NatTrans.app (natTransPInfty_f (Karoubi.{v_1, u_1} C) n) Y₃)
⊢ P₄.f n = P₃.f n

Tactic:
simp only [P₃, P₄, ← natTransPInfty_f_app]

Premises used: AlgebraicTopology.DoldKan.natTransPInfty_f_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h :
  Functor.obj
      (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⋙
        karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
      Y₂ =
    Functor.obj (Functor.obj (Functor.whiskeringRight SimplexCategoryᵒᵖ C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y₂
⊢ Eq (α := HomologicalComplex.X K[Y₄] n ⟶ HomologicalComplex.X K[Y₄] n)
    (NatTrans.app (natTransPInfty_f (Karoubi.{v_1, u_1} C) n) Y₄ :
      Functor.obj
          (Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
            (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
          Y₄ ⟶
        Functor.obj
          (Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
            (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
          Y₄)
    (NatTrans.app (natTransPInfty_f (Karoubi.{v_1, u_1} C) n) Y₃)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
⊢ P₄.f n = P₃.f n

Tactic:
have h₄₃ : P₄.f n = P₃.f n := by
    have h := Functor.congr_obj (toKaroubi_comp_karoubiFunctorCategoryEmbedding _ _) Y₂
    simp only [P₃, P₄, ← natTransPInfty_f_app]
    congr 1
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
⊢ Eq (α :=
    Functor.obj
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
            (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
        Y ⟶
      Functor.obj
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
            (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
        Y)
    (NatTrans.app (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi.{v_1, u_1} C) n)
      Y)
    (CategoryTheory.Functor.map
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
            (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
        Y.decompId_i ≫
      NatTrans.app (𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) ◫ natTransPInfty_f (Karoubi.{v_1, u_1} C) n)
          { X := Y.X, p := 𝟙 Y.X, idem := ⋯ : Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } ≫
        CategoryTheory.Functor.map
          (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            Functor.comp (D := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C))
              (HomologicalComplex.eval (Karoubi.{v_1, u_1} C) (ComplexShape.down ℕ) n))
          Y.decompId_p)

Tactic:
have h₁₄ := Idempotents.natTrans_eq
    ((𝟙 (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)) ◫
      (natTransPInfty_f (Karoubi C) n)) Y
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  (𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n) ≫
      𝟙 (KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌) =
    (KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      ((𝟙
              (KaroubiFunctorCategoryEmbedding.obj
                  { X := Y.X, p := 𝟙 Y.X, idem := ⋯ :
                    Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } _⦋n⦌) ≫
            HomologicalComplex.Hom.f PInfty n) ≫
          𝟙
            (KaroubiFunctorCategoryEmbedding.obj
                { X := Y.X, p := 𝟙 Y.X, idem := ⋯ :
                  Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } _⦋n⦌)) ≫
        (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)
⊢ Eq.{v_1 + 1} (α := KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌ ⟶ KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n ⟶
        HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n)
    ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌))

Tactic:
rw [id_comp, id_comp, comp_id, comp_id] at h₁₄

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  Eq.{v_1 + 1} (α := KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌ ⟶ KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n ⟶
        HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n)
    ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌))
rw :
  Karoubi.Hom.f
      ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
        HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)) =
    Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
⊢ (P₁.f n).f = Y.p.app (op ⦋n⦌) ≫ P₂.f n

Tactic:
rw [← h₃₂, ← h₄₃, h₁₄]
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  Eq.{v_1 + 1} (α := KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌ ⟶ KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n ⟶
        HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n)
    ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌))
simp :
  Y.p.app (op ⦋n⦌) ≫
      CategoryStruct.comp (Y :=
        KaroubiFunctorCategoryEmbedding.obj
              { X := Y.X, p := 𝟙 Y.X, idem := ⋯ :
                Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } _⦋n⦌.X)
        (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n)) (Y.p.app (op ⦋n⦌)) =
    Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
⊢ Karoubi.Hom.f
      ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
        HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌)) =
    Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f

Tactic:
simp only [KaroubiFunctorCategoryEmbedding.map_app_f, Karoubi.decompId_p_f,
    Karoubi.decompId_i_f, Karoubi.comp_f]

Premises used: CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.Karoubi.decompId_i_f, CategoryTheory.Idempotents.Karoubi.decompId_p_f, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map_app_f
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  Eq.{v_1 + 1} (α := KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌ ⟶ KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n ⟶
        HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n)
    ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌))
π : Y₄ ⟶ Y₄ :=
  CategoryTheory.Functor.map
    (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⋙
      karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    Y.p
⊢ Eq (α := Y₄ _⦋n⦌.X ⟶ (HomologicalComplex.X K[Y₄] n).X)
    (Karoubi.Hom.f (π.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n))
    (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n ≫ π.app (op ⦋n⦌)))

Tactic:
have eq := Karoubi.hom_ext_iff.mp (PInfty_f_naturality n π)
-- Module: Mathlib.AlgebraicTopology.DoldKan.PInfty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
Y : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
Y₁ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C := Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C) Y
Y₂ : SimplicialObject.{v_1, u_1} C := Y.X
Y₃ : SimplicialObject (Karoubi.{v_1, u_1} C) :=
  Functor.obj (Functor.obj (whiskering C (Karoubi.{v_1, u_1} C)) (toKaroubi C)) Y.X
Y₄ : SimplexCategoryᵒᵖ ⥤ Karoubi.{v_1, u_1} C :=
  Functor.obj (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    (Functor.obj (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C)) Y.X)
P₁ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₁] K[Y₁] := PInfty
P₂ : Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[Y₂] K[Y₂] := PInfty
P₃ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₃] K[Y₃] := PInfty
P₄ : Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ) K[Y₄] K[Y₄] := PInfty
h₃₂ : (P₃.f n).f = P₂.f n
h₄₃ : P₄.f n = P₃.f n
h₁₄ :
  Eq.{v_1 + 1} (α := KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌ ⟶ KaroubiFunctorCategoryEmbedding.obj Y _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n :
      HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n ⟶
        HomologicalComplex.X
          (Functor.obj (alternatingFaceMapComplex (Karoubi.{v_1, u_1} C)) (KaroubiFunctorCategoryEmbedding.obj Y)) n)
    ((KaroubiFunctorCategoryEmbedding.map Y.decompId_i).app (op ⦋n⦌) ≫
      HomologicalComplex.Hom.f PInfty n ≫ (KaroubiFunctorCategoryEmbedding.map Y.decompId_p).app (op ⦋n⦌))
π : Y₄ ⟶ Y₄ :=
  CategoryTheory.Functor.map
    (toKaroubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) ⋙
      karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C)
    Y.p
eq :
  Eq (α := Y₄ _⦋n⦌.X ⟶ Y₄ _⦋n⦌.X) (Y.p.app (op ⦋n⦌) ≫ Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n))
    (CategoryStruct.comp (Y := Y₄ _⦋n⦌.X) (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n)) (Y.p.app (op ⦋n⦌)))
rw :
  Y.p.app (op ⦋n⦌) ≫ Y.p.app (op ⦋n⦌) ≫ Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n) =
    Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
rw₁ rw₂ : Y.p.app (op ⦋n⦌) ≫ Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n) = Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f
⊢ Y.p.app (op ⦋n⦌) ≫
      CategoryStruct.comp (Y :=
        KaroubiFunctorCategoryEmbedding.obj
              { X := Y.X, p := 𝟙 Y.X, idem := ⋯ :
                Karoubi (CategoryTheory.Functor.{0, v_1, 0, u_1} SimplexCategoryᵒᵖ C) } _⦋n⦌.X)
        (Karoubi.Hom.f (HomologicalComplex.Hom.f PInfty n)) (Y.p.app (op ⦋n⦌)) =
    Y.p.app (op ⦋n⦌) ≫ (P₄.f n).f

Tactic:
rw [← eq, app_idem_assoc Y (op ⦋n⦌)]

Premises used: CategoryTheory.Idempotents.app_idem_assoc, SimplexCategory.mk, Opposite.op
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (P 0) (𝟙 K[X])

Tactic:
rfl

Premises used: rfl, AlgebraicTopology.DoldKan.P
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
⊢ P (q + 1) = P q ≫ HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) (Hσ q)

Tactic:
rfl

Premises used: rfl, AlgebraicTopology.DoldKan.P
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ HomologicalComplex.Hom.f (P 0) 0 = 𝟙 (HomologicalComplex.X K[X] 0)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
hq : HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
⊢ HomologicalComplex.Hom.f (P (q + 1)) 0 = 𝟙 (HomologicalComplex.X K[X] 0)

Tactic:
simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
      HomologicalComplex.id_f, id_comp, hq, Hσ_eq_zero, add_zero]

Premises used: HomologicalComplex.add_f_apply, HomologicalComplex.id_f, AlgebraicTopology.DoldKan.P_succ, HomologicalComplex.comp_f, AlgebraicTopology.DoldKan.Hσ_eq_zero, add_zero, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
zero : HomologicalComplex.Hom.f (P 0) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
succ :
  ∀ (q : ℕ) (hq : HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)),
    HomologicalComplex.Hom.f (P (q + 1)) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
⊢ HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)

Tactic:
induction q with
  | zero => rfl
  | succ q hq =>
    simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
      HomologicalComplex.id_f, id_comp, hq, Hσ_eq_zero, add_zero]

Premises used: HomologicalComplex.add_f_apply, HomologicalComplex.id_f, AlgebraicTopology.DoldKan.P_succ, HomologicalComplex.comp_f, AlgebraicTopology.DoldKan.Hσ_eq_zero, add_zero, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
rw : P q + HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) (P q) = 𝟙 K[X]
⊢ HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (P q) (Q q) = 𝟙 K[X]

Tactic:
rw [Q]

Premises used: AlgebraicTopology.DoldKan.Q
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q : ℕ
⊢ P q + HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) (P q) = 𝟙 K[X]

Tactic:
abel
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
⊢ HAdd.hAdd (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f (P q) n)
      (HomologicalComplex.Hom.f (Q q) n) =
    𝟙 (X _⦋n⦌)

Tactic:
HomologicalComplex.congr_hom (P_add_Q q) n

Premises used: AlgebraicTopology.DoldKan.P_add_Q, HomologicalComplex.congr_hom