-- Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
theorem map_alternatingFaceMapComplex {D : Type*} [Category D] [Preadditive D] (F : C ⥤ D)
    [F.Additive] :
    alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex _ =
      (SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D

Proof state:
case h_map
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X Y : SimplicialObject C
f : X ⟶ Y
⊢ (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f =
    eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯

Tactic:
ext n

Result:
case h_map.h
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f).f n =
    (eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯).f n

Proof state:
case h_obj.h_X
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).X =
    (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).X

Tactic:
ext n

Result:
case h_obj.h_X.h
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
n : ℕ
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).X n =
    (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).X n

Proof state:
case h_map
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ autoParam
    (∀ (X Y : SimplicialObject C) (f : X ⟶ Y),
      (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f =
        eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯)
    _auto✝

Tactic:
intro X Y f

Result:
case h_map
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X Y : SimplicialObject C
f : X ⟶ Y
⊢ (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f =
    eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯

Proof state:
case h_obj.h_X.h
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
n : ℕ
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).X n =
    (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).X n

Tactic:
rfl

Result:
no goals