[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
