[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.28, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
⊢ b < n + 1 + 1
[PROOFSTEP]
simp only [hnbq, Nat.lt_add_one_iff, le_add_iff_nonneg_right, zero_le]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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
[PROOFSTEP]
rw [assoc, SimplicialObject.δ_comp_σ_of_gt', Fin.pred_succ, v.comp_δ_eq_zero_assoc _ _ hj, zero_comp]
[GOAL]
case H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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
[PROOFSTEP]
dsimp
[GOAL]
case H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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
[PROOFSTEP]
rw [Fin.lt_iff_val_lt_val, Fin.val_succ]
[GOAL]
case H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
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
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
⊢ j ≠ 0
[PROOFSTEP]
intro hj'
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
Y : C
X : SimplicialObject C
n b q : ℕ
φ : Y ⟶ X.obj (Opposite.op [n + 1])
v : HigherFacesVanish q φ
hnbq : n + 1 = b + q
j : Fin (n + 1 + 1)
hj : n + 1 + 1 ≤ ↑j + q
hj' : j = 0
⊢ False
[PROOFSTEP]
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 
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
[PROOFSTEP]
revert i hi
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
⊢ ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
[PROOFSTEP]
induction' q with q hq
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ ∀ (i : Fin (n + 1)),
    n + 1 ≤ ↑i + Nat.zero → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P Nat.zero) (n + 1) = 0
[PROOFSTEP]
intro i (hi : n + 1 ≤ i)
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ ↑i
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P Nat.zero) (n + 1) = 0
[PROOFSTEP]
exfalso
[GOAL]
case zero.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
hi : n + 1 ≤ ↑i
⊢ False
[PROOFSTEP]
linarith [Fin.is_lt i]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
⊢ ∀ (i : Fin (n + 1)),
    n + 1 ≤ ↑i + Nat.succ q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
intro i (hi : n + 1 ≤ i + q + 1)
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
by_cases n + 1 ≤ (i : ℕ) + q
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
by_cases n + 1 ≤ (i : ℕ) + q
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
h : n + 1 ≤ ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
h : ¬n + 1 ≤ ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
replace hi : n = i + q := by
  obtain ⟨j, hj⟩ := le_iff_exists_add.mp hi
  rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, hj, not_lt, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at h 
  rw [← add_left_inj 1, hj, self_eq_add_right, h]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
h : ¬n + 1 ≤ ↑i + q
⊢ n = ↑i + q
[PROOFSTEP]
obtain ⟨j, hj⟩ := le_iff_exists_add.mp hi
[GOAL]
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
h : ¬n + 1 ≤ ↑i + q
j : ℕ
hj : ↑i + q + 1 = n + 1 + j
⊢ n = ↑i + q
[PROOFSTEP]
rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, hj, not_lt, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at h 
[GOAL]
case intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
hi : n + 1 ≤ ↑i + q + 1
j : ℕ
h : j = 0
hj : ↑i + q + 1 = n + 1 + j
⊢ n = ↑i + q
[PROOFSTEP]
rw [← add_left_inj 1, hj, self_eq_add_right, h]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n q : ℕ
hq : ∀ (i : Fin (n + 1)), n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (n + 1) = 0
i : Fin (n + 1)
h : ¬n + 1 ≤ ↑i + q
hi : n = ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = 0
[PROOFSTEP]
rcases n with _ | n
[GOAL]
case neg.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
i : Fin (Nat.zero + 1)
h : ¬Nat.zero + 1 ≤ ↑i + q
hi : Nat.zero = ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (Nat.zero + 1) = 0
[PROOFSTEP]
fin_cases i
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬Nat.zero + 1 ≤ ↑{ val := 0, isLt := (_ : 0 < Nat.zero + 1) } + q
hi : Nat.zero = ↑{ val := 0, isLt := (_ : 0 < Nat.zero + 1) } + q
⊢ SimplicialObject.σ X { val := 0, isLt := (_ : 0 < Nat.zero + 1) } ≫
      HomologicalComplex.Hom.f (P (Nat.succ q)) (Nat.zero + 1) =
    0
