no goals
C : Type ?u.65766
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q n a m : ℕ
ha : n = a + q
hnm : ComplexShape.Rel c m n
⊢ X.obj [n + 1].op = HomologicalComplex.X K[X] m
congr
C : Type u_2
inst✝¹ : Category 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 [n + 1].op = X.obj [m].op) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op)
C : Type u_2
inst✝¹ : Category 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 [n + 1].op = X.obj [m].op)
simp only [hσ', hσ]
case inl
C : Type u_2
inst✝¹ : Category 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 [n + 1].op = X.obj [m].op) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op)

case inr
C : Type u_2
inst✝¹ : Category 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 [n + 1].op = X.obj [m].op) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op)
C : Type u_2
inst✝¹ : Category 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 [n + 1].op = X.obj [m].op) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op)
split_ifs
case inl.h
C : Type u_2
inst✝¹ : Category 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
case inl
C : Type u_2
inst✝¹ : Category 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 [n + 1].op = X.obj [m].op) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op)
exfalso
no goals
case inl.h
C : Type u_2
inst✝¹ : Category 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
linarith
case inr
C : Type u_2
inst✝¹ : Category 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 [n + 1].op = X.obj [m].op) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op)
case inr
C : Type u_2
inst✝¹ : Category 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 [n + 1].op = X.obj [m].op) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op)
have h' := tsub_eq_of_eq_add ha
no goals
case inr
C : Type u_2
inst✝¹ : Category 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 [n + 1].op = X.obj [m].op) =
    ((-1) ^ a • σ X { val := a, isLt := (_ : a < Nat.succ n) }) ≫ eqToHom (_ : X.obj [n + 1].op = X.obj [m].op)
congr