no goals
C : Type ?u.24
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
⊢ b < n + 1 + 1
simp only [hnbq, Nat.lt_add_one_iff, le_add_iff_nonneg_right, zero_le]
case H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ Fin.succ { val := b, isLt := (_ : b < n + 1 + 1) } < Fin.succ j

case H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ Fin.succ { val := b, isLt := (_ : b < n + 1 + 1) } < Fin.succ j

C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ j ≠ 0

case H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ Fin.succ { val := b, isLt := (_ : b < n + 1 + 1) } < Fin.succ j

case H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ Fin.succ { val := b, isLt := (_ : b < n + 1 + 1) } < Fin.succ j
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ (φ ≫ SimplicialObject.σ X { val := b, isLt := (_ : b < n + 1 + 1) }) ≫ SimplicialObject.δ X (Fin.succ j) = 0
rw [assoc, SimplicialObject.δ_comp_σ_of_gt', Fin.pred_succ, v.comp_δ_eq_zero_assoc _ _ hj,
  zero_comp]
case H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ { val := b + 1, isLt := (_ : Nat.succ b < Nat.succ (n + 2)) } < Fin.succ j
case H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ Fin.succ { val := b, isLt := (_ : b < n + 1 + 1) } < Fin.succ j
dsimp
case H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ↑{ val := b + 1, isLt := (_ : Nat.succ b < Nat.succ (n + 2)) } < ↑j + 1
case H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ { val := b + 1, isLt := (_ : Nat.succ b < Nat.succ (n + 2)) } < Fin.succ j
rw [Fin.lt_iff_val_lt_val, Fin.val_succ]
no goals
case H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ ↑{ val := b + 1, isLt := (_ : Nat.succ b < Nat.succ (n + 2)) } < ↑j + 1
linarith
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
hj' : j = 0
⊢ False
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ j ≠ 0
intro hj'
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj [n + 1].op
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
hj' : j = 0
⊢ False
simp only [hnbq, add_comm b, add_assoc, hj', Fin.val_zero, zero_add, add_le_iff_nonpos_right,
  nonpos_iff_eq_zero, add_eq_zero, false_and] at hj