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 : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : ¬Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0

Tactic:
simp only [mapMono_eq_zero K i' h₂ h₄, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero
-- 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 ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : ¬Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0

Tactic:
simp only [mapMono_eq_zero K i h₁ h₃, zero_comp]

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero, CategoryTheory.Limits.zero_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
simp :
  Eq (α := summand K Δ A ⟶ obj₂ K Δ')
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (Sigma.ι (summand K Δ') (A.pull θ)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
⊢ Eq (α := summand K Δ A ⟶ obj₂ K Δ') (Sigma.ι (summand K Δ) A ≫ map K θ)
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))

Tactic:
simp only [map, colimit.ι_desc, Cofan.mk_ι_app]

Premises used: CategoryTheory.Limits.Cofan.mk_ι_app, AlgebraicTopology.DoldKan.Γ₀.Obj.map, CategoryTheory.Limits.colimit.ι_desc
-- 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
obtain :
  ∀ {e : unop Δ' ⟶ image (θ.unop ≫ A.e)}
    {i : image (θ.unop ≫ A.e) ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))}
    [inst_5 : Epi e] [inst_6 : Mono i] (fac : e ≫ i = θ.unop ≫ A.e),
    Eq (α := summand K Δ A ⟶ obj₂ K Δ')
      (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
        (Sigma.ι (summand K Δ') (A.pull θ)))
      (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
⊢ Eq (α := summand K Δ A ⟶ obj₂ K Δ')
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (Sigma.ι (summand K Δ') (A.pull θ)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))

Tactic:
obtain rfl := SimplexCategory.image_eq fac

Premises used: SimplexCategory.image_eq, 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 Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
e_a : image.ι (θ.unop ≫ A.e) = i
e_a₁ : A.pull θ = Splitting.IndexSet.mk e
⊢ Eq (α := summand K Δ A ⟶ obj₂ K Δ')
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (Sigma.ι (summand K Δ') (A.pull θ)))
    (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))

Tactic:
congr
-- 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 Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ image.ι (θ.unop ≫ A.e) = i

Tactic:
SimplexCategory.image_ι_eq fac

Premises used: SimplexCategory.image_ι_eq
-- 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 Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ image.ι (θ.unop ≫ A.e) = i

Tactic:
exact SimplexCategory.image_ι_eq fac

Premises used: SimplexCategory.image_ι_eq
-- 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 Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
e_a : factorThruImage (θ.unop ≫ A.e) = e
⊢ Splitting.IndexSet.mk (Δ' := image (θ.unop ≫ A.e)) (factorThruImage (θ.unop ≫ A.e)) = Splitting.IndexSet.mk e

Tactic:
congr
-- 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 Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ factorThruImage (θ.unop ≫ A.e) = e

Tactic:
SimplexCategory.factorThruImage_eq fac

Premises used: SimplexCategory.factorThruImage_eq
-- 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 Δ
θ : Δ ⟶ Δ'
e : unop Δ' ⟶ image (θ.unop ≫ A.e)
i : image (θ.unop ≫ A.e) ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ factorThruImage (θ.unop ≫ A.e) = e

Tactic:
exact SimplexCategory.factorThruImage_eq fac

Premises used: SimplexCategory.factorThruImage_eq
-- 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 Δ
θ : Δ ⟶ Δ'
⊢ Eq (α := summand K Δ A ⟶ obj₂ K Δ') (Sigma.ι (summand K Δ) A ≫ map K θ)
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (Sigma.ι (summand K Δ') (A.pull θ)))

Tactic:
map_on_summand₀ K A (A.fac_pull θ)

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, CategoryTheory.SimplicialObject.Splitting.IndexSet.fac_pull, CategoryTheory.SimplicialObject.Splitting.IndexSet.pull
-- 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ᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
dsimp :
  colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) =
    colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
        { as := A : Discrete (Splitting.IndexSet Δ) } ≫
      𝟙 (Obj.obj₂ K Δ)
⊢ colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) =
    colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
        { as := A : Discrete (Splitting.IndexSet Δ) } ≫
      𝟙 (Obj.obj₂ K Δ)

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ᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
rw : A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) = 𝟙 (unop Δ) ≫ A.e
rw₁ : A.e = 𝟙 (unop Δ) ≫ A.e
rw₂ rw₃ : A.e = A.e
⊢ A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e

Tactic:
rw [unop_id, comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.unop_id, 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ᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e

Tactic:
have fac : A.e ≫ 𝟙 A.1.unop = (𝟙 Δ).unop ≫ A.e := by rw [unop_id, comp_id, 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ᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac :
  A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e
rw :
  Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) =
    colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
        { as := A : Discrete (Splitting.IndexSet Δ) } ≫
      𝟙 (Obj.obj₂ K Δ)
⊢ colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A } ≫ Obj.map K (𝟙 Δ) =
    colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
        { as := A : Discrete (Splitting.IndexSet Δ) } ≫
      𝟙 (Obj.obj₂ K Δ)

Tactic:
rw [Obj.map_on_summand₀ K A fac, Obj.Termwise.mapMono_id, id_comp]

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, 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ᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac :
  A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e
dsimp :
  Eq.{v_1 + 1} (α := Obj.summand K Δ A ⟶ sigmaObj.{0, v_1, u_1} fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
    (Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A } ≫
      𝟙 (sigmaObj.{0, v_1, u_1} fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A))
⊢ Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e) =
    colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
        { as := A : Discrete (Splitting.IndexSet Δ) } ≫
      𝟙 (Obj.obj₂ K Δ)

Tactic:
dsimp only [Obj.obj₂]

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂
-- 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ᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac :
  A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e
rw :
  Eq.{v_1 + 1} (α := Obj.summand K Δ A ⟶ sigmaObj.{0, v_1, u_1} fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
    (Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A })
⊢ Eq.{v_1 + 1} (α := Obj.summand K Δ A ⟶ sigmaObj.{0, v_1, u_1} fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
    (Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A } ≫
      𝟙 (sigmaObj.{0, v_1, u_1} fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A))

Tactic:
rw [comp_id]

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_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ᵒᵖ
x : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
fac :
  A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    Quiver.Hom.unop (𝟙 Δ) ≫ A.e
⊢ Eq.{v_1 + 1} (α := Obj.summand K Δ A ⟶ sigmaObj.{0, v_1, u_1} fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A)
    (Sigma.ι (Obj.summand K Δ) (Splitting.IndexSet.mk A.e))
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ) ↦ Obj.summand K Δ A) { as := A })

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_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ''_1 : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
rw : θ.unop ≫ θ'.unop ≫ A.e = (θ.unop ≫ θ'.unop) ≫ A.e
rw₁ rw₂ : θ.unop ≫ θ'.unop ≫ A.e = θ.unop ≫ θ'.unop ≫ A.e
⊢ θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e

Tactic:
rw [unop_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.unop_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 Δ'_1 Δ''_1 : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
⊢ θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e

Tactic:
have fac : θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e := by rw [unop_comp, assoc]
-- 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 Δ'_1 Δ''_1 : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac : θ.unop ≫ θ'.unop ≫ A.e = (θ' ≫ θ).unop ≫ A.e
⊢ CategoryStruct.comp (Y := image (Y := image (θ'.unop ≫ A.e)) (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
      (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
      (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e)) =
    (θ' ≫ θ).unop ≫ A.e

Tactic:
rw [← image.fac (θ'.unop ≫ A.e), ← assoc, ←
      image.fac (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)), assoc] at fac

Premises used: CategoryTheory.Limits.factorThruImage, CategoryTheory.Category.assoc, Quiver.Hom.unop, CategoryTheory.Limits.image.fac, 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_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ''_1 : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac :
  CategoryStruct.comp (Y := image (Y := image (θ'.unop ≫ A.e)) (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
      (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
      (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e)) =
    (θ' ≫ θ).unop ≫ A.e
simp :
  Eq (α :=
    Functor.obj.{0, v_1, 0, u_1} (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A)
        { as := A : Discrete (Splitting.IndexSet Δ'') } ⟶
      Obj.obj₂ K Δ)
    (CategoryStruct.comp (Y := K.X (image (Y := image (θ'.unop ≫ A.e)) (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e))).len)
      (Obj.Termwise.mapMono K (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e)))
      (Sigma.ι (Obj.summand K Δ)
        (Splitting.IndexSet.mk (Δ' := image (Y := image (θ'.unop ≫ A.e)) (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
          (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e))))))
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ (A.pull θ').e)).len)
      (Obj.Termwise.mapMono K (image.ι (θ.unop ≫ (A.pull θ').e) ≫ image.ι (θ'.unop ≫ A.e)))
      (Sigma.ι (Obj.summand K Δ) ((A.pull θ').pull θ)))
⊢ Eq (α :=
    Functor.obj.{0, v_1, 0, u_1} (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A)
        { as := A : Discrete (Splitting.IndexSet Δ'') } ⟶
      Obj.obj₂ K Δ)
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A) { as := A } ≫
      Obj.map K (θ' ≫ θ))
    (colimit.ι (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A) { as := A } ≫
      Obj.map K θ' ≫ Obj.map K θ)

Tactic:
simp only [Obj.map_on_summand₀'_assoc K A θ', Obj.map_on_summand₀' K _ θ,
      Obj.Termwise.mapMono_comp_assoc, Obj.map_on_summand₀ K A fac]

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc
-- 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 Δ'_1 Δ''_1 : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ'' Δ' Δ : SimplexCategoryᵒᵖ
θ' : Δ'' ⟶ Δ'
θ : Δ' ⟶ Δ
x : Discrete (Splitting.IndexSet Δ'')
A : Splitting.IndexSet Δ''
fac :
  CategoryStruct.comp (Y := image (Y := image (θ'.unop ≫ A.e)) (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
      (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
      (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e)) =
    (θ' ≫ θ).unop ≫ A.e
⊢ Eq (α :=
    Functor.obj.{0, v_1, 0, u_1} (Discrete.functor fun (A : Splitting.IndexSet Δ'') ↦ Obj.summand K Δ'' A)
        { as := A : Discrete (Splitting.IndexSet Δ'') } ⟶
      Obj.obj₂ K Δ)
    (CategoryStruct.comp (Y := K.X (image (Y := image (θ'.unop ≫ A.e)) (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e))).len)
      (Obj.Termwise.mapMono K (image.ι (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)) ≫ image.ι (θ'.unop ≫ A.e)))
      (Sigma.ι (Obj.summand K Δ)
        (Splitting.IndexSet.mk (Δ' := image (Y := image (θ'.unop ≫ A.e)) (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e)))
          (factorThruImage (θ.unop ≫ factorThruImage (θ'.unop ≫ A.e))))))
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ (A.pull θ').e)).len)
      (Obj.Termwise.mapMono K (image.ι (θ.unop ≫ (A.pull θ').e) ≫ image.ι (θ'.unop ≫ A.e)))
      (Sigma.ι (Obj.summand K Δ) ((A.pull θ').pull θ)))

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_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 ≫
        𝟙 (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 Δ)
⊢ Eq (α :=
    Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ A ⟶
      Cocone.pt (F := Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))
        (Splitting.cofan' (fun (n : ℕ) ↦ K.X n) (obj K)
          (fun (n : ℕ) ↦ Sigma.ι (Obj.summand K (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌))) Δ))
    (Cofan.inj (colimit.cocone (Discrete.functor (Splitting.summand (fun (n : ℕ) ↦ K.X n) Δ))) A ≫
      Iso.hom
        (Iso.refl
          (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) Δ))))))
    (Cofan.inj
      (Splitting.cofan' (fun (n : ℕ) ↦ K.X n) (obj K)
        (fun (n : ℕ) ↦ Sigma.ι (Obj.summand K (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌))) Δ)
      A)

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_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 Δ
⊢ A.e ≫ 𝟙 (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))) =
    A.e.op.unop ≫ 𝟙 (unop (op (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α })))))

Tactic:
rfl