[PROOFSTEP]
dsimp at h hi 
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X { val := 0, isLt := (_ : 0 < Nat.zero + 1) } ≫
      HomologicalComplex.Hom.f (P (Nat.succ q)) (Nat.zero + 1) =
    0
[PROOFSTEP]
rw [show q = 0 by linarith]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ q = 0
[PROOFSTEP]
linarith
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X { val := 0, isLt := (_ : 0 < Nat.zero + 1) } ≫
      HomologicalComplex.Hom.f (P (Nat.succ 0)) (Nat.zero + 1) =
    0
[PROOFSTEP]
change X.σ 0 ≫ (P 1).f 1 = 0
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X 0 ≫ HomologicalComplex.Hom.f (P 1) 1 = 0
[PROOFSTEP]
simp only [P_succ, HomologicalComplex.add_f_apply, comp_add, HomologicalComplex.id_f,
  AlternatingFaceMapComplex.obj_d_eq, Hσ, HomologicalComplex.comp_f,
  Homotopy.nullHomotopicMap'_f (c_mk 2 1 rfl) (c_mk 1 0 rfl), comp_id]
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X 0 ≫ HomologicalComplex.Hom.f (P 0) 1 +
      (SimplicialObject.σ X 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            (Finset.sum Finset.univ fun i => (-1) ^ ↑i • SimplicialObject.δ X i) ≫
              hσ' 0 0 1 (_ : ComplexShape.Rel c 1 0) +
        SimplicialObject.σ X 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            hσ' 0 1 2 (_ : ComplexShape.Rel c 2 1) ≫
              Finset.sum Finset.univ fun i => (-1) ^ ↑i • SimplicialObject.δ X i) =
    0
[PROOFSTEP]
erw [hσ'_eq' (zero_add 0).symm, hσ'_eq' (add_zero 1).symm, comp_id, Fin.sum_univ_two, Fin.sum_univ_succ,
  Fin.sum_univ_two]
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X 0 +
      (SimplicialObject.σ X 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            ((-1) ^ ↑0 • SimplicialObject.δ X 0 + (-1) ^ ↑1 • SimplicialObject.δ X 1) ≫
              ((-1) ^ 0 • SimplicialObject.σ X { val := 0, isLt := (_ : 0 < Nat.succ 0) }) +
        SimplicialObject.σ X 0 ≫
          HomologicalComplex.Hom.f (P 0) 1 ≫
            ((-1) ^ 1 • SimplicialObject.σ X { val := 1, isLt := (_ : 1 < Nat.succ 1) }) ≫
              ((-1) ^ ↑0 • SimplicialObject.δ X 0 +
                ((-1) ^ ↑(Fin.succ 0) • SimplicialObject.δ X (Fin.succ 0) +
                  (-1) ^ ↑(Fin.succ 1) • SimplicialObject.δ X (Fin.succ 1)))) =
    0
[PROOFSTEP]
simp only [Fin.val_zero, pow_zero, pow_one, pow_add, one_smul, neg_smul, Fin.mk_one, Fin.val_succ, Fin.val_one,
  Fin.succ_one_eq_two, P_zero, HomologicalComplex.id_f, Fin.val_two, pow_two, mul_neg, one_mul, neg_mul, neg_neg,
  id_comp, add_comp, comp_add, Fin.mk_zero, neg_comp, comp_neg, Fin.succ_zero_eq_one]
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X 0 +
      (SimplicialObject.σ X 0 ≫ SimplicialObject.δ X 0 ≫ SimplicialObject.σ X 0 +
          -SimplicialObject.σ X 0 ≫ SimplicialObject.δ X 1 ≫ SimplicialObject.σ X 0 +
        (-SimplicialObject.σ X 0 ≫ SimplicialObject.σ X 1 ≫ SimplicialObject.δ X 0 +
          (SimplicialObject.σ X 0 ≫ SimplicialObject.σ X 1 ≫ SimplicialObject.δ X 1 +
            -SimplicialObject.σ X 0 ≫ SimplicialObject.σ X 1 ≫ SimplicialObject.δ X 2))) =
    0
[PROOFSTEP]
erw [SimplicialObject.δ_comp_σ_self, SimplicialObject.δ_comp_σ_self_assoc, SimplicialObject.δ_comp_σ_succ, comp_id,
  SimplicialObject.δ_comp_σ_of_le X (show (0 : Fin 2) ≤ Fin.castSucc 0 by rw [Fin.castSucc_zero]),
  SimplicialObject.δ_comp_σ_self_assoc, SimplicialObject.δ_comp_σ_succ_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ 0 ≤ Fin.castSucc 0
[PROOFSTEP]
rw [Fin.castSucc_zero]
[GOAL]
case neg.zero.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq :
  ∀ (i : Fin (Nat.zero + 1)),
    Nat.zero + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.zero + 1) = 0
h : ¬0 + 1 ≤ 0 + q
hi : 0 = 0 + q
⊢ SimplicialObject.σ X 0 +
      (SimplicialObject.σ X 0 + -SimplicialObject.σ X 0 +
        (-SimplicialObject.σ X 0 + (SimplicialObject.σ X 0 + -SimplicialObject.σ X 0))) =
    0
[PROOFSTEP]
simp only [add_right_neg, add_zero, zero_add]
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (Nat.succ n + 1) = 0
[PROOFSTEP]
rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp, P_succ]
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
⊢ (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i) ≫
        HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) +
      (HomologicalComplex.Hom.f (Q q) (Nat.succ n) ≫ SimplicialObject.σ X i) ≫
        HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
