C : Type u_2
inst✝¹ : Category 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
⊢ f.app [n].op ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app [m].op
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n m : ℕ
hnm : ComplexShape.Rel c m n
X Y : SimplicialObject C
f : X ⟶ Y
⊢ f.app [n].op ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app [m].op
have h : n + 1 = m := hnm
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
⊢ f.app [n].op ≫ hσ' q n (n + 1) hnm = hσ' q n (n + 1) hnm ≫ f.app [n + 1].op
C : Type u_2
inst✝¹ : Category 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
⊢ f.app [n].op ≫ hσ' q n m hnm = hσ' q n m hnm ≫ f.app [m].op
subst h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
⊢ f.app [n].op ≫ hσ q n = hσ q n ≫ f.app [n + 1].op
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
⊢ f.app [n].op ≫ hσ' q n (n + 1) hnm = hσ' q n (n + 1) hnm ≫ f.app [n + 1].op
simp only [hσ', eqToHom_refl, comp_id]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
⊢ (f.app [n].op ≫ 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) }) ≫ f.app [n + 1].op
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
⊢ f.app [n].op ≫ hσ q n = hσ q n ≫ f.app [n + 1].op
unfold hσ
case inl
C : Type u_2
inst✝¹ : Category 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
⊢ f.app [n].op ≫ 0 = 0 ≫ f.app [n + 1].op

case inr
C : Type u_2
inst✝¹ : Category 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
⊢ f.app [n].op ≫ ((-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) }) ≫ f.app [n + 1].op
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
hnm : ComplexShape.Rel c (n + 1) n
⊢ (f.app [n].op ≫ 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) }) ≫ f.app [n + 1].op
split_ifs
no goals
case inl
C : Type u_2
inst✝¹ : Category 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
⊢ f.app [n].op ≫ 0 = 0 ≫ f.app [n + 1].op
rw [zero_comp, comp_zero]
case inr
C : Type u_2
inst✝¹ : Category 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) • f.app [n].op ≫ σ Y { val := n - q, isLt := (_ : n - q < Nat.succ n) } =
    (-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) } ≫ f.app [n + 1].op
case inr
C : Type u_2
inst✝¹ : Category 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
⊢ f.app [n].op ≫ ((-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) }) ≫ f.app [n + 1].op
simp only [zsmul_comp, comp_zsmul]
case inr
C : Type u_2
inst✝¹ : Category 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) • f.app [n].op ≫ σ Y { val := n - q, isLt := (_ : n - q < Nat.succ n) } =
    (-1) ^ (n - q) • f.app [n].op ≫ Y.map (SimplexCategory.σ { val := n - q, isLt := (_ : n - q < Nat.succ n) }).op
case inr
C : Type u_2
inst✝¹ : Category 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) • f.app [n].op ≫ σ Y { val := n - q, isLt := (_ : n - q < Nat.succ n) } =
    (-1) ^ (n - q) • σ X { val := n - q, isLt := (_ : n - q < Nat.succ n) } ≫ f.app [n + 1].op
erw [f.naturality]
no goals
case inr
C : Type u_2
inst✝¹ : Category 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) • f.app [n].op ≫ σ Y { val := n - q, isLt := (_ : n - q < Nat.succ n) } =
    (-1) ^ (n - q) • f.app [n].op ≫ Y.map (SimplexCategory.σ { val := n - q, isLt := (_ : n - q < Nat.succ n) }).op
rfl