[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]


[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.725, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
j : ℕ
⊢ ¬ComplexShape.Rel c 0 j
[PROOFSTEP]
intro hj
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.725, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
j : ℕ
hj : ComplexShape.Rel c 0 j
⊢ False
[PROOFSTEP]
dsimp at hj
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.725, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
j : ℕ
hj : j + 1 = 0
⊢ False
[PROOFSTEP]
apply Nat.not_succ_le_zero j
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.725, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
j : ℕ
hj : j + 1 = 0
⊢ Nat.succ j ≤ 0
[PROOFSTEP]
rw [Nat.succ_eq_add_one, hj]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.35594, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnm : ComplexShape.Rel c m n
⊢ X.obj (op [n + 1]) = HomologicalComplex.X K[X] m
[PROOFSTEP]
congr
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : ComplexShape.Rel c m n
⊢ hσ' q n m hnm = 0
[PROOFSTEP]
simp only [hσ', hσ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : ComplexShape.Rel c m n
⊢ (if n < q then 0 else (-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
      eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m])) =
    0
[PROOFSTEP]
split_ifs
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n m : ℕ
hnq : n < q
hnm : ComplexShape.Rel c m n
⊢ 0 ≫ eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m])) = 0
[PROOFSTEP]
exact zero_comp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.71579, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : ComplexShape.Rel c m n
⊢ X.obj (op [n + 1]) = HomologicalComplex.X K[X] m
[PROOFSTEP]
congr
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : ComplexShape.Rel c m n
⊢ hσ' q n m hnm =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m]))
[PROOFSTEP]
simp only [hσ', hσ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : ComplexShape.Rel c m n
⊢ (if n < q then 0 else (-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
      eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m])) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m]))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : ComplexShape.Rel c m n
h✝ : n < q
⊢ 0 ≫ eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m])) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m]))
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : ComplexShape.Rel c m n
h✝ : n < q
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : ComplexShape.Rel c m n
h✝ : ¬n < q
⊢ ((-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
      eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m])) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m]))
[PROOFSTEP]
have h' := tsub_eq_of_eq_add ha
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : ComplexShape.Rel c m n
h✝ : ¬n < q
h' : n - q = a
⊢ ((-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
      eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m])) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m]))
