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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ (φ ≫ HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 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 φ
⊢ HigherFacesVanish (q + 1) (φ ≫ HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q) (n + 1))
intro j hj₁
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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ (φ ≫ (𝟙 (X.obj [n + 1].op) + HomologicalComplex.Hom.f (Hσ q) (n + 1))) ≫ δ X (Fin.succ j) = 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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ (φ ≫ HomologicalComplex.Hom.f (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0
dsimp
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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ (φ ≫ (𝟙 (X.obj [n + 1].op) + HomologicalComplex.Hom.f (Hσ q) (n + 1))) ≫ δ X (Fin.succ j) = 0
simp only [comp_add, add_comp, comp_id]
case pos
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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : n < q
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0

case neg
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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : ¬n < q
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0
by_cases hqn : n < q
case neg.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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0
case neg
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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : ¬n < q
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0
cases' Nat.le.dest (not_lt.mp hqn) with a ha
case neg.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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) } ≫ δ X (Fin.succ j)
case neg.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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0
rw [v.comp_Hσ_eq (show n = a + q by linarith), neg_comp, add_neg_eq_zero, assoc, assoc]
case neg.intro.zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a : ℕ
φ : Y ⟶ X.obj [Nat.zero + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.zero + 1)
hj₁ : Nat.zero + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.zero < q
ha : q + a = Nat.zero
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.zero + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ Nat.zero) } ≫ δ X (Fin.succ j)

case neg.intro.succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
case neg.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 φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ n) } ≫ δ X (Fin.succ j)
cases' n with m hm
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : a = ↑j
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
case neg.intro.succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
by_cases hj₂ : a = (j : ℕ)
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
have haj : a < j := (Ne.le_iff_lt hj₂).mp (by linarith)
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
have hj₃ := j.is_lt
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
have ham : a ≤ m := by
  by_contra h
  rw [not_le, ← Nat.succ_le_iff] at h
  linarith
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < Fin.succ j

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < Fin.succ j
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
rw [X.δ_comp_σ_of_gt', j.pred_succ]
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < Fin.succ j

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < Fin.succ j
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < Fin.succ j

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < Fin.succ j
swap
case neg.inl
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))

case neg.inr
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
obtain _ | ham'' := ham.lt_or_eq
no goals
case pos
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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : n < q
⊢ φ ≫ δ X (Fin.succ j) + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ δ X (Fin.succ j) = 0
rw [v.comp_Hσ_eq_zero hqn, zero_comp, add_zero, v j (by linarith)]
no goals
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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : n < q
⊢ n + 1 ≤ ↑j + q
linarith
no goals
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 + 1)
hj₁ : n + 1 ≤ ↑j + (q + 1)
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ n = a + q
linarith
case neg.intro.zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a : ℕ
φ : Y ⟶ X.obj [Nat.zero + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.zero + 1)
hj₁ : Nat.zero + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.zero < q
ha : q + a = Nat.zero
⊢ φ ≫ δ X (Fin.succ 0) = φ ≫ δ X { val := 0 + 1, isLt := (_ : 0 + 1 < Nat.zero + 2) }
case neg.intro.zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a : ℕ
φ : Y ⟶ X.obj [Nat.zero + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.zero + 1)
hj₁ : Nat.zero + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.zero < q
ha : q + a = Nat.zero
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.zero + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ Nat.zero) } ≫ δ X (Fin.succ j)
simp only [Nat.eq_zero_of_add_eq_zero_left ha, Fin.eq_zero j, Fin.mk_zero, Fin.mk_one,
  δ_comp_σ_succ, comp_id]