have v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i) := (HigherFacesVanish.of_P q n).comp_σ hi
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
⊢ (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i) ≫
        HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) +
      (HomologicalComplex.Hom.f (Q q) (Nat.succ n) ≫ SimplicialObject.σ X i) ≫
        HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
erw [← assoc, v.comp_P_eq_self, HomologicalComplex.add_f_apply, Preadditive.comp_add, comp_id, v.comp_Hσ_eq hi, assoc,
  SimplicialObject.δ_comp_σ_succ_assoc, Fin.eta, decomposition_Q n q, sum_comp, sum_comp, Finset.sum_eq_zero, add_zero,
  add_neg_eq_zero]
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
⊢ ∀ (x : Fin (n + 1)),
    x ∈ Finset.filter (fun i => ↑i < q) Finset.univ →
      ((HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
              SimplicialObject.δ X (Fin.succ (↑Fin.revPerm x)) ≫ SimplicialObject.σ X (↑Fin.revPerm x)) ≫
            SimplicialObject.σ X i) ≫
          HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
        0
[PROOFSTEP]
intro j hj
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : j ∈ Finset.filter (fun i => ↑i < q) Finset.univ
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
simp only [true_and_iff, Finset.mem_univ, Finset.mem_filter] at hj 
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : Nat.succ n = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
simp only [Nat.succ_eq_add_one] at hi 
[GOAL]
case neg.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
obtain ⟨k, hk⟩ := Nat.le.dest (Nat.lt_succ_iff.mp (Fin.is_lt j))
[GOAL]
case neg.succ.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : ↑j + k = n
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
rw [add_comm] at hk 
[GOAL]
case neg.succ.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
have hi' : i = Fin.castSucc ⟨i, by linarith⟩ := by
  ext
  simp only [Fin.castSucc_mk, Fin.eta]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ ↑i < n + 1
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
⊢ ↑i = ↑(Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) })
[PROOFSTEP]
simp only [Fin.castSucc_mk, Fin.eta]
[GOAL]
case neg.succ.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
have eq :=
  hq j.revPerm.succ
    (by
      simp only [← hk, Fin.revPerm_eq j hk.symm, Nat.succ_eq_add_one, Fin.succ_mk, Fin.val_mk]
      linarith)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