[PROOFSTEP]
congr
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n a : ℕ
ha : n = a + q
⊢ hσ' q n (n + 1) (_ : n + 1 = n + 1) = (-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }
[PROOFSTEP]
rw [hσ'_eq ha rfl, eqToHom_refl, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (Hσ q) 0 = 0
[PROOFSTEP]
unfold Hσ
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) 0 = 0
[PROOFSTEP]
rw [nullHomotopicMap'_f_of_not_rel_left (c_mk 1 0 rfl) cs_down_0_not_rel_left]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' q 0 1 (_ : ComplexShape.Rel c 1 0) ≫ HomologicalComplex.d K[X] 1 0 = 0
[PROOFSTEP]
rcases q with (_ | q)
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ hσ' Nat.zero 0 1 (_ : ComplexShape.Rel c 1 0) ≫ HomologicalComplex.d K[X] 1 0 = 0
[PROOFSTEP]
rw [hσ'_eq (show 0 = 0 + 0 by rfl) (c_mk 1 0 rfl)]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ 0 = 0 + 0
[PROOFSTEP]
rfl
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ (((-1) ^ 0 • σ X { val := 0, isLt := (_ : 0 < Nat.succ 0) }) ≫ eqToHom (_ : X.obj (op [0 + 1]) = X.obj (op [1]))) ≫
      HomologicalComplex.d K[X] 1 0 =
    0
[PROOFSTEP]
simp only [pow_zero, Fin.mk_zero, one_zsmul, eqToHom_refl, Category.comp_id]
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ σ X 0 ≫ HomologicalComplex.d K[X] 1 0 = 0
[PROOFSTEP]
erw [ChainComplex.of_d]
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ σ X 0 ≫ AlternatingFaceMapComplex.objD X 0 = 0
[PROOFSTEP]
rw [AlternatingFaceMapComplex.objD, Fin.sum_univ_two, Fin.val_zero, Fin.val_one, pow_zero, pow_one, one_smul, neg_smul,
  one_smul, comp_add, comp_neg, add_neg_eq_zero]
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ σ X 0 ≫ δ X 0 = σ X 0 ≫ δ X 1
[PROOFSTEP]
erw [δ_comp_σ_self, δ_comp_σ_succ]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' (Nat.succ q) 0 1 (_ : ComplexShape.Rel c 1 0) ≫ HomologicalComplex.d K[X] 1 0 = 0
[PROOFSTEP]
rw [hσ'_eq_zero (Nat.succ_pos q) (c_mk 1 0 rfl), zero_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n m : ℕ
hnm : ComplexShape.Rel c m n
X Y : SimplicialObject C
f : X ⟶ Y
⊢ NatTrans.app f (op [n]) ≫ hσ' q n m hnm = hσ' q n m hnm ≫ NatTrans.app f (op [m])
[PROOFSTEP]
have h : n + 1 = m := hnm
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n m : ℕ
hnm : ComplexShape.Rel c m n
X Y : SimplicialObject C
f : X ⟶ Y
h : n + 1 = m
⊢ NatTrans.app f (op [n]) ≫ hσ' q n m hnm = hσ' q n m hnm ≫ NatTrans.app f (op [m])
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
⊢ NatTrans.app f (op [n]) ≫ hσ' q n (n + 1) hnm = hσ' q n (n + 1) hnm ≫ NatTrans.app f (op [n + 1])
[PROOFSTEP]
simp only [hσ', eqToHom_refl, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
⊢ NatTrans.app f (op [n]) ≫ hσ q n = hσ q n ≫ NatTrans.app f (op [n + 1])
[PROOFSTEP]
unfold hσ
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
⊢ (NatTrans.app f (op [n]) ≫
      if n < q then 0 else (-1) ^ (n - q) • σ Y { val := n - q, isLt := (_ : n - q < Nat.succ n) }) =
    (if n < q then 0 else (-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
      NatTrans.app f (op [n + 1])
[PROOFSTEP]
split_ifs
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
h✝ : n < q
⊢ NatTrans.app f (op [n]) ≫ 0 = 0 ≫ NatTrans.app f (op [n + 1])
[PROOFSTEP]
rw [zero_comp, comp_zero]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
h✝ : ¬n < q
⊢ NatTrans.app f (op [n]) ≫ ((-1) ^ (n - q) • σ Y { val := n - q, isLt := (_ : n - q < Nat.succ n) }) =
    ((-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫ NatTrans.app f (op [n + 1])
[PROOFSTEP]
simp only [zsmul_comp, comp_zsmul]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
h✝ : ¬n < q
⊢ (-1) ^ (n - q) • NatTrans.app f (op [n]) ≫ σ Y { val := n - q, isLt := (_ : n - q < Nat.succ n) } =
    (-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) } ≫ NatTrans.app f (op [n + 1])
[PROOFSTEP]
erw [f.naturality]
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
h✝ : ¬n < q
⊢ (-1) ^ (n - q) • NatTrans.app f (op [n]) ≫ σ Y { val := n - q, isLt := (_ : n - q < Nat.succ n) } =
    (-1) ^ (n - q) •
      NatTrans.app f (op [n]) ≫ Y.map (SimplexCategory.σ { val := n - q, isLt := (_ : n - q < Nat.succ n) }).op
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.259122, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ (fun X => Hσ q) x✝ = (fun X => Hσ q) x✝¹ ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
unfold Hσ
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.259122, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ (fun X => nullHomotopicMap' (hσ' q)) x✝ =
    (fun X => nullHomotopicMap' (hσ' q)) x✝¹ ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
rw [nullHomotopicMap'_comp, comp_nullHomotopicMap']
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.259122, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (nullHomotopicMap' fun i j hij => HomologicalComplex.Hom.f ((alternatingFaceMapComplex C).map f) i ≫ hσ' q i j hij) =
    nullHomotopicMap' fun i j hij => hσ' q i j hij ≫ HomologicalComplex.Hom.f ((alternatingFaceMapComplex C).map f) j
[PROOFSTEP]
congr
[GOAL]
case e_h
C : Type u_1
inst✝¹ : Category.{?u.259122, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (fun i j hij => HomologicalComplex.Hom.f ((alternatingFaceMapComplex C).map f) i ≫ hσ' q i j hij) = fun i j hij =>
    hσ' q i j hij ≫ HomologicalComplex.Hom.f ((alternatingFaceMapComplex C).map f) j
[PROOFSTEP]
ext n m hnm
[GOAL]
case e_h.h.h.h
C : Type u_1
inst✝¹ : Category.{?u.259122, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
n m : ℕ
hnm : ComplexShape.Rel (ComplexShape.down ℕ) m n
⊢ HomologicalComplex.Hom.f ((alternatingFaceMapComplex C).map f) n ≫ hσ' q n m hnm =
    hσ' q n m hnm ≫ HomologicalComplex.Hom.f ((alternatingFaceMapComplex C).map f) m
[PROOFSTEP]
simp only [alternatingFaceMapComplex_map_f, hσ'_naturality]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n m : ℕ
hnm : ComplexShape.Rel c m n
⊢ hσ' q n m hnm = G.map (hσ' q n m hnm)
[PROOFSTEP]
unfold hσ' hσ
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n m : ℕ
hnm : ComplexShape.Rel c m n
⊢ (if n < q then 0
      else (-1) ^ (n - q) • σ (((whiskering C D).obj G).obj X) { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
      eqToHom (_ : (((whiskering C D).obj G).obj X).obj (op [n + 1]) = (((whiskering C D).obj G).obj X).obj (op [m])) =
    G.map
      ((if n < q then 0 else (-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
        eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m])))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n m : ℕ
hnm : ComplexShape.Rel c m n
h✝ : n < q
⊢ 0 ≫ eqToHom (_ : (((whiskering C D).obj G).obj X).obj (op [n + 1]) = (((whiskering C D).obj G).obj X).obj (op [m])) =
    G.map (0 ≫ eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m])))
[PROOFSTEP]
simp only [Functor.map_zero, zero_comp]
[GOAL]
case neg
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n m : ℕ
hnm : ComplexShape.Rel c m n
h✝ : ¬n < q
⊢ ((-1) ^ (n - q) • σ (((whiskering C D).obj G).obj X) { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
      eqToHom (_ : (((whiskering C D).obj G).obj X).obj (op [n + 1]) = (((whiskering C D).obj G).obj X).obj (op [m])) =
    G.map
      (((-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
        eqToHom (_ : X.obj (op [n + 1]) = X.obj (op [m])))
[PROOFSTEP]
simp only [eqToHom_map, Functor.map_comp, Functor.map_zsmul]
[GOAL]
case neg
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n m : ℕ
hnm : ComplexShape.Rel c m n
h✝ : ¬n < q
⊢ ((-1) ^ (n - q) • σ (((whiskering C D).obj G).obj X) { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
      eqToHom (_ : (((whiskering C D).obj G).obj X).obj (op [n + 1]) = (((whiskering C D).obj G).obj X).obj (op [m])) =
    ((-1) ^ (n - q) • G.map (σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) })) ≫
      eqToHom (_ : G.obj (X.obj (op [n + 1])) = G.obj (HomologicalComplex.X K[X] m))
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
⊢ HomologicalComplex.Hom.f (Hσ q) n = G.map (HomologicalComplex.Hom.f (Hσ q) n)
[PROOFSTEP]
unfold Hσ
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
⊢ HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n =
    G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n)
[PROOFSTEP]
have eq := HomologicalComplex.congr_hom (map_nullHomotopicMap' G (@hσ' _ _ _ X q)) n
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
eq :
  HomologicalComplex.Hom.f ((Functor.mapHomologicalComplex G c).map (nullHomotopicMap' (hσ' q))) n =
    HomologicalComplex.Hom.f (nullHomotopicMap' fun i j hij => G.map (hσ' q i j hij)) n
⊢ HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n =
    G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n)
[PROOFSTEP]
simp only [Functor.mapHomologicalComplex_map_f, ← map_hσ'] at eq
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
eq :
  G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n) =
    HomologicalComplex.Hom.f (nullHomotopicMap' fun i j hij => hσ' q i j hij) n
⊢ HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n =
    G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n)
[PROOFSTEP]
rw [eq]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
eq :
  G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n) =
    HomologicalComplex.Hom.f (nullHomotopicMap' fun i j hij => hσ' q i j hij) n
⊢ HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n =
    HomologicalComplex.Hom.f (nullHomotopicMap' fun i j hij => hσ' q i j hij) n
[PROOFSTEP]
let h := (Functor.congr_obj (map_alternatingFaceMapComplex G) X).symm
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
eq :
  G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n) =
    HomologicalComplex.Hom.f (nullHomotopicMap' fun i j hij => hσ' q i j hij) n
h : ((whiskering C D).obj G ⋙ alternatingFaceMapComplex D).obj X =
  (alternatingFaceMapComplex C ⋙ Functor.mapHomologicalComplex G (ComplexShape.down ℕ)).obj X :=
  Eq.symm (Functor.congr_obj (map_alternatingFaceMapComplex G) X)
⊢ HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n =
    HomologicalComplex.Hom.f (nullHomotopicMap' fun i j hij => hσ' q i j hij) n
[PROOFSTEP]
congr


[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ ∀ (i j : ℕ),
    ComplexShape.Rel (ComplexShape.down ℕ) i j →
      ((fun n => Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (Γ₀.splitting K)) n)) i).hom ≫
          HomologicalComplex.d K i j =
        HomologicalComplex.d (Splitting.nondegComplex (Γ₀.splitting K)) i j ≫
          ((fun n => Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (Γ₀.splitting K)) n)) j).hom
