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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ 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⦌)))

Tactic:
simpa only [P_f_0_eq] using comp_id _

Premises used: AlgebraicTopology.DoldKan.P_f_0_eq, 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
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⦌)))

Tactic:
(HigherFacesVanish.on_Γ₀_summand_id K n).comp_P_eq_self

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id, AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂, CategoryTheory.Limits.colimit, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self
-- 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 : ℕ
⊢ 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⦌)))

Tactic:
exact (HigherFacesVanish.on_Γ₀_summand_id K n).comp_P_eq_self

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorN
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
      (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C) ⋙ N₂) X)) (Karoubi.X (Functor.obj N₁ X)))
    (Karoubi.Hom.f (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) PInfty

Tactic:
rfl

Premises used: AlgebraicTopology.DoldKan.PInfty, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorN
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Karoubi.X (Functor.obj N₁ X))
      (Karoubi.X (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C) ⋙ N₂) X)))
    (Karoubi.Hom.f (NatTrans.app (Iso.inv toKaroubiCompN₂IsoN₁) X)) PInfty

Tactic:
rfl

Premises used: AlgebraicTopology.DoldKan.PInfty, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ℕ
dsimp :
  𝟙 (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1)) ≫ K.d (n + 1) n =
    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⦌)) :
          Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
              (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
            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⦌)))
        (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ K (op ⦋n⦌))
            (HomologicalComplex.d (AlternatingFaceMapComplex.obj (Γ₀.obj K)) (n + 1) n)
            (Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
          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⦌)) ⟶
            Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n) ≫
      𝟙 (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
⊢ Eq (α := HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) (n + 1) ⟶ K.X n)
    (CategoryStruct.comp (Y := K.X (n + 1))
      (Iso.hom
        ((fun (x : ℕ) ↦
            (Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x) :
              HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x ≅
                HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x))
          (n + 1)))
      (K.d (n + 1) n))
    (HomologicalComplex.d (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) (n + 1) n ≫
      Iso.hom
        ((fun (x : ℕ) ↦
            (Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x) :
              HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x ≅
                HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x))
          n))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ℕ
simp :
  Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (∑ j : Fin (n + 2),
      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⦌)))
        ((HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • (Γ₀.obj K).δ j) ≫
          Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))
⊢ 𝟙 (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1)) ≫ K.d (n + 1) n =
    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⦌)) :
          Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
              (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
            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⦌)))
        (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ K (op ⦋n⦌))
            (HomologicalComplex.d (AlternatingFaceMapComplex.obj (Γ₀.obj K)) (n + 1) n)
            (Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
          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⦌)) ⟶
            Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n) ≫
      𝟙 (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)

Tactic:
simp only [id_comp, comp_id, AlternatingFaceMapComplex.obj_d_eq, Preadditive.sum_comp,
        Preadditive.comp_sum]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.Category.comp_id, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (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⦌)))
      (HSMul.hSMul (β := Γ₀.obj K _⦋n + 1⦌ ⟶ Γ₀.obj K _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) ((Γ₀.obj K).δ 0) ≫
        Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))
rw₁ :
  ∀ (x : Fin (n + 2)),
    x ≠ 0 →
      Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
        (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⦌)))
            ((HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • (Γ₀.obj K).δ x) ≫
              Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
          Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
        (0 : Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (∑ j : Fin (n + 2),
      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⦌)))
        ((HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • (Γ₀.obj K).δ j) ≫
          Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))

Tactic:
rw [Fintype.sum_eq_single (0 : Fin (n + 2))]

Premises used: OfNat.ofNat, Fintype.sum_eq_single
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ℕ
simp :
  Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (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⦌)))
      ((Γ₀.obj K).δ 0 ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (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⦌)))
      (HSMul.hSMul (β := Γ₀.obj K _⦋n + 1⦌ ⟶ Γ₀.obj K _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) ((Γ₀.obj K).δ 0) ≫
        Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))

Tactic:
simp only [Fin.val_zero, pow_zero, one_zsmul]

