awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
q : ℕ
hq :
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P q)
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
succ :
  HAdd.hAdd (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ Hσ q) =
    HAdd.hAdd (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
      (P q ≫ Hσ q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P (q + 1))
    (P (q + 1) ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)

Tactic:
simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
q : ℕ
hq :
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P q)
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
succ :
  HAdd.hAdd (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
      (P q ≫ NatTrans.app (natTransHσ q) x ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) =
    HAdd.hAdd (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
      (P q ≫ Hσ q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
⊢ HAdd.hAdd (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ Hσ q) =
    HAdd.hAdd (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
      (P q ≫ Hσ q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)

Tactic:
erw [(natTransHσ q).naturality f]

Premises used: AlgebraicTopology.DoldKan.natTransHσ, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
q : ℕ
hq :
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P q)
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
⊢ HAdd.hAdd (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
      (P q ≫ NatTrans.app (natTransHσ q) x ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f) =
    HAdd.hAdd (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
      (P q ≫ Hσ q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q : ℕ
x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
zero :
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P 0)
    (P 0 ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
succ :
  ∀ (q : ℕ)
    (hq :
      Eq (α :=
        Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
          (Functor.obj (alternatingFaceMapComplex C) x_1))
        (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P q)
        (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)),
    Eq (α :=
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
        (Functor.obj (alternatingFaceMapComplex C) x_1))
      (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P (q + 1))
      (P (q + 1) ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj (alternatingFaceMapComplex C) x)
      (Functor.obj (alternatingFaceMapComplex C) x_1))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C) f ≫ P q)
    (P q ≫ CategoryTheory.Functor.map (alternatingFaceMapComplex C) f)

Tactic:
induction q with
    | zero =>
      dsimp [alternatingFaceMapComplex]
      simp only [P_zero, id_comp, comp_id]
    | succ q hq =>
      simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]
      -- `erw` is needed to see through `natTransHσ q).app = Hσ q`
      erw [(natTransHσ q).naturality f]
      rfl

Premises used: CategoryTheory.Category.assoc, AlgebraicTopology.DoldKan.natTransHσ, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, CategoryTheory.Preadditive.add_comp, CategoryTheory.NatTrans.naturality, CategoryTheory.Preadditive.comp_add, AlgebraicTopology.DoldKan.P_zero, AlgebraicTopology.alternatingFaceMapComplex, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[Y] n) (f.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f (P q) n)
    (HomologicalComplex.Hom.f (P q) n ≫ f.app (op ⦋n⦌))

Tactic:
HomologicalComplex.congr_hom ((natTransP q).naturality f) n

Premises used: CategoryTheory.NatTrans.naturality, HomologicalComplex.congr_hom, AlgebraicTopology.DoldKan.natTransP
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
simp : f.app (op ⦋n⦌) ≫ 𝟙 (HomologicalComplex.X K[Y] n) = 𝟙 (HomologicalComplex.X K[X] n) ≫ f.app (op ⦋n⦌)
⊢ Eq (α := X _⦋n⦌ ⟶ HomologicalComplex.X K[Y] n) (f.app (op ⦋n⦌) ≫ HomologicalComplex.Hom.f (Q q) n)
    (HomologicalComplex.Hom.f (Q q) n ≫ f.app (op ⦋n⦌))

Tactic:
simp only [Q, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, P_f_naturality,
    sub_comp, sub_left_inj]

Premises used: HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, sub_left_inj, AlgebraicTopology.DoldKan.Q, CategoryTheory.Preadditive.comp_sub, AlgebraicTopology.DoldKan.P_f_naturality, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
dsimp : f.app (op ⦋n⦌) ≫ 𝟙 (Y _⦋n⦌) = 𝟙 (X _⦋n⦌) ≫ f.app (op ⦋n⦌)
⊢ f.app (op ⦋n⦌) ≫ 𝟙 (HomologicalComplex.X K[Y] n) = 𝟙 (HomologicalComplex.X K[X] n) ≫ f.app (op ⦋n⦌)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
q n : ℕ
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
⊢ f.app (op ⦋n⦌) ≫ 𝟙 (Y _⦋n⦌) = 𝟙 (X _⦋n⦌) ≫ f.app (op ⦋n⦌)

Tactic:
simp only [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
n : ℕ
zero :
  Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (𝟙 K[X]) n))
    (HomologicalComplex.Hom.f (𝟙 K[(Functor.obj (whiskering C D) G).obj X]) n)