[PROOFSTEP]
rintro _ n (rfl : n + 1 = _)
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((fun n => Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (Γ₀.splitting K)) n)) (n + 1)).hom ≫
      HomologicalComplex.d K (n + 1) n =
    HomologicalComplex.d (Splitting.nondegComplex (Γ₀.splitting K)) (n + 1) n ≫
      ((fun n => Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (Γ₀.splitting K)) n)) n).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ 𝟙 (Splitting.N (Γ₀.splitting K) (n + 1)) ≫ HomologicalComplex.d K (n + 1) n =
    (Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
        HomologicalComplex.d (AlternatingFaceMapComplex.obj (Γ₀.obj K)) (n + 1) n ≫
          Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))) ≫
      𝟙 (Splitting.N (Γ₀.splitting K) n)
[PROOFSTEP]
simp only [id_comp, comp_id, AlternatingFaceMapComplex.obj_d_eq, Preadditive.sum_comp, Preadditive.comp_sum]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.d K (n + 1) n =
    Finset.sum Finset.univ fun j =>
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
        ((-1) ^ ↑j • δ (Γ₀.obj K) j) ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
rw [Fintype.sum_eq_single (0 : Fin (n + 2))]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.d K (n + 1) n =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      ((-1) ^ ↑0 • δ (Γ₀.obj K) 0) ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
simp only [Fin.val_zero, pow_zero, one_zsmul]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.d K (n + 1) n =
    Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      δ (Γ₀.obj K) 0 ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