⊢ Nat.succ n + 1 ≤ ↑(Fin.succ (↑Fin.revPerm j)) + q
[PROOFSTEP]
simp only [← hk, Fin.revPerm_eq j hk.symm, Nat.succ_eq_add_one, Fin.succ_mk, Fin.val_mk]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
⊢ k + ↑j + 1 + 1 ≤ k + 1 + q
[PROOFSTEP]
linarith
[GOAL]
case neg.succ.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
eq : SimplicialObject.σ X (Fin.succ (↑Fin.revPerm j)) ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
⊢ ((HomologicalComplex.Hom.f (P ↑j) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm j)) ≫ SimplicialObject.σ X (↑Fin.revPerm j)) ≫
        SimplicialObject.σ X i) ≫
      HomologicalComplex.Hom.f (P q ≫ (𝟙 (AlternatingFaceMapComplex.obj X) + Hσ q)) (Nat.succ n + 1) =
    0
[PROOFSTEP]
rw [HomologicalComplex.comp_f, assoc, assoc, assoc, hi', SimplicialObject.σ_comp_σ_assoc, reassoc_of% eq, zero_comp,
  comp_zero, comp_zero, comp_zero]
[GOAL]
case neg.succ.intro.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
eq : SimplicialObject.σ X (Fin.succ (↑Fin.revPerm j)) ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
⊢ { val := ↑i, isLt := (_ : ↑i < n + 1) } ≤ ↑Fin.revPerm j
[PROOFSTEP]
simp only [Fin.revPerm_eq j hk.symm, Fin.le_iff_val_le_val, Fin.val_mk]
[GOAL]
case neg.succ.intro.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
hq :
  ∀ (i : Fin (Nat.succ n + 1)),
    Nat.succ n + 1 ≤ ↑i + q → SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
i : Fin (Nat.succ n + 1)
h : ¬Nat.succ n + 1 ≤ ↑i + q
hi : n + 1 = ↑i + q
v : HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ SimplicialObject.σ X i)
j : Fin (n + 1)
hj : ↑j < q
k : ℕ
hk : k + ↑j = n
hi' : i = Fin.castSucc { val := ↑i, isLt := (_ : ↑i < n + 1) }
eq : SimplicialObject.σ X (Fin.succ (↑Fin.revPerm j)) ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n + 1) = 0
⊢ ↑i ≤ k
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ SimplicialObject.σ X i ≫ HomologicalComplex.Hom.f PInfty (n + 1) = 0
[PROOFSTEP]
rw [PInfty_f, σ_comp_P_eq_zero X i]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ n + 1 ≤ ↑i + (n + 1)
[PROOFSTEP]
simp only [le_add_iff_nonneg_left, zero_le]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
θ : [n] ⟶ Δ'
hθ : ¬Mono θ
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty n = 0
[PROOFSTEP]
rw [SimplexCategory.mono_iff_injective] at hθ 
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
θ : [n] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty n = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty Nat.zero = 0
[PROOFSTEP]
exfalso
[GOAL]
case zero.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ False
[PROOFSTEP]
apply hθ
[GOAL]
case zero.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
[PROOFSTEP]
intro x y h
[GOAL]
case zero.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
x y : Fin (SimplexCategory.len [Nat.zero] + 1)
h : ↑(SimplexCategory.Hom.toOrderHom θ) x = ↑(SimplexCategory.Hom.toOrderHom θ) y
⊢ x = y
[PROOFSTEP]
fin_cases x
[GOAL]
case zero.h.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
y : Fin (SimplexCategory.len [Nat.zero] + 1)
h :
  ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    ↑(SimplexCategory.Hom.toOrderHom θ) y
⊢ { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } = y
[PROOFSTEP]
fin_cases y
[GOAL]
case zero.h.head.head
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
h :
  ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) }
⊢ { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) }
[PROOFSTEP]
rfl
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : [Nat.succ n✝] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n✝) = 0
[PROOFSTEP]
obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ
[GOAL]
case succ.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : [Nat.succ n✝] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : [n✝] ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n✝) = 0
[PROOFSTEP]
rw [h, op_comp, X.map_comp, assoc, show X.map (SimplexCategory.σ i).op = X.σ i by rfl, σ_comp_PInfty, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : [Nat.succ n✝] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : [n✝] ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ X.map (SimplexCategory.σ i).op = SimplicialObject.σ X i
[PROOFSTEP]
rfl