Premises used: pow_zero, one_zsmul, Fin.val_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (K.d (n + 1) n ≫
      𝟙 (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌))))
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (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⦌)))
      ((Γ₀.obj K).δ 0 ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))

Tactic:
rw [δ, Γ₀.Obj.mapMono_on_summand_id_assoc, Γ₀.Obj.Termwise.mapMono_δ₀,
          Splitting.cofan_inj_πSummand_eq_id]

Premises used: CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_id, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, CategoryTheory.SimplicialObject.δ, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ℕ
dsimp : Eq (α := K.X (n + 1) ⟶ K.X n) (K.d (n + 1) n) (K.d (n + 1) n ≫ 𝟙 (K.X n))
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (K.d (n + 1) n ≫
      𝟙 (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌))))

Tactic:
dsimp only [Γ₀.splitting, Splitting.summand.eq_1, Splitting.IndexSet.id_fst]

Premises used: CategoryTheory.SimplicialObject.Splitting.IndexSet.id_fst, AlgebraicTopology.DoldKan.Γ₀.splitting, CategoryTheory.SimplicialObject.Splitting.summand.eq_1
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 rw₁ : Eq (α := K.X (n + 1) ⟶ K.X n) (K.d (n + 1) n) (K.d (n + 1) n)
⊢ Eq (α := K.X (n + 1) ⟶ K.X n) (K.d (n + 1) n) (K.d (n + 1) n ≫ 𝟙 (K.X n))

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ℕ
i : Fin (n + 2)
hi : i ≠ 0
dsimp :
  Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
    (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⦌)))
        ((HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • (Γ₀.obj K).δ i) ≫
          Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
      Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
    (0 : Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
    (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⦌)))
        ((HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • (Γ₀.obj K).δ i) ≫
          Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
      Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
    (0 : Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ℕ
i : Fin (n + 2)
hi : i ≠ 0
simp :
  HSMul.hSMul (β :=
      Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
      (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
      (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⦌)))
          ((Γ₀.obj K).δ i ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
        Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n) =
    0
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
    (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⦌)))
        ((HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • (Γ₀.obj K).δ i) ≫
          Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
      Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
    (0 : Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)

Tactic:
simp only [Preadditive.zsmul_comp, Preadditive.comp_zsmul]

Premises used: CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Preadditive.zsmul_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h₁ : ⦋n + 1⦌ ≠ ⦋n⦌
h₂ : ¬Isδ₀ (SimplexCategory.δ i)
⊢ HSMul.hSMul (β :=
      Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
      (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
      (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⦌)))
          ((Γ₀.obj K).δ i ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
        Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n) =
    0

Tactic:
rw [δ, Γ₀.Obj.mapMono_on_summand_id_assoc, Γ₀.Obj.Termwise.mapMono_eq_zero, zero_comp,
          zsmul_zero]

Premises used: zsmul_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero, CategoryTheory.Limits.zero_comp, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, CategoryTheory.SimplicialObject.δ
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : ⦋n + 1⦌ = ⦋n⦌
⊢ ⦋n + 1⦌.len = ⦋n⦌.len

Tactic:
replace h := congr_arg SimplexCategory.len h
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : ⦋n + 1⦌.len = ⦋n⦌.len
⊢ n + 1 = n

Tactic:
change n + 1 = n at h
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : n + 1 = n
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ i)

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

Premises used: AlgebraicTopology.DoldKan.Isδ₀.iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN
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 ℕ
w :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) i ⟶
        (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.hom (Iso.app N₁Γ₀ K))) i)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f
          (Iso.hom
            (Iso.symm (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≪≫
              mapIso (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₀NondegComplexIso K))))
        i)
⊢ Eq (α := obj (Γ₀ ⋙ N₁) K ≅ obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K) (Iso.app N₁Γ₀ K)
    (Iso.symm (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≪≫
      mapIso (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₀NondegComplexIso K))

Tactic:
ext