erw [Γ₀.Obj.mapMono_on_summand_id_assoc, Γ₀.Obj.Termwise.mapMono_δ₀, Splitting.ι_πSummand_eq_id, comp_id]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ∀ (x : Fin (n + 2)),
    x ≠ 0 →
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
          ((-1) ^ ↑x • δ (Γ₀.obj K) x) ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) =
        0
[PROOFSTEP]
intro i hi
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      ((-1) ^ ↑i • δ (Γ₀.obj K) i) ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) =
    0
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
      ((-1) ^ ↑i • δ (Γ₀.obj K) i) ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) =
    0
[PROOFSTEP]
simp only [Preadditive.zsmul_comp, Preadditive.comp_zsmul, assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ (-1) ^ ↑i •
      Splitting.ιSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n + 1])) ≫
        δ (Γ₀.obj K) i ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op [n])) =
    0
[PROOFSTEP]
erw [Γ₀.Obj.mapMono_on_summand_id_assoc, Γ₀.Obj.Termwise.mapMono_eq_zero, zero_comp, zsmul_zero]
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ [n + 1] ≠ [n]
[PROOFSTEP]
intro h
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : [n + 1] = [n]
⊢ False
[PROOFSTEP]
replace h := congr_arg SimplexCategory.len h
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : SimplexCategory.len [n + 1] = SimplexCategory.len [n]
⊢ False
[PROOFSTEP]
change n + 1 = n at h
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : n + 1 = n
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case h₂
C : Type u_1
inst✝² : Category.{?u.42, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ i)
[PROOFSTEP]
simpa only [Isδ₀.iff] using hi
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ N₁Γ₀.app K =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).symm ≪≫
      (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)