⊢ Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (P 0) n)) (HomologicalComplex.Hom.f (P 0) n)

Tactic:
simp only [P_zero]

Premises used: AlgebraicTopology.DoldKan.P_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
n : ℕ
⊢ Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (𝟙 K[X]) n))
    (HomologicalComplex.Hom.f (𝟙 K[(Functor.obj (whiskering C D) G).obj X]) n)

Tactic:
apply G.map_id

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
n q : ℕ
hq :
  Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (P q) n)) (HomologicalComplex.Hom.f (P q) n)
⊢ Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (P (q + 1)) n)) (HomologicalComplex.Hom.f (P (q + 1)) n)

Tactic:
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
      comp_id, Functor.map_add, Functor.map_comp, hq, map_Hσ]

Premises used: HomologicalComplex.add_f_apply, AlgebraicTopology.DoldKan.map_Hσ, CategoryTheory.Functor.map_add, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, HomologicalComplex.comp_f, CategoryTheory.Preadditive.comp_add, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
zero :
  Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (P 0) n)) (HomologicalComplex.Hom.f (P 0) n)
succ :
  ∀ (q : ℕ)
    (hq :
      Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
        (G.map (HomologicalComplex.Hom.f (P q) n)) (HomologicalComplex.Hom.f (P q) n)),
    Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
      (G.map (HomologicalComplex.Hom.f (P (q + 1)) n)) (HomologicalComplex.Hom.f (P (q + 1)) n)
⊢ Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (P q) n)) (HomologicalComplex.Hom.f (P q) n)

Tactic:
induction q with
  | zero =>
    simp only [P_zero]
    apply G.map_id
  | succ q hq =>
    simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
      comp_id, Functor.map_add, Functor.map_comp, hq, map_Hσ]

Premises used: HomologicalComplex.add_f_apply, AlgebraicTopology.DoldKan.map_Hσ, CategoryTheory.Functor.map_add, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, HomologicalComplex.comp_f, CategoryTheory.Functor.map_id, CategoryTheory.Preadditive.comp_add, AlgebraicTopology.DoldKan.P_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
rw : G.map (𝟙 (X _⦋n⦌)) = 𝟙 ((Functor.obj (whiskering C D) G).obj X _⦋n⦌)
⊢ Eq (α := G.obj (HomologicalComplex.X K[X] n) ⟶ G.obj (HomologicalComplex.X K[X] n))
    (G.map (HomologicalComplex.Hom.f (Q q) n)) (HomologicalComplex.Hom.f (Q q) n)

Tactic:
rw [← add_right_inj (G.map ((P q : K[X] ⟶ _).f n)), ← G.map_add, map_P G X q n, P_add_Q_f,
    P_add_Q_f]

Premises used: HomologicalComplex.Hom.f, CategoryTheory.Functor.map_add, CategoryTheory.Functor.map, AlgebraicTopology.DoldKan.map_P, add_right_inj, AlgebraicTopology.DoldKan.P_add_Q_f, AlgebraicTopology.DoldKan.P
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Preadditive.{v_2, u_2} D
G : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : G.Additive
X : SimplicialObject.{v_1, u_1} C
q n : ℕ
⊢ G.map (𝟙 (X _⦋n⦌)) = 𝟙 ((Functor.obj (whiskering C D) G).obj X _⦋n⦌)

Tactic:
apply G.map_id

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
pos :
  (h : B = A) →
    s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
neg :
  (h : ¬B = A) →
    s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
⊢ s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len

Tactic:
by_cases h : B = A
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B = A
subst :
  s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len =
    s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len
⊢ s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len =
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len

Tactic:
subst h
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
B : IndexSet Δ
⊢ s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len =
    s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B = A
⊢ s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len

