awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
rw :
  Eq.{v_1 + 1} (α :=
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
    (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A :
      Quiver.Hom.{v_1, u_1} (V := C) (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ A)
        (Cocone.pt.{0, v_1, 0, u_1} (F := Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))
          (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ)))))
    (𝟙 (K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len) ≫
      Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
⊢ Eq.{v_1 + 1} (α :=
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
    (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A ≫
        𝟙 (colimit.{0, 0, v_1, u_1} (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) :
      K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
    (Sigma.ι (Obj.summand K (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })))
          (Splitting.IndexSet.id (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) ≫
        Obj.map K A.e.op :
      K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)

Tactic:
rw [comp_id, Γ₀.Obj.map_on_summand₀ K (SimplicialObject.Splitting.IndexSet.id A.1)
        (show A.e ≫ 𝟙 _ = A.e.op.unop ≫ 𝟙 _ by rfl), Γ₀.Obj.Termwise.mapMono_id]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, Sigma.fst, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
dsimp :
  Eq.{v_1 + 1} (α :=
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
    (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A :
      Quiver.Hom.{v_1, u_1} (V := C) (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ A)
        (Cocone.pt.{0, v_1, 0, u_1} (F := Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))
          (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ)))))
    (𝟙 (K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len) ≫
      Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
⊢ Eq.{v_1 + 1} (α :=
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
    (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A :
      Quiver.Hom.{v_1, u_1} (V := C) (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ A)
        (Cocone.pt.{0, v_1, 0, u_1} (F := Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))
          (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ)))))
    (𝟙 (K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len) ≫
      Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
rw :
  Eq.{v_1 + 1} (α :=
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
    (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A)
    (Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
⊢ Eq.{v_1 + 1} (α :=
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
    (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A :
      Quiver.Hom.{v_1, u_1} (V := C) (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ A)
        (Cocone.pt.{0, v_1, 0, u_1} (F := Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))
          (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ)))))
    (𝟙 (K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len) ≫
      Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Eq.{v_1 + 1} (α :=
    K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ Obj.obj₂ K Δ)
    (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A)
    (Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
dsimp :
  Eq (α :=
    Splitting.N (X := obj K) (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      obj₂ K Δ')
    ((Splitting.ι (splitting K)
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        map K A.e.op) ≫
      map K θ)
    (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)
⊢ Eq (α := Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ A ⟶ (obj K).obj Δ')
    (Cofan.inj (Splitting.cofan (splitting K) Δ) A ≫ (obj K).map θ)
    (Termwise.mapMono K i ≫ Cofan.inj (Splitting.cofan (splitting K) Δ') (Splitting.IndexSet.mk e))

Tactic:
dsimp [Splitting.cofan]

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
change :
  Eq (α :=
    Splitting.N (X := obj K) (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      (obj K).obj Δ')
    ((Splitting.ι (splitting K)
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        (obj K).map A.e.op) ≫
      (obj K).map θ)
    (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)
⊢ Eq (α :=
    Splitting.N (X := obj K) (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      obj₂ K Δ')
    ((Splitting.ι (splitting K)
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        map K A.e.op) ≫
      map K θ)
    (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)

Tactic:
change (_ ≫ (Γ₀.obj K).map A.e.op) ≫ (Γ₀.obj K).map θ = _

Premises used: AlgebraicTopology.DoldKan.Γ₀.obj, Quiver.Hom.op, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.SimplicialObject.Splitting.IndexSet.e
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
rw :
  Eq (α :=
    Splitting.N (X := obj K) (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      (obj K).obj Δ')
    (Splitting.ι (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      (obj K).map (A.e.op ≫ θ))
    (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)
⊢ Eq (α :=
    Splitting.N (X := obj K) (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      (obj K).obj Δ')
    ((Splitting.ι (splitting K)
          (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        (obj K).map A.e.op) ≫
      (obj K).map θ)
    (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)

Tactic:
rw [assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
dsimp :
  Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Sigma.ι (summand K (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })))
          (Splitting.IndexSet.id (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) ≫
        map K (A.e.op ≫ θ) :
      K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
        Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op :
      K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
⊢ Eq (α :=
    Splitting.N (X := obj K) (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      (obj K).obj Δ')
    (Splitting.ι (splitting K)
        (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      (obj K).map (A.e.op ≫ θ))
    (Termwise.mapMono K i ≫ Splitting.ι (splitting K) Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op)

Tactic:
dsimp [splitting]

Premises used: AlgebraicTopology.DoldKan.Γ₀.splitting
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
rw : θ.unop ≫ A.e = (A.e.op ≫ θ).unop
⊢ e ≫ i =
    (A.e.op ≫ θ).unop ≫
      𝟙 (unop (op (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })))))

Tactic:
rw [comp_id, fac]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ θ.unop ≫ A.e = (A.e.op ≫ θ).unop

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
rw :
  Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op)
⊢ Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Sigma.ι (summand K (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })))
          (Splitting.IndexSet.id (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) ≫
        map K (A.e.op ≫ θ) :
      K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
        Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op :
      K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')

Tactic:
rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id A.1)
    (show e ≫ i = ((Splitting.IndexSet.e A).op ≫ θ).unop ≫ 𝟙 _ by rw [comp_id, fac]; rfl)]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, Sigma.fst
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
dsimp :
  Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K Δ')
        (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
          (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e ⋯)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K e.op)
⊢ Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op)

Tactic:
dsimp only [Splitting.IndexSet.id_fst, Splitting.IndexSet.mk, op_unop, Splitting.IndexSet.e]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id_fst, CategoryTheory.SimplicialObject.Splitting.IndexSet.mk, Opposite.op_unop, CategoryTheory.SimplicialObject.Splitting.IndexSet.e
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ e ≫ 𝟙 Δ'' = e.op.unop ≫ 𝟙 (unop (op Δ''))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
rw :
  Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K Δ')
        (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
          (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e ⋯)))
    (Termwise.mapMono K i ≫ 𝟙 (K.X Δ''.len) ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
⊢ Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K Δ')
        (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
          (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e ⋯)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K e.op)

Tactic:
rw [Γ₀.Obj.map_on_summand₀ K (Splitting.IndexSet.id (op Δ''))
      (show e ≫ 𝟙 Δ'' = e.op.unop ≫ 𝟙 _ by simp), Termwise.mapMono_id]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, Opposite.op, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
dsimp :
  Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K Δ')
        (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
          (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e ⋯)))
    (Termwise.mapMono K i ≫ 𝟙 (K.X Δ''.len) ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
⊢ Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K Δ')
        (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
          (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e ⋯)))
    (Termwise.mapMono K i ≫ 𝟙 (K.X Δ''.len) ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))

Tactic:
dsimp only [Splitting.IndexSet.id_fst]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id_fst
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
rw :
  Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K Δ')
        (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
          (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e ⋯)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
⊢ Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K Δ')
        (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
          (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e ⋯)))
    (Termwise.mapMono K i ≫ 𝟙 (K.X Δ''.len) ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K Δ')
        (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
          (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e ⋯)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
fac :
  CategoryStruct.comp (Y := image (θ.unop ≫ A.e)) (factorThruImage (θ.unop ≫ A.e)) (image.ι (θ.unop ≫ A.e)) =
    θ.unop ≫ A.e
⊢ Eq (α := Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ A ⟶ (obj K).obj Δ')
    (Cofan.inj (Splitting.cofan (splitting K) Δ) A ≫ (obj K).map θ)
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (Cofan.inj (Splitting.cofan (splitting K) Δ') (A.pull θ)))

Tactic:
apply Obj.map_on_summand

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ CategoryStruct.comp (Y := image (θ.unop ≫ A.e)) (factorThruImage (θ.unop ≫ A.e)) (image.ι (θ.unop ≫ A.e)) =
    θ.unop ≫ A.e

Tactic:
apply image.fac

Premises used: CategoryTheory.Limits.image.fac