[PROOFSTEP]
ext1
[GOAL]
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).hom =
    ((Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).hom
[PROOFSTEP]
dsimp [N₁Γ₀]
[GOAL]
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (((Karoubi.Hom.mk PInfty ≫ NatTrans.app Split.toKaroubiNondegComplexFunctorIsoN₁.inv (Split.mk' (Γ₀.splitting K))) ≫
          Karoubi.Hom.mk (𝟙 (Splitting.nondegComplex (Γ₀.splitting K)))) ≫
        (toKaroubi (ChainComplex C ℕ)).map (NatTrans.app Γ₀'CompNondegComplexFunctor.hom K)) ≫
      Karoubi.Hom.mk (𝟙 K) =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
[PROOFSTEP]
erw [id_comp, comp_id, comp_id]
[GOAL]
case w
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app Split.toKaroubiNondegComplexFunctorIsoN₁.inv (Split.mk' (Γ₀.splitting K)) ≫
      (toKaroubi (ChainComplex C ℕ)).map (NatTrans.app Γ₀'CompNondegComplexFunctor.hom K) =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app N₁Γ₀.hom K =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
[PROOFSTEP]
change (N₁Γ₀.app K).hom = _
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).hom =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
[PROOFSTEP]
simp only [N₁Γ₀_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ ((Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).hom =
    (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
      (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app N₁Γ₀.inv K =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫
      (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).hom
[PROOFSTEP]
change (N₁Γ₀.app K).inv = _
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ (N₁Γ₀.app K).inv =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫
      (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).hom
[PROOFSTEP]
simp only [N₁Γ₀_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ ((Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).symm ≪≫
        (toKaroubi (ChainComplex C ℕ)).mapIso (Γ₀NondegComplexIso K)).inv =
    (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫
      (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.Hom.f (NatTrans.app N₁Γ₀.hom K).f n =
    HomologicalComplex.Hom.f (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv.f n
[PROOFSTEP]
rw [N₁Γ₀_hom_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.Hom.f
      ((Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv ≫
          (toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).hom).f
      n =
    HomologicalComplex.Hom.f (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).inv.f n
[PROOFSTEP]
apply comp_id
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.Hom.f (NatTrans.app N₁Γ₀.inv K).f n =
    HomologicalComplex.Hom.f (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).hom.f n
[PROOFSTEP]
rw [N₁Γ₀_inv_app]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ HomologicalComplex.Hom.f
      ((toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫
          (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).hom).f
      n =
    HomologicalComplex.Hom.f (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)).hom.f n
[PROOFSTEP]
apply id_comp
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ = Γ₀ ⋙ N₁
[PROOFSTEP]
have h := Functor.congr_obj (functorExtension₂_comp_whiskeringLeft_toKaroubi (ChainComplex C ℕ) (SimplicialObject C)) Γ₀
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
h :
  (functorExtension₂ (ChainComplex C ℕ) (SimplicialObject C) ⋙
          (whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (SimplicialObject C))).obj
            (toKaroubi (ChainComplex C ℕ))).obj
      Γ₀ =
    ((whiskeringRight (ChainComplex C ℕ) (SimplicialObject C) (Karoubi (SimplicialObject C))).obj
          (toKaroubi (SimplicialObject C))).obj
      Γ₀
⊢ toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ = Γ₀ ⋙ N₁
[PROOFSTEP]
have h' :=
  Functor.congr_obj (functorExtension₁_comp_whiskeringLeft_toKaroubi (SimplicialObject C) (ChainComplex C ℕ)) N₁
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
h :
  (functorExtension₂ (ChainComplex C ℕ) (SimplicialObject C) ⋙
          (whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (SimplicialObject C))).obj
            (toKaroubi (ChainComplex C ℕ))).obj
      Γ₀ =
    ((whiskeringRight (ChainComplex C ℕ) (SimplicialObject C) (Karoubi (SimplicialObject C))).obj
          (toKaroubi (SimplicialObject C))).obj
      Γ₀
h' :
  (functorExtension₁ (SimplicialObject C) (ChainComplex C ℕ) ⋙
          (whiskeringLeft (SimplicialObject C) (Karoubi (SimplicialObject C)) (Karoubi (ChainComplex C ℕ))).obj
            (toKaroubi (SimplicialObject C))).obj
      N₁ =
    (𝟭 (SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ))).obj N₁
⊢ toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ = Γ₀ ⋙ N₁
[PROOFSTEP]
dsimp [N₂, Γ₂, functorExtension₁] at h h' ⊢
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
h :
  toKaroubi (ChainComplex C ℕ) ⋙ (functorExtension₂ (ChainComplex C ℕ) (SimplicialObject C)).obj Γ₀ =
    Γ₀ ⋙ toKaroubi (SimplicialObject C)
h' : toKaroubi (SimplicialObject C) ⋙ FunctorExtension₁.obj N₁ = N₁
⊢ toKaroubi (ChainComplex C ℕ) ⋙
      (functorExtension₂ (ChainComplex C ℕ) (SimplicialObject C)).obj Γ₀ ⋙ FunctorExtension₁.obj N₁ =
    Γ₀ ⋙ N₁
[PROOFSTEP]
rw [← Functor.assoc, h, Functor.assoc, h']
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : Karoubi (ChainComplex C ℕ)
n : ℕ
⊢ HomologicalComplex.Hom.f (NatTrans.app N₂Γ₂.inv X).f n =
    HomologicalComplex.Hom.f X.p n ≫ Splitting.ιSummand (Γ₀.splitting X.X) (Splitting.IndexSet.id (op [n]))
[PROOFSTEP]
simp only [N₂Γ₂, Functor.preimageIso, Iso.trans, whiskeringLeft_obj_preimage_app, N₂Γ₂ToKaroubiIso_inv, assoc,
  Functor.id_map, NatTrans.comp_app, eqToHom_app, Karoubi.comp_f, Karoubi.eqToHom_f, Karoubi.decompId_p_f,
  HomologicalComplex.comp_f, N₁Γ₀_inv_app_f_f, Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, Functor.comp_map,
  Functor.comp_obj, Karoubi.decompId_i_f, eqToHom_refl, comp_id, N₂_map_f_f, Γ₂_map_f_app, N₁_obj_p,
  PInfty_on_Γ₀_splitting_summand_eq_self_assoc, toKaroubi_obj_X, Splitting.ι_desc, Splitting.IndexSet.id_fst,
  SimplexCategory.len_mk, unop_op, Karoubi.HomologicalComplex.p_idem_assoc]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ whiskerLeft (toKaroubi (ChainComplex C ℕ)) N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
[PROOFSTEP]
let e : _ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 _ := N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
e : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex C ℕ)) :=
  N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
⊢ whiskerLeft (toKaroubi (ChainComplex C ℕ)) N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
[PROOFSTEP]
have h := ((whiskeringLeft _ _ (Karoubi (ChainComplex C ℕ))).obj (toKaroubi (ChainComplex C ℕ))).image_preimage e.hom
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
e : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex C ℕ)) :=
  N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
h :
  ((whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (ChainComplex C ℕ))).obj
          (toKaroubi (ChainComplex C ℕ))).map
      (((whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (ChainComplex C ℕ))).obj
            (toKaroubi (ChainComplex C ℕ))).preimage
        e.hom) =
    e.hom
⊢ whiskerLeft (toKaroubi (ChainComplex C ℕ)) N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
[PROOFSTEP]
dsimp only [whiskeringLeft, N₂Γ₂, Functor.preimageIso] at h ⊢
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
e : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex C ℕ)) :=
  N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀
h :
  whiskerLeft (toKaroubi (ChainComplex C ℕ))
      ((CategoryTheory.Functor.mk
            { obj := fun G => toKaroubi (ChainComplex C ℕ) ⋙ G,
              map := fun {X Y} α => whiskerLeft (toKaroubi (ChainComplex C ℕ)) α }).preimage
        (N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀).hom) =
    (N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀).hom
⊢ whiskerLeft (toKaroubi (ChainComplex C ℕ))
      ((CategoryTheory.Functor.mk
            { obj := fun G => toKaroubi (ChainComplex C ℕ) ⋙ G,
              map := fun {X Y} α => whiskerLeft (toKaroubi (ChainComplex C ℕ)) α }).preimage
        (N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀).hom) =
    N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
[PROOFSTEP]
exact h