-- 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_obj
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 =
    ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X

Tactic:
apply HomologicalComplex.ext

Result:
case h_obj.h_d
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
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).d i j

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

Proof state:
case h_obj.h_d
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
j : ℕ
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).d (j + 1) j ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).d (j + 1) j

Tactic:
dsimp only [Functor.comp_obj]

Result:
case h_obj.h_d
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
j : ℕ
⊢ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((alternatingFaceMapComplex C).obj X)).d (j + 1) j ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ ((alternatingFaceMapComplex D).obj (((SimplicialObject.whiskering C D).obj F).obj X)).d (j + 1) j

Proof state:
case h_obj.h_d
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
j : ℕ
⊢ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj ((alternatingFaceMapComplex C).obj X)).d (j + 1) j ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ ((alternatingFaceMapComplex D).obj (((SimplicialObject.whiskering C D).obj F).obj X)).d (j + 1) j

Tactic:
simp only [Functor.mapHomologicalComplex_obj_d, alternatingFaceMapComplex_obj_d,
  eqToHom_refl, id_comp, comp_id, AlternatingFaceMapComplex.objD, Functor.map_sum,
  Functor.map_zsmul]

Result:
case h_obj.h_d
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
j : ℕ
⊢ ∑ x : Fin (j + 2), (-1) ^ ↑x • F.map (X.δ x) =
    ∑ i : Fin (j + 2), (-1) ^ ↑i • (((SimplicialObject.whiskering C D).obj F).obj X).δ i

Proof state:
case h_obj.h_d
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
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).d i j

Tactic:
rintro i j (rfl : j + 1 = i)

Result:
case h_obj.h_d
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
j : ℕ
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).d (j + 1) j ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).d (j + 1) j

Proof state:
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

Tactic:
simp only [Functor.comp_map, HomologicalComplex.comp_f, alternatingFaceMapComplex_map_f,
  Functor.mapHomologicalComplex_map_f, HomologicalComplex.eqToHom_f, eqToHom_refl, comp_id,
  id_comp, SimplicialObject.whiskering_obj_map_app]

Result:
no goals

Proof state:
case h_obj.h_d
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
j : ℕ
⊢ ∑ x : Fin (j + 2), (-1) ^ ↑x • F.map (X.δ x) =
    ∑ i : Fin (j + 2), (-1) ^ ↑i • (((SimplicialObject.whiskering C D).obj F).obj X).δ i

Tactic:
rfl

Result:
no goals

Proof state:
case h_obj
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 =
      ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X

Tactic:
intro X

Result:
case h_obj
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 =
    ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X

Proof state:
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
⊢ alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ) =
    (SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D

Tactic:
apply CategoryTheory.Functor.ext

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
⊢ 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✝

case h_obj
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 =
      ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X