[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
⊢ HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
induction' q with q hq
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.Hom.f (Q Nat.zero) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.zero) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
simp only [Nat.zero_eq, Q_zero, HomologicalComplex.zero_f_apply, Nat.not_lt_zero, Finset.filter_False, Finset.sum_empty]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
by_cases hqn : q + 1 ≤ n + 1
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : ¬q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
swap
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : ¬q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
rw [Q_is_eventually_constant (show n + 1 ≤ q by linarith), hq]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : ¬q + 1 ≤ n + 1
⊢ n + 1 ≤ q
[PROOFSTEP]
linarith
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : ¬q + 1 ≤ n + 1
⊢ ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
congr 1
[GOAL]
case neg.e_s
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : ¬q + 1 ≤ n + 1
⊢ Finset.filter (fun i => ↑i < q) Finset.univ = Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case neg.e_s.a.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
⊢ { val := x, isLt := hx } ∈ Finset.filter (fun i => ↑i < q) Finset.univ ↔
    { val := x, isLt := hx } ∈ Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, Finset.mem_filter, Finset.mem_univ, true_and]
[GOAL]
case neg.e_s.a.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
⊢ x < q ↔ x < q + 1
[PROOFSTEP]
constructor
[GOAL]
case neg.e_s.a.mk.mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
⊢ x < q → x < q + 1
[PROOFSTEP]
intro
[GOAL]
case neg.e_s.a.mk.mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
⊢ x < q + 1 → x < q
[PROOFSTEP]
intro
[GOAL]
case neg.e_s.a.mk.mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
a✝ : x < q
⊢ x < q + 1
[PROOFSTEP]
linarith
[GOAL]
case neg.e_s.a.mk.mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : ¬q + 1 ≤ n + 1
x : ℕ
hx : x < n + 1
a✝ : x < q + 1
⊢ x < q
[PROOFSTEP]
linarith
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
cases' Nat.le.dest (Nat.succ_le_succ_iff.mp hqn) with a ha
[GOAL]
case pos.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ HomologicalComplex.Hom.f (Q (Nat.succ q)) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
rw [Q_succ, HomologicalComplex.sub_f_apply, HomologicalComplex.comp_f, hq]
[GOAL]
case pos.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i) -
      HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
symm
[GOAL]
case pos.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i) -
      HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)
[PROOFSTEP]
conv_rhs => rw [sub_eq_add_neg, add_comm]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
| ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i) -
    HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)
[PROOFSTEP]
rw [sub_eq_add_neg, add_comm]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
| ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i) -
    HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)
[PROOFSTEP]
rw [sub_eq_add_neg, add_comm]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
| ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i) -
    HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)
[PROOFSTEP]
rw [sub_eq_add_neg, add_comm]
[GOAL]
case pos.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
⊢ ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i) =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) +
      ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
let q' : Fin (n + 1) := ⟨q, Nat.succ_le_iff.mp hqn⟩
[GOAL]
case pos.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ ∑ i in Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i) =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) +
      ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
rw [← @Finset.add_sum_erase _ _ _ _ _ _ q' (by simp)]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ q' ∈ Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ
[PROOFSTEP]
simp
[GOAL]
case pos.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ HomologicalComplex.Hom.f (P ↑q') (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm q')) ≫ SimplicialObject.σ X (↑Fin.revPerm q') +
      ∑ x in Finset.erase (Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ) q',
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm x)) ≫ SimplicialObject.σ X (↑Fin.revPerm x) =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) +
      ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
congr
[GOAL]
case pos.intro.e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ HomologicalComplex.Hom.f (P ↑q') (n + 1) ≫
      SimplicialObject.δ X (Fin.succ (↑Fin.revPerm q')) ≫ SimplicialObject.σ X (↑Fin.revPerm q') =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)
[PROOFSTEP]
have hnaq' : n = a + q := by linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ n = a + q
[PROOFSTEP]
linarith
[GOAL]
case pos.intro.e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
hnaq' : n = a + q
⊢ HomologicalComplex.Hom.f (P ↑q') (n + 1) ≫
      SimplicialObject.δ X (Fin.succ (↑Fin.revPerm q')) ≫ SimplicialObject.σ X (↑Fin.revPerm q') =
    -HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)
[PROOFSTEP]
simp only [Fin.val_mk, (HigherFacesVanish.of_P q n).comp_Hσ_eq hnaq', q'.revPerm_eq hnaq', neg_neg]
[GOAL]
case pos.intro.e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
hnaq' : n = a + q
⊢ HomologicalComplex.Hom.f (P q) (n + 1) ≫
      SimplicialObject.δ X (Fin.succ { val := a, isLt := (_ : a < Nat.succ n) }) ≫
        SimplicialObject.σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    HomologicalComplex.Hom.f (P q) (n + 1) ≫
      SimplicialObject.δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } ≫
        SimplicialObject.σ X { val := a, isLt := (_ : a < Nat.succ n) }
[PROOFSTEP]
rfl
[GOAL]
case pos.intro.e_a.e_s
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
⊢ Finset.erase (Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ) q' = Finset.filter (fun i => ↑i < q) Finset.univ
[PROOFSTEP]
ext ⟨i, hi⟩
[GOAL]
case pos.intro.e_a.e_s.a.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
i : ℕ
hi : i < n + 1
⊢ { val := i, isLt := hi } ∈ Finset.erase (Finset.filter (fun i => ↑i < Nat.succ q) Finset.univ) q' ↔
    { val := i, isLt := hi } ∈ Finset.filter (fun i => ↑i < q) Finset.univ
[PROOFSTEP]
simp only [Nat.succ_eq_add_one, Nat.lt_succ_iff_lt_or_eq, Finset.mem_univ, forall_true_left, Finset.mem_filter,
  lt_self_iff_false, or_true, and_self, not_true, Finset.mem_erase, ne_eq, Fin.mk.injEq, true_and]
[GOAL]
case pos.intro.e_a.e_s.a.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n q : ℕ
hq :
  HomologicalComplex.Hom.f (Q q) (n + 1) =
    ∑ i in Finset.filter (fun i => ↑i < q) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
hqn : q + 1 ≤ n + 1
a : ℕ
ha : q + a = n
q' : Fin (n + 1) := { val := q, isLt := (_ : q < n + 1) }
i : ℕ
hi : i < n + 1
⊢ ¬i = q ∧ (i < q ∨ i = q) ↔ i < q
[PROOFSTEP]
aesop
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ φ (id X n) = 𝟙 (X.obj (op [n + 1]))
[PROOFSTEP]
simp only [← P_add_Q_f (n + 1) (n + 1), φ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ (id X n).a +
      ∑ x : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm x)) ≫ b (id X n) (↑Fin.revPerm x) =
    HomologicalComplex.Hom.f (P (n + 1)) (n + 1) + HomologicalComplex.Hom.f (Q (n + 1)) (n + 1)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ (id X n).a = HomologicalComplex.Hom.f (P (n + 1)) (n + 1)
[PROOFSTEP]
simp only [id, PInfty_f, P_f_idem]
[GOAL]
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ ∑ x : Fin (n + 1),
      HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm x)) ≫ b (id X n) (↑Fin.revPerm x) =
    HomologicalComplex.Hom.f (Q (n + 1)) (n + 1)