Tactic:
exact eqToHom (by subst h; rfl)

Premises used: CategoryTheory.eqToHom
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : ¬B = A
⊢ s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len

Tactic:
exact 0
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ s.πSummand A = 𝟙 (summand s.N Δ A)

Tactic:
simp [πSummand]

Premises used: CategoryTheory.SimplicialObject.Splitting.πSummand
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
dsimp :
  Eq (α :=
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len)
    ((s.cofan Δ).inj A ≫ s.desc Δ fun (B_1 : IndexSet Δ) ↦ if h : B_1 = B then eqToHom ⋯ else 0) 0
⊢ (s.cofan Δ).inj A ≫ s.πSummand B = 0

Tactic:
dsimp [πSummand]

Premises used: CategoryTheory.SimplicialObject.Splitting.πSummand
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : HasZeroMorphisms.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
rw :
  Eq.{v_1 + 1} (α :=
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len)
    (if h : A = B then eqToHom ⋯ else 0) 0
rw₁ rw₂ :
  Eq.{v_1 + 1} (α :=
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len)
    0 0
⊢ Eq (α :=
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶
      s.N (unop (B.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len)
    ((s.cofan Δ).inj A ≫ s.desc Δ fun (B_1 : IndexSet Δ) ↦ if h : B_1 = B then eqToHom ⋯ else 0) 0

Tactic:
rw [ι_desc, dif_neg h.symm]

Premises used: Ne.symm, dif_neg, CategoryTheory.SimplicialObject.Splitting.ι_desc
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
h :
  ∀ (A : IndexSet Δ),
    (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A
⊢ Eq.{v_1 + 1} (α := X.obj Δ ⟶ X.obj Δ) (𝟙 (X.obj Δ)) (∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A)

Tactic:
apply s.hom_ext'

Premises used: CategoryTheory.SimplicialObject.Splitting.hom_ext'
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h : (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A
⊢ (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
h :
  ∀ (b : IndexSet Δ),
    Membership.mem (γ := Finset (IndexSet Δ)) Finset.univ b →
      b ≠ A → (s.cofan Δ).inj A ≫ s.πSummand b ≫ (s.cofan Δ).inj b = 0
h₁ : A ∉ Finset.univ → (s.cofan Δ).inj A ≫ s.πSummand A ≫ (s.cofan Δ).inj A = 0
⊢ (s.cofan Δ).inj A ≫ 𝟙 (X.obj Δ) = (s.cofan Δ).inj A ≫ ∑ A : IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A

Tactic:
erw [comp_id, comp_sum, Finset.sum_eq_single A, cofan_inj_πSummand_eq_id_assoc]

Premises used: CategoryTheory.Category.comp_id, Finset.sum_eq_single, CategoryTheory.Preadditive.comp_sum, CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_id_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h :
  Membership.mem (γ := Finset (IndexSet Δ)) Finset.univ B →
    B ≠ A → (s.cofan Δ).inj A ≫ s.πSummand B ≫ (s.cofan Δ).inj B = 0
⊢ Membership.mem (γ := Finset (IndexSet Δ)) Finset.univ B →
    B ≠ A → (s.cofan Δ).inj A ≫ s.πSummand B ≫ (s.cofan Δ).inj B = 0

Tactic:
_
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h_1 : Membership.mem (γ := Finset (IndexSet Δ)) Finset.univ B
h₂ : B ≠ A
h :
  Eq (α := s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ X.obj Δ)
    (0 ≫ (s.cofan Δ).inj B) 0
h₁ h₃ :
  Eq.{v_1 + 1} (α :=
    s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ X.obj Δ) 0 0
⊢ (s.cofan Δ).inj A ≫ s.πSummand B ≫ (s.cofan Δ).inj B = 0

Tactic:
rw [s.cofan_inj_πSummand_eq_zero_assoc _ _ h₂, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, CategoryTheory.SimplicialObject.Splitting.cofan_inj_πSummand_eq_zero_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A ∉ Finset.univ → (s.cofan Δ).inj A ≫ s.πSummand A ≫ (s.cofan Δ).inj A = 0

Tactic:
simp