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 : ℕ
⊢ HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n =
    G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n)
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 : ℕ
⊢ HomologicalComplex.Hom.f (Hσ q) n = G.map (HomologicalComplex.Hom.f (Hσ q) n)
unfold Hσ
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 : ℕ
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)
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 : ℕ
⊢ HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n =
    G.map (HomologicalComplex.Hom.f (nullHomotopicMap' (hσ' q)) n)
have eq := HomologicalComplex.congr_hom (map_nullHomotopicMap' G (@hσ' _ _ _ X q)) n
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 : ℕ
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)
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 : ℕ
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)
simp only [Functor.mapHomologicalComplex_map_f, ← map_hσ'] at eq
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 : ℕ
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
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 : ℕ
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)
rw [eq]
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 : ℕ
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
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 : ℕ
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
let h := (Functor.congr_obj (map_alternatingFaceMapComplex G) X).symm
no goals
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 : ℕ
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
congr