awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
h :
  HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e))) ≫ X.map (A.pull θ).e.op =
    HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ X.map θ
⊢ HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e))) ≫ X.map (A.pull θ).e.op =
    HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)).map θ

Tactic:
dsimp only [toKaroubi]

Premises used: CategoryTheory.Idempotents.toKaroubi
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
h :
  Eq (α := Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶ X.obj Δ')
    (HomologicalComplex.Hom.f PInfty
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e)) ≫ (A.pull θ).e.op) :
      HomologicalComplex.X K[X]
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
        X.obj Δ')
    (HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (A.e.op ≫ θ))
⊢ HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e))) ≫ X.map (A.pull θ).e.op =
    HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map A.e.op ≫ X.map θ

Tactic:
simp only [← X.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
h : Quiver.Hom.op (image.ι (θ.unop ≫ A.e)) ≫ (A.pull θ).e.op = A.e.op ≫ θ
⊢ Eq (α := Splitting.summand (Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X])) Δ A ⟶ X.obj Δ')
    (HomologicalComplex.Hom.f PInfty
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        X.map (Quiver.Hom.op (image.ι (θ.unop ≫ A.e)) ≫ (A.pull θ).e.op) :
      HomologicalComplex.X K[X]
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
        X.obj Δ')
    (HomologicalComplex.Hom.f PInfty
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      X.map (A.e.op ≫ θ))

Tactic:
congr 2
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
h : ((A.pull θ).e ≫ image.ι (θ.unop ≫ A.e)).op = A.e.op ≫ θ
⊢ Quiver.Hom.op (image.ι (θ.unop ≫ A.e)) ≫ (A.pull θ).e.op = A.e.op ≫ θ

Tactic:
simp only [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ ((A.pull θ).e ≫ image.ι (θ.unop ≫ A.e)).op = A.e.op ≫ θ

Tactic:
Quiver.Hom.unop_inj (A.fac_pull θ)

Premises used: Quiver.Hom.unop_inj, CategoryTheory.SimplicialObject.Splitting.IndexSet.fac_pull
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
θ : Δ ⟶ Δ'
A : Splitting.IndexSet Δ
⊢ ((A.pull θ).e ≫ image.ι (θ.unop ≫ A.e)).op = A.e.op ≫ θ

Tactic:
exact Quiver.Hom.unop_inj (A.fac_pull θ)

Premises used: Quiver.Hom.unop_inj, CategoryTheory.SimplicialObject.Splitting.IndexSet.fac_pull
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
h :
  ∀ (n : ℕ),
    Eq (α :=
      Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X]) n ⟶
        Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) _⦋n⦌)
      (Splitting.φ (Γ₀.splitting K[X])
        ((Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).p ≫
          {
              app := fun (Δ : SimplexCategoryᵒᵖ) ↦
                Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
                  HomologicalComplex.Hom.f PInfty
                      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
                    X.map A.e.op,
              naturality := ⋯ } ≫
            Karoubi.p (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        n)
      (Splitting.φ (Γ₀.splitting K[X])
        {
          app := fun (Δ : SimplexCategoryᵒᵖ) ↦
            Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
              HomologicalComplex.Hom.f PInfty
                  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
                X.map A.e.op,
          naturality := ⋯ }
        n)
⊢ Eq (α :=
    (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).X ⟶
      Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
    ((Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).p ≫
      {
          app := fun (Δ : SimplexCategoryᵒᵖ) ↦
            Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
              HomologicalComplex.Hom.f PInfty
                  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
                X.map A.e.op,
          naturality := ⋯ } ≫
        Karoubi.p (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
    {
      app := fun (Δ : SimplexCategoryᵒᵖ) ↦
        Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
            X.map A.e.op,
      naturality := ⋯ }

Tactic:
apply (Γ₀.splitting K[X]).hom_ext

Premises used: AlgebraicTopology.DoldKan.Γ₀.splitting, AlgebraicTopology.AlternatingFaceMapComplex.obj, CategoryTheory.SimplicialObject.Splitting.hom_ext
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
h :
  Eq (α := Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X]) n ⟶ X _⦋n⦌)
    (Splitting.ι (Γ₀.splitting K[X]) n ≫
      CategoryStruct.comp (Y := Γ₀.Obj.obj₂ K[X] (op ⦋n⦌))
        (Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
            CategoryStruct.comp (Y :=
              X.obj (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })))
              (HomologicalComplex.Hom.f PInfty
                  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len :
                HomologicalComplex.X K[X]
                    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ⟶
                  HomologicalComplex.X K[X]
                    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len)
              (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) (op ⦋n⦌)) A) :
          Γ₀.obj K[X] _⦋n⦌ ⟶ Γ₀.Obj.obj₂ K[X] (op ⦋n⦌))
        ((Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
              HomologicalComplex.Hom.f PInfty
                  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
                X.map A.e.op) ≫
            𝟙 (X _⦋n⦌) :
          Γ₀.Obj.obj₂ K[X] (op ⦋n⦌) ⟶ X _⦋n⦌))
    (Splitting.ι (Γ₀.splitting K[X]) n ≫
      Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
        HomologicalComplex.Hom.f PInfty
            (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
          X.map A.e.op)
⊢ Eq (α :=
    Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X]) n ⟶
      Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) _⦋n⦌)
    (Splitting.φ (Γ₀.splitting K[X])
      ((Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X).p ≫
        {
            app := fun (Δ : SimplexCategoryᵒᵖ) ↦
              Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
                HomologicalComplex.Hom.f PInfty
                    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
                  X.map A.e.op,
            naturality := ⋯ } ≫
          Karoubi.p (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
      n)
    (Splitting.φ (Γ₀.splitting K[X])
      {
        app := fun (Δ : SimplexCategoryᵒᵖ) ↦
          Splitting.desc (Γ₀.splitting K[X]) Δ fun (A : Splitting.IndexSet Δ) ↦
            HomologicalComplex.Hom.f PInfty
                (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
              X.map A.e.op,
        naturality := ⋯ }
      n)

Tactic:
dsimp [N₁]

Premises used: AlgebraicTopology.DoldKan.N₁
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq (α := Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X]) n ⟶ X _⦋n⦌)
    (Splitting.ι (Γ₀.splitting K[X]) n ≫
      CategoryStruct.comp (Y := Γ₀.Obj.obj₂ K[X] (op ⦋n⦌))
        (Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
            CategoryStruct.comp (Y :=
              X.obj (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })))
              (HomologicalComplex.Hom.f PInfty
                  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len :
                HomologicalComplex.X K[X]
                    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ⟶
                  HomologicalComplex.X K[X]
                    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len)
              (Cofan.inj (Splitting.cofan (Γ₀.splitting K[X]) (op ⦋n⦌)) A) :
          Γ₀.obj K[X] _⦋n⦌ ⟶ Γ₀.Obj.obj₂ K[X] (op ⦋n⦌))
        ((Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
              HomologicalComplex.Hom.f PInfty
                  (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
                X.map A.e.op) ≫
            𝟙 (X _⦋n⦌) :
          Γ₀.Obj.obj₂ K[X] (op ⦋n⦌) ⟶ X _⦋n⦌))
    (Splitting.ι (Γ₀.splitting K[X]) n ≫
      Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
        HomologicalComplex.Hom.f PInfty
            (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
          X.map A.e.op)

Tactic:
simp only [← Splitting.cofan_inj_id, Splitting.ι_desc, comp_id, Splitting.ι_desc_assoc,
          assoc, PInfty_f_idem_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.SimplicialObject.Splitting.cofan_inj_id, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, CategoryTheory.SimplicialObject.Splitting.ι_desc, CategoryTheory.SimplicialObject.Splitting.ι_desc_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
n : ℕ
⊢ Eq (α := Splitting.N (X := Γ₀.obj K[X]) (Γ₀.splitting K[X]) n ⟶ Y _⦋n⦌)
    (Splitting.ι (Γ₀.splitting K[X]) n ≫
      CategoryStruct.comp (Y := Γ₀.Obj.obj₂ K[Y] (op ⦋n⦌))
        (Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
            CategoryStruct.comp (Y :=
                X.obj (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })))
                (HomologicalComplex.Hom.f PInfty
                    (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len :
                  HomologicalComplex.X K[X]
                      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ⟶
                    HomologicalComplex.X K[X]
                      (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len)
                (f.app (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))) ≫
              Cofan.inj (Splitting.cofan (Γ₀.splitting K[Y]) (op ⦋n⦌)) A :
          Γ₀.obj K[X] _⦋n⦌ ⟶ Γ₀.Obj.obj₂ K[Y] (op ⦋n⦌))
        (Splitting.desc (Γ₀.splitting K[Y]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
            HomologicalComplex.Hom.f PInfty
                (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
              Y.map A.e.op :
          Γ₀.obj K[Y] _⦋n⦌ ⟶ Y _⦋n⦌))
    (Splitting.ι (Γ₀.splitting K[X]) n ≫
      (Splitting.desc (Γ₀.splitting K[X]) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
          HomologicalComplex.Hom.f PInfty
              (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
            X.map A.e.op) ≫
        f.app (op ⦋n⦌))

Tactic:
simp only [← Splitting.cofan_inj_id, Splitting.ι_desc, Splitting.ι_desc_assoc, assoc,
      PInfty_f_idem_assoc, PInfty_f_naturality_assoc,
      NatTrans.naturality, Splitting.IndexSet.id_fst, unop_op, len_mk]

Premises used: CategoryTheory.Category.assoc, SimplexCategory.len_mk, CategoryTheory.SimplicialObject.Splitting.cofan_inj_id, CategoryTheory.SimplicialObject.Splitting.IndexSet.id_fst, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, CategoryTheory.NatTrans.naturality, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, CategoryTheory.SimplicialObject.Splitting.ι_desc, Opposite.unop_op, CategoryTheory.SimplicialObject.Splitting.ι_desc_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P ⟶
      Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)
    (NatTrans.app
      (Functor.preimage
        (Functor.obj
          (Functor.whiskeringLeft (SimplicialObject.{v_1, u_1} C) (Karoubi (SimplicialObject.{v_1, u_1} C))
            (Karoubi (SimplicialObject.{v_1, u_1} C)))
          (toKaroubi (SimplicialObject.{v_1, u_1} C)))
        (Iso.hom Γ₂N₂ToKaroubiIso ≫ Γ₂N₁.natTrans))
      P)
    (CategoryTheory.Functor.map (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P.decompId_i ≫
      NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso ≫ Γ₂N₁.natTrans) P.X ≫ P.decompId_p)

Tactic:
simp only [whiskeringLeft_obj_preimage_app, Functor.id_map]

Premises used: CategoryTheory.Functor.id_map, CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
rw :
  Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)
    (NatTrans.app Γ₂N₁.natTrans X)
    (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
      CategoryTheory.Functor.map (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂)
          (Karoubi.decompId_i (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
        NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso ≫ Γ₂N₁.natTrans)
            (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
          Karoubi.decompId_p (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)
    (NatTrans.app Γ₂N₁.natTrans X)
    (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
      NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))

Tactic:
rw [Γ₂N₂.natTrans_app_f_app]

Premises used: AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
dsimp :
  Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)
    (NatTrans.app Γ₂N₁.natTrans X)
    (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
      CategoryStruct.comp (Y :=
        Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂)
          { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
            p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := ⋯ :
            Karoubi (SimplicialObject.{v_1, u_1} C) })
        (CategoryTheory.Functor.map Γ₂
          (CategoryTheory.Functor.map N₂ (𝟙 (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))))
        ((NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso)
              (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
            NatTrans.app Γ₂N₁.natTrans (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
          𝟙
            { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
              p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := ⋯ }))
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)
    (NatTrans.app Γ₂N₁.natTrans X)
    (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
      CategoryTheory.Functor.map (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂)
          (Karoubi.decompId_i (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
        NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso ≫ Γ₂N₁.natTrans)
            (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
          Karoubi.decompId_p (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))

Tactic:
dsimp only [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi, Functor.comp_map,
    NatTrans.comp_app]

Premises used: CategoryTheory.Idempotents.Karoubi.decompId_i_toKaroubi, CategoryTheory.NatTrans.comp_app, CategoryTheory.Idempotents.Karoubi.decompId_p_toKaroubi, CategoryTheory.Functor.comp_map
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
rw :
  NatTrans.app Γ₂N₁.natTrans X =
    NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      𝟙
          (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
            (Functor.obj N₂ (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
        (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso)
              (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
            NatTrans.app Γ₂N₁.natTrans (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
          𝟙
            { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
              p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := ⋯ :
              Karoubi (SimplicialObject.{v_1, u_1} C) }
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)
    (NatTrans.app Γ₂N₁.natTrans X)
    (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
      CategoryStruct.comp (Y :=
        Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂)
          { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
            p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := ⋯ :
            Karoubi (SimplicialObject.{v_1, u_1} C) })
        (CategoryTheory.Functor.map Γ₂
          (CategoryTheory.Functor.map N₂ (𝟙 (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))))
        ((NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso)
              (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
            NatTrans.app Γ₂N₁.natTrans (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
          𝟙
            { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
              p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := ⋯ }))

Tactic:
rw [N₂.map_id, Γ₂.map_id, Iso.app_inv]

Premises used: CategoryTheory.Iso.app_inv, AlgebraicTopology.DoldKan.Γ₂, AlgebraicTopology.DoldKan.N₂, CategoryTheory.Functor.map_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
dsimp :
  NatTrans.app Γ₂N₁.natTrans X =
    NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      𝟙
          (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
            (Functor.obj N₂ { X := X, p := 𝟙 X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) })) ≫
        (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso) X ≫ NatTrans.app Γ₂N₁.natTrans X) ≫
          𝟙 { X := X, p := 𝟙 X, idem := ⋯ : Karoubi (SimplicialObject.{v_1, u_1} C) }
⊢ NatTrans.app Γ₂N₁.natTrans X =
    NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      𝟙
          (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
            (Functor.obj N₂ (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
        (NatTrans.app (Iso.hom Γ₂N₂ToKaroubiIso)
              (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
            NatTrans.app Γ₂N₁.natTrans (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))) ≫
          𝟙
            { X := Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X),
              p := 𝟙 (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)), idem := ⋯ :
              Karoubi (SimplicialObject.{v_1, u_1} C) }

Tactic:
dsimp only [toKaroubi]

Premises used: CategoryTheory.Idempotents.toKaroubi