[PROOFSTEP]
exact Eq.trans (by congr; simp) (decomposition_Q n (n + 1)).symm
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ ∑ x : Fin (n + 1),
      HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm x)) ≫ b (id X n) (↑Fin.revPerm x) =
    ∑ i in Finset.filter (fun i => ↑i < n + 1) Finset.univ,
      HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
        SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ SimplicialObject.σ X (↑Fin.revPerm i)
[PROOFSTEP]
congr
[GOAL]
case e_s
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ Finset.univ = Finset.filter (fun i => ↑i < n + 1) Finset.univ
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ φ (postComp f h) = φ f ≫ h
[PROOFSTEP]
unfold φ postComp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ { a := f.a ≫ h, b := fun i => b f i ≫ h }.a +
      ∑ i : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫
            b { a := f.a ≫ h, b := fun i => b f i ≫ h } (↑Fin.revPerm i) =
    (HomologicalComplex.Hom.f PInfty (n + 1) ≫ f.a +
        ∑ i : Fin (n + 1),
          HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
            SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ b f (↑Fin.revPerm i)) ≫
      h
[PROOFSTEP]
simp only [add_comp, sum_comp, assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ φ (preComp f g) = NatTrans.app g (op [n + 1]) ≫ φ f
[PROOFSTEP]
unfold φ preComp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫
        { a := NatTrans.app g (op [n + 1]) ≫ f.a, b := fun i => NatTrans.app g (op [n]) ≫ b f i }.a +
      ∑ i : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
          SimplicialObject.δ X' (Fin.succ (↑Fin.revPerm i)) ≫
            b { a := NatTrans.app g (op [n + 1]) ≫ f.a, b := fun i => NatTrans.app g (op [n]) ≫ b f i }
              (↑Fin.revPerm i) =
    NatTrans.app g (op [n + 1]) ≫
      (HomologicalComplex.Hom.f PInfty (n + 1) ≫ f.a +
        ∑ i : Fin (n + 1),
          HomologicalComplex.Hom.f (P ↑i) (n + 1) ≫
            SimplicialObject.δ X (Fin.succ (↑Fin.revPerm i)) ≫ b f (↑Fin.revPerm i))
[PROOFSTEP]
simp only [PInfty_f, comp_add]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ NatTrans.app g (op [n + 1]) ≫ f.a +
      ∑ x : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
          SimplicialObject.δ X' (Fin.succ (↑Fin.revPerm x)) ≫ NatTrans.app g (op [n]) ≫ b f (↑Fin.revPerm x) =
    NatTrans.app g (op [n + 1]) ≫ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ f.a +
      NatTrans.app g (op [n + 1]) ≫
        ∑ x : Fin (n + 1),
          HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
            SimplicialObject.δ X (Fin.succ (↑Fin.revPerm x)) ≫ b f (↑Fin.revPerm x)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ NatTrans.app g (op [n + 1]) ≫ f.a =
    NatTrans.app g (op [n + 1]) ≫ HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ f.a
[PROOFSTEP]
simp only [P_f_naturality_assoc]
[GOAL]
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X X' : SimplicialObject C
n : ℕ
Z Z' : C
f : MorphComponents X n Z
g : X' ⟶ X
h : Z ⟶ Z'
⊢ ∑ x : Fin (n + 1),
      HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
        SimplicialObject.δ X' (Fin.succ (↑Fin.revPerm x)) ≫ NatTrans.app g (op [n]) ≫ b f (↑Fin.revPerm x) =
    NatTrans.app g (op [n + 1]) ≫
      ∑ x : Fin (n + 1),
        HomologicalComplex.Hom.f (P ↑x) (n + 1) ≫
          SimplicialObject.δ X (Fin.succ (↑Fin.revPerm x)) ≫ b f (↑Fin.revPerm x)
[PROOFSTEP]
simp only [comp_sum, P_f_naturality_assoc, SimplicialObject.δ_naturality_assoc]
