C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category 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 [n + 1].op = (((whiskering C D).obj G).obj X).obj [m].op) =
    G.map
      ((if n < q then 0 else (-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
        eqToHom (_ : X.obj [n + 1].op = X.obj [m].op))
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category 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)
unfold hσ' hσ
case inl
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category 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 [n + 1].op = (((whiskering C D).obj G).obj X).obj [m].op) =
    G.map (0 ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op))

case inr
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category 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 [n + 1].op = (((whiskering C D).obj G).obj X).obj [m].op) =
    G.map
      (((-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
        eqToHom (_ : X.obj [n + 1].op = X.obj [m].op))
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category 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 [n + 1].op = (((whiskering C D).obj G).obj X).obj [m].op) =
    G.map
      ((if n < q then 0 else (-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
        eqToHom (_ : X.obj [n + 1].op = X.obj [m].op))
split_ifs
no goals
case inl
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category 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 [n + 1].op = (((whiskering C D).obj G).obj X).obj [m].op) =
    G.map (0 ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op))
simp only [Functor.map_zero, zero_comp]
case inr
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category 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 [n + 1].op = (((whiskering C D).obj G).obj X).obj [m].op) =
    ((-1) ^ (n - q) • G.map (σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) })) ≫
      eqToHom (_ : G.obj (X.obj [n + 1].op) = G.obj (HomologicalComplex.X K[X] m))
case inr
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category 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 [n + 1].op = (((whiskering C D).obj G).obj X).obj [m].op) =
    G.map
      (((-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) }) ≫
        eqToHom (_ : X.obj [n + 1].op = X.obj [m].op))
simp only [eqToHom_map, Functor.map_comp, Functor.map_zsmul]
no goals
case inr
C : Type u_4
inst✝⁴ : Category C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_1
inst✝² : Category 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 [n + 1].op = (((whiskering C D).obj G).obj X).obj [m].op) =
    ((-1) ^ (n - q) • G.map (σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) })) ≫
      eqToHom (_ : G.obj (X.obj [n + 1].op) = G.obj (HomologicalComplex.X K[X] m))
rfl