case h.zero
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) Nat.zero =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) Nat.zero

case h.succ
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) (Nat.succ n) =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) (Nat.succ n)
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X ≫ PInfty = inclusionOfMooreComplexMap X
ext (_|n)
case h.zero
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0 ≫ 𝟙 (X.obj (SimplexCategory.mk 0).op) =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0
case h.zero
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) Nat.zero =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) Nat.zero
dsimp
no goals
case h.zero
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0 ≫ 𝟙 (X.obj (SimplexCategory.mk 0).op) =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0
simp only [comp_id]
no goals
case h.succ
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) (Nat.succ n) =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) (Nat.succ n)
exact (HigherFacesVanish.inclusionOfMooreComplexMap n).comp_P_eq_self