case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hqn : Nat.zero ≤ q
⊢ HomologicalComplex.Hom.f (P (q + 1)) Nat.zero = HomologicalComplex.Hom.f (P q) Nat.zero

case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : Nat.succ n ≤ q
⊢ HomologicalComplex.Hom.f (P (q + 1)) (Nat.succ n) = HomologicalComplex.Hom.f (P q) (Nat.succ n)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : n ≤ q
⊢ HomologicalComplex.Hom.f (P (q + 1)) n = HomologicalComplex.Hom.f (P q) n
rcases n with (_|n)
no goals
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hqn : Nat.zero ≤ q
⊢ HomologicalComplex.Hom.f (P (q + 1)) Nat.zero = HomologicalComplex.Hom.f (P q) Nat.zero
simp only [Nat.zero_eq, P_f_0_eq]
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : Nat.succ n ≤ q
⊢ HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ HomologicalComplex.Hom.f (Hσ q) (Nat.succ n) = 0
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : Nat.succ n ≤ q
⊢ HomologicalComplex.Hom.f (P (q + 1)) (Nat.succ n) = HomologicalComplex.Hom.f (P q) (Nat.succ n)
simp only [P_succ, add_right_eq_self, comp_add, HomologicalComplex.comp_f,
  HomologicalComplex.add_f_apply, comp_id]
no goals
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hqn : Nat.succ n ≤ q
⊢ HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ HomologicalComplex.Hom.f (Hσ q) (Nat.succ n) = 0
exact (HigherFacesVanish.of_P q n).comp_Hσ_eq_zero (Nat.succ_le_iff.mp hqn)