case intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : Fin.succ i ≠ 0
hj₂ : n + 2 ≤ ↑(Fin.succ i) + q
⊢ φ ≫ δ X (Fin.succ i) = 0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
j : Fin (n + 2)
hj₁ : j ≠ 0
hj₂ : n + 2 ≤ ↑j + q
⊢ φ ≫ δ X j = 0
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero hj₁
case intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : Fin.succ i ≠ 0
hj₂ : n + 2 ≤ ↑(Fin.succ i) + q
⊢ n + 1 ≤ ↑i + q
case intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : Fin.succ i ≠ 0
hj₂ : n + 2 ≤ ↑(Fin.succ i) + q
⊢ φ ≫ δ X (Fin.succ i) = 0
apply v i
case intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : Fin.succ i ≠ 0
hj₂ : n + 2 ≤ ↑i + 1 + q
⊢ n + 1 ≤ ↑i + q
case intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : Fin.succ i ≠ 0
hj₂ : n + 2 ≤ ↑(Fin.succ i) + q
⊢ n + 1 ≤ ↑i + q
simp only [Fin.val_succ] at hj₂
no goals
case intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
i : Fin (n + 1)
hj₁ : Fin.succ i ≠ 0
hj₂ : n + 2 ≤ ↑i + 1 + q
⊢ n + 1 ≤ ↑i + q
linarith