no goals
case neg.intro.zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a : ℕ
φ : Y ⟶ X.obj [Nat.zero + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.zero + 1)
hj₁ : Nat.zero + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.zero < q
ha : q + a = Nat.zero
⊢ φ ≫ δ X (Fin.succ 0) = φ ≫ δ X { val := 0 + 1, isLt := (_ : 0 + 1 < Nat.zero + 2) }
rfl
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : a = ↑j
⊢ φ ≫ δ X (Fin.succ j) = φ ≫ δ X { val := ↑j + 1, isLt := (_ : ↑j + 1 < Nat.succ m + 2) }
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : a = ↑j
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        σ X { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } ≫ δ X (Fin.succ j)
simp only [hj₂, Fin.eta, δ_comp_σ_succ, comp_id]
no goals
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : a = ↑j
⊢ φ ≫ δ X (Fin.succ j) = φ ≫ δ X { val := ↑j + 1, isLt := (_ : ↑j + 1 < Nat.succ m + 2) }
rfl
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
⊢ a ≤ ↑j
linarith
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
h : ¬a ≤ m
⊢ False
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
⊢ a ≤ m
by_contra h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
h : Nat.succ m ≤ a
⊢ False
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
h : ¬a ≤ m
⊢ False
rw [not_le, ← Nat.succ_le_iff] at h
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
h : Nat.succ m ≤ a
⊢ False
linarith
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ ↑(Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }) < ↑(Fin.succ j)
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < Fin.succ j
rw [Fin.lt_iff_val_lt_val]
no goals
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
⊢ ↑(Fin.succ { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }) < ↑(Fin.succ j)
simpa only [Fin.val_mk, Fin.val_succ, add_lt_add_iff_right] using haj
case neg.inl
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X
            (Fin.castLT { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) }
              (_ : ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } < m + 2)) ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))

case neg.inl.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≤ ↑Fin.castSucc j
case neg.inl
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
rw [← X.δ_comp_δ''_assoc]
case neg.inl.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≤ ↑Fin.castSucc j

case neg.inl
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X
            (Fin.castLT { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) }
              (_ : ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } < m + 2)) ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
case neg.inl
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X
            (Fin.castLT { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) }
              (_ : ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } < m + 2)) ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))

case neg.inl.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≤ ↑Fin.castSucc j
swap
no goals
case neg.inl
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X
            (Fin.castLT { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) }
              (_ : ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } < m + 2)) ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
simp only [← assoc, v j (by linarith), zero_comp]
case neg.inl.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≤ ↑(↑Fin.castSucc j)
case neg.inl.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≤ ↑Fin.castSucc j
rw [Fin.le_iff_val_le_val]
case neg.inl.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ a + 1 ≤ ↑j
case neg.inl.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≤ ↑(↑Fin.castSucc j)
dsimp
no goals
case neg.inl.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ a + 1 ≤ ↑j
linarith
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
h✝ : a < m
⊢ Nat.succ m + 1 ≤ ↑j + q
linarith
case neg.inr
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))

case neg.inr.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } = ↑Fin.castSucc j
case neg.inr
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
rw [X.δ_comp_δ_self'_assoc]
case neg.inr.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } = ↑Fin.castSucc j

case neg.inr
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
case neg.inr
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))

case neg.inr.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } = ↑Fin.castSucc j
swap
no goals
case neg.inr
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ δ X (Fin.succ j) =
    φ ≫
      δ X (Fin.succ j) ≫
        δ X j ≫
          σ X
            (Fin.castLT { val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) }
              (_ : ↑{ val := a, isLt := (_ : a < Nat.succ (Nat.succ m)) } < m + 1))
simp only [← assoc, v j (by linarith), zero_comp]
case neg.inr.H.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } = ↑(↑Fin.castSucc j)
case neg.inr.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } = ↑Fin.castSucc j
ext
case neg.inr.H.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ a + 1 = ↑j
case neg.inr.H.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ ↑{ val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (Nat.succ m + 1)) } = ↑(↑Fin.castSucc j)
dsimp
no goals
case neg.inr.H.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ a + 1 = ↑j
linarith
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
q a m : ℕ
φ : Y ⟶ X.obj [Nat.succ m + 1].op
v : HigherFacesVanish q φ
j : Fin (Nat.succ m + 1)
hj₁ : Nat.succ m + 1 ≤ ↑j + (q + 1)
hqn : ¬Nat.succ m < q
ha : q + a = Nat.succ m
hj₂ : ¬a = ↑j
haj : a < ↑j
hj₃ : ↑j < Nat.succ m + 1
ham : a ≤ m
ham'' : a = m
⊢ Nat.succ m + 1 ≤ ↑j + q
linarith