A : Type u_1
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
      SimplicialObject.δ X (Fin.succ j) =
    0
A : Type u_1
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ HomologicalComplex.Hom.f (AlgebraicTopology.inclusionOfMooreComplexMap X) (n + 1) ≫
      SimplicialObject.δ X (Fin.succ j) =
    0
dsimp [AlgebraicTopology.inclusionOfMooreComplexMap, NormalizedMooreComplex.objX]
no goals
A : Type u_1
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
      SimplicialObject.δ X (Fin.succ j) =
    0
rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j
  (by simp only [Finset.mem_univ])), assoc, kernelSubobject_arrow_comp, comp_zero]
no goals
A : Type u_1
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ j ∈ Finset.univ
simp only [Finset.mem_univ]