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 ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst_3 : Mono i
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := obj K) (splitting K)) (op Δ) (Splitting.IndexSet.id (op Δ)) ⟶
      (obj K).obj (op Δ'))
    (Cofan.inj (Splitting.cofan (splitting K) (op Δ)) (Splitting.IndexSet.id (op Δ)) ≫ (obj K).map i.op)
    (Termwise.mapMono K i ≫ Cofan.inj (Splitting.cofan (splitting K) (op Δ')) (Splitting.IndexSet.id (op Δ')))

Tactic:
Obj.map_on_summand K (Splitting.IndexSet.id (op Δ)) i.op (rfl : 𝟙 _ ≫ i = i ≫ 𝟙 _)

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id, Quiver.Hom.op, Opposite.op, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, 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
e : Δ' ⟶ Δ
inst_3 : Epi e
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := obj K) (splitting K)) (op Δ) (Splitting.IndexSet.id (op Δ)) ⟶
      (obj K).obj (op Δ'))
    (Cofan.inj (Splitting.cofan (splitting K) (op Δ)) (Splitting.IndexSet.id (op Δ)) ≫ (obj K).map e.op)
    (Cofan.inj (Splitting.cofan (splitting K) (op Δ')) (Splitting.IndexSet.mk e))

Tactic:
simpa only [Γ₀.Obj.map_on_summand K (Splitting.IndexSet.id (op Δ)) e.op
      (rfl : e ≫ 𝟙 Δ = e ≫ 𝟙 Δ),
    Γ₀.Obj.Termwise.mapMono_id] using id_comp _

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id, Quiver.Hom.op, Opposite.op, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, rfl, 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'_1 : ChainComplex.{v_1, u_1, 0} C ℕ
f_1 : K_1 ⟶ K'_1
Δ_1 Δ'_1 Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
h :
  ∀ (A : Splitting.IndexSet Δ'),
    Eq (α := Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ' A ⟶ (obj K').obj Δ)
      (Cofan.inj (Splitting.cofan (splitting K) Δ') A ≫
        (obj K).map θ ≫
          Splitting.desc (splitting K) Δ fun (A : Splitting.IndexSet Δ) ↦
            f.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
              Cofan.inj (Splitting.cofan (splitting K') Δ) A)
      (CategoryStruct.comp (Y :=
        Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ'))
          (Splitting.cofan (splitting K) Δ'))
        (Cofan.inj (Splitting.cofan (splitting K) Δ') A :
          Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ' A ⟶
            Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ'))
              (Splitting.cofan (splitting K) Δ'))
        ((Splitting.desc (splitting K) Δ' fun (A : Splitting.IndexSet Δ') ↦
              f.f (unop (A.fst (β := fun (Δ'_2 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_2 // Epi α }))).len ≫
                Cofan.inj (Splitting.cofan (splitting K') Δ') A) ≫
            (obj K').map θ :
          (obj K).obj Δ' ⟶ (obj K').obj Δ))
⊢ ((obj K).map θ ≫
      Splitting.desc (splitting K) Δ fun (A : Splitting.IndexSet Δ) ↦
        f.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
          Cofan.inj (Splitting.cofan (splitting K') Δ) A) =
    (Splitting.desc (splitting K) Δ' fun (A : Splitting.IndexSet Δ') ↦
        f.f (unop (A.fst (β := fun (Δ'_2 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_2 // Epi α }))).len ≫
          Cofan.inj (Splitting.cofan (splitting K') Δ') A) ≫
      (obj K').map θ

Tactic:
apply (Γ₀.splitting K).hom_ext'

Premises used: AlgebraicTopology.DoldKan.Γ₀.splitting, CategoryTheory.SimplicialObject.Splitting.hom_ext'
-- 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'_1 : ChainComplex.{v_1, u_1, 0} C ℕ
f_1 : K_1 ⟶ K'_1
Δ_1 Δ'_1 Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
A : Splitting.IndexSet Δ'
h :
  Eq (α := Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ' A ⟶ (obj K').obj Δ)
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Obj.Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (f.f (unop ((A.pull θ).fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        Cofan.inj (Splitting.cofan (splitting K') Δ) (A.pull θ)))
    (f.f (unop (A.fst (β := fun (Δ'_2 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_2 // Epi α }))).len ≫
      CategoryStruct.comp (Y := K'.X (image (θ.unop ≫ A.e)).len) (Obj.Termwise.mapMono K' (image.ι (θ.unop ≫ A.e)))
        (Cofan.inj (Splitting.cofan (splitting K') Δ) (A.pull θ)))
⊢ Eq (α := Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ' A ⟶ (obj K').obj Δ)
    (Cofan.inj (Splitting.cofan (splitting K) Δ') A ≫
      (obj K).map θ ≫
        Splitting.desc (splitting K) Δ fun (A : Splitting.IndexSet Δ) ↦
          f.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
            Cofan.inj (Splitting.cofan (splitting K') Δ) A)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ'))
        (Splitting.cofan (splitting K) Δ'))
      (Cofan.inj (Splitting.cofan (splitting K) Δ') A :
        Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ' A ⟶
          Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ'))
            (Splitting.cofan (splitting K) Δ'))
      ((Splitting.desc (splitting K) Δ' fun (A : Splitting.IndexSet Δ') ↦
            f.f (unop (A.fst (β := fun (Δ'_2 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_2 // Epi α }))).len ≫
              Cofan.inj (Splitting.cofan (splitting K') Δ') A) ≫
          (obj K').map θ :
        (obj K).obj Δ' ⟶ (obj K').obj Δ))

Tactic:
simp only [(splitting K).ι_desc_assoc, Obj.map_on_summand'_assoc K _ θ, (splitting K).ι_desc,
      assoc, Obj.map_on_summand' K' _ θ]

Premises used: CategoryTheory.Category.assoc, AlgebraicTopology.DoldKan.Γ₀.splitting, CategoryTheory.SimplicialObject.Splitting.ι_desc, CategoryTheory.SimplicialObject.Splitting.ι_desc_assoc, 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'_1 : ChainComplex.{v_1, u_1, 0} C ℕ
f_1 : K_1 ⟶ K'_1
Δ_1 Δ'_1 Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
A : Splitting.IndexSet Δ'
⊢ Eq (α := Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ' A ⟶ (obj K').obj Δ)
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Obj.Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (f.f (unop ((A.pull θ).fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
        Cofan.inj (Splitting.cofan (splitting K') Δ) (A.pull θ)))
    (f.f (unop (A.fst (β := fun (Δ'_2 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_2 // Epi α }))).len ≫
      CategoryStruct.comp (Y := K'.X (image (θ.unop ≫ A.e)).len) (Obj.Termwise.mapMono K' (image.ι (θ.unop ≫ A.e)))
        (Cofan.inj (Splitting.cofan (splitting K') Δ) (A.pull θ)))

Tactic:
apply Obj.Termwise.mapMono_naturality_assoc

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality_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'_1 : ChainComplex.{v_1, u_1, 0} C ℕ
f_1 : K_1 ⟶ K'_1
Δ Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
n : ℕ
dsimp :
  Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n ⟶ Γ₀.Obj.obj₂ K' (op ⦋n⦌))
    (Splitting.ι (Γ₀.splitting K) n ≫
      Splitting.desc (Γ₀.splitting K) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
        f.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
          Cofan.inj (Splitting.cofan (Γ₀.splitting K') (op ⦋n⦌)) A)
    (f.f n ≫ Splitting.ι (Γ₀.splitting K') n)
⊢ (Split.mk' (X := Γ₀.obj K) (Γ₀.splitting K)).s.ι n ≫ NatTrans.app (Γ₀.map f) (op ⦋n⦌) =
    f.f n ≫ (Split.mk' (X := Γ₀.obj K') (Γ₀.splitting K')).s.ι n

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'_1 : ChainComplex.{v_1, u_1, 0} C ℕ
f_1 : K_1 ⟶ K'_1
Δ Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
n : ℕ
simp :
  Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n ⟶ Γ₀.Obj.obj₂ K' (op ⦋n⦌))
    (f.f
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
              (Splitting.IndexSet.id (op ⦋n⦌)))).len ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting K') (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
    (f.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting K') (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n ⟶ Γ₀.Obj.obj₂ K' (op ⦋n⦌))
    (Splitting.ι (Γ₀.splitting K) n ≫
      Splitting.desc (Γ₀.splitting K) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
        f.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
          Cofan.inj (Splitting.cofan (Γ₀.splitting K') (op ⦋n⦌)) A)
    (f.f n ≫ Splitting.ι (Γ₀.splitting K') n)

Tactic:
simp only [← Splitting.cofan_inj_id, (Γ₀.splitting K).ι_desc]

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan_inj_id, AlgebraicTopology.DoldKan.Γ₀.splitting, CategoryTheory.SimplicialObject.Splitting.ι_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_1 K'_1 : ChainComplex.{v_1, u_1, 0} C ℕ
f_1 : K_1 ⟶ K'_1
Δ Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
n : ℕ
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n ⟶ Γ₀.Obj.obj₂ K' (op ⦋n⦌))
    (f.f
        (unop
            (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
              (Splitting.IndexSet.id (op ⦋n⦌)))).len ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting K') (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
    (f.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting K') (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))

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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
_ :
  n + 1 ≤ (↑j : ℕ) + (n + 1) →
    Eq (α :=
      Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
          (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
        Γ₀.obj K _⦋n⦌)
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
        (Γ₀.obj K).δ j.succ)
      0
⊢ n + 1 ≤ (↑j : ℕ) + (n + 1) →
    Eq (α :=
      Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
          (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
        Γ₀.obj K _⦋n⦌)
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
        (Γ₀.obj K).δ j.succ)
      0

Tactic:
_
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
    (Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))

Tactic:
have eq := Γ₀.Obj.mapMono_on_summand_id K (SimplexCategory.δ j.succ)
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
eq :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
    (Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
rw :
  ∀
    (eq :
      Eq (α :=
        Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
            (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
          Γ₀.obj K _⦋n⦌)
        (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
          (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
        0),
    Eq (α :=
      Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
          (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
        Γ₀.obj K _⦋n⦌)
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
        (Γ₀.obj K).δ j.succ)
      0
h₁ : ⦋n + 1⦌ ≠ ⦋n⦌
h₂ : ¬Isδ₀ (SimplexCategory.δ j.succ)
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).δ j.succ)
    0

Tactic:
rw [Γ₀.Obj.Termwise.mapMono_eq_zero K, zero_comp] at eq

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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h_1 : n + 1 ≤ (↑j : ℕ) + (n + 1)
eq :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
    (Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
h : ⦋n + 1⦌ = ⦋n⦌
⊢ False

Tactic:
(Nat.succ_ne_self n) (congr_arg SimplexCategory.len h)

Premises used: Nat.succ_ne_self, congr_arg, SimplexCategory.len
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h_1 : n + 1 ≤ (↑j : ℕ) + (n + 1)
eq :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
    (Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
h : ⦋n + 1⦌ = ⦋n⦌
⊢ False

Tactic:
exact (Nat.succ_ne_self n) (congr_arg SimplexCategory.len h)

Premises used: Nat.succ_ne_self, congr_arg, SimplexCategory.len
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h_1 : n + 1 ≤ (↑j : ℕ) + (n + 1)
eq :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
    (Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
h : Isδ₀ (SimplexCategory.δ j.succ)
⊢ j.succ = 0

Tactic:
simpa only [Isδ₀.iff] using h

Premises used: AlgebraicTopology.DoldKan.Isδ₀.iff
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
eq :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
    (Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
⊢ ¬Isδ₀ (SimplexCategory.δ j.succ)

Tactic:
exact fun h => Fin.succ_ne_zero j (by simpa only [Isδ₀.iff] using h)

Premises used: Fin.succ_ne_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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
eq :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
    0
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).δ j.succ)
    0

Tactic:
eq

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂, CategoryTheory.SimplicialObject.Splitting.summand, CategoryTheory.Limits.colimit, CategoryTheory.SimplicialObject.δ
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
eq :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
    0
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).δ j.succ)
    0

Tactic:
exact 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
rw :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
      HomologicalComplex.X K[Γ₀.obj K] n)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f (P n) n))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
      HomologicalComplex.X K[Γ₀.obj K] n)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))

Tactic:
rw [PInfty_f]

Premises used: AlgebraicTopology.DoldKan.PInfty_f
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
zero :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋0⦌) (Splitting.IndexSet.id (op ⦋0⦌)) ⟶
      HomologicalComplex.X K[Γ₀.obj K] 0)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋0⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋0⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋0⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋0⦌)) (Splitting.IndexSet.id (op ⦋0⦌)))
      (HomologicalComplex.Hom.f (P 0) 0))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋0⦌)) (Splitting.IndexSet.id (op ⦋0⦌)))
succ :
  ∀ (n : ℕ),
    Eq (α :=
      Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
          (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
        HomologicalComplex.X K[Γ₀.obj K] (n + 1))
      (CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
          Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
          (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
        (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
        (HomologicalComplex.Hom.f (P (n + 1)) (n + 1)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
      HomologicalComplex.X K[Γ₀.obj K] n)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f (P n) n))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))

Tactic:
rcases n with _ | n