case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X : SimplicialObject C
⊢ factorThru (objX X (0 + 1)) (arrow (objX X (0 + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (0 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      arrow (objX X (0 + 1)) ≫ SimplicialObject.δ X 0 ≫ inv (arrow ⊤) =
    0

case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ factorThru (objX X (Nat.succ n + 0 + 1)) (arrow (objX X (Nat.succ n + 0 + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (Nat.succ n + 0 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      factorThru (objX X (n + 1)) (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)) =
    0
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ objD X (n + 1) ≫ objD X n = 0
rcases n with _ | n <;> dsimp [objD]
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ factorThru (objX X (Nat.succ n + 0 + 1)) (arrow (objX X (Nat.succ n + 0 + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (Nat.succ n + 0 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      factorThru (objX X (n + 1)) (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)) =
    0
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X : SimplicialObject C
⊢ factorThru (objX X (0 + 1)) (arrow (objX X (0 + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (0 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      arrow (objX X (0 + 1)) ≫ SimplicialObject.δ X 0 ≫ inv (arrow ⊤) =
    0

case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ factorThru (objX X (Nat.succ n + 0 + 1)) (arrow (objX X (Nat.succ n + 0 + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (Nat.succ n + 0 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      factorThru (objX X (n + 1)) (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)) =
    0
. erw [Subobject.factorThru_arrow_assoc, Category.assoc,
    ← X.δ_comp_δ_assoc (Fin.zero_le (0 : Fin 2)),
    ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin 2) (by simp)),
    Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
no goals
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ factorThru (objX X (Nat.succ n + 0 + 1)) (arrow (objX X (Nat.succ n + 0 + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (Nat.succ n + 0 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      factorThru (objX X (n + 1)) (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)) =
    0
. erw [factorThru_right, factorThru_eq_zero, factorThru_arrow_assoc, Category.assoc,
    ← X.δ_comp_δ (Fin.zero_le (0 : Fin (n + 3))),
    ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin (n + 3)) (by simp)),
    Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
no goals
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X : SimplicialObject C
⊢ factorThru (objX X (0 + 1)) (arrow (objX X (0 + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (0 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      arrow (objX X (0 + 1)) ≫ SimplicialObject.δ X 0 ≫ inv (arrow ⊤) =
    0
erw [Subobject.factorThru_arrow_assoc, Category.assoc,
  ← X.δ_comp_δ_assoc (Fin.zero_le (0 : Fin 2)),
  ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin 2) (by simp)),
  Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X : SimplicialObject C
⊢ 0 ∈ Finset.univ
simp
no goals
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ factorThru (objX X (Nat.succ n + 0 + 1)) (arrow (objX X (Nat.succ n + 0 + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (Nat.succ n + 0 + 1 + 1)) ≫ SimplicialObject.δ X 0)) ≫
      factorThru (objX X (n + 1)) (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)
        (_ :
          Factors (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k)))
            (arrow (objX X (n + 1 + 1)) ≫ SimplicialObject.δ X 0)) =
    0
erw [factorThru_right, factorThru_eq_zero, factorThru_arrow_assoc, Category.assoc,
  ← X.δ_comp_δ (Fin.zero_le (0 : Fin (n + 3))),
  ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin (n + 3)) (by simp)),
  Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ 0 ∈ Finset.univ
simp