case zero
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
⊢ Factors (NormalizedMooreComplex.objX X Nat.zero) (HomologicalComplex.Hom.f PInfty Nat.zero)

case succ
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ Factors (NormalizedMooreComplex.objX X (Nat.succ n)) (HomologicalComplex.Hom.f PInfty (Nat.succ n))
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ Factors (NormalizedMooreComplex.objX X n) (HomologicalComplex.Hom.f PInfty n)
rcases n with _|n
no goals
case zero
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
⊢ Factors (NormalizedMooreComplex.objX X Nat.zero) (HomologicalComplex.Hom.f PInfty Nat.zero)
apply top_factors
case succ
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ ∀ (i : Fin (n + 1)),
    i ∈ Finset.univ →
      Factors (kernelSubobject (SimplicialObject.δ X (Fin.succ i)))
        (HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n))
case succ
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ Factors (NormalizedMooreComplex.objX X (Nat.succ n)) (HomologicalComplex.Hom.f PInfty (Nat.succ n))
rw [PInfty_f, NormalizedMooreComplex.objX, finset_inf_factors]
case succ
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ Factors (kernelSubobject (SimplicialObject.δ X (Fin.succ i))) (HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n))
case succ
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ ∀ (i : Fin (n + 1)),
    i ∈ Finset.univ →
      Factors (kernelSubobject (SimplicialObject.δ X (Fin.succ i)))
        (HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n))
intro i _
case succ.w
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n) ≫ SimplicialObject.δ X (Fin.succ i) = 0
case succ
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ Factors (kernelSubobject (SimplicialObject.δ X (Fin.succ i))) (HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n))
apply kernelSubobject_factors
no goals
case succ.w
A : Type u_2
inst✝¹ : Category A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n) ≫ SimplicialObject.δ X (Fin.succ i) = 0
exact (HigherFacesVanish.of_P (n + 1) n) i le_add_self