-- Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
theorem map_Hσ {D : Type*} [Category D] [Preadditive D] (G : C ⥤ D) [G.Additive]
    (X : SimplicialObject C) (q n : ℕ) :
    (Hσ q : K[((whiskering C D).obj G).obj X] ⟶ _).f n = G.map ((Hσ q : K[X] ⟶ _).f n)

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
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n
h : ((whiskering C D).obj G ⋙ alternatingFaceMapComplex D).obj X =
  (alternatingFaceMapComplex C ⋙ G.mapHomologicalComplex (ComplexShape.down ℕ)).obj X :=
  Eq.symm (Functor.congr_obj (map_alternatingFaceMapComplex G) X)
⊢ (nullHomotopicMap' (hσ' q)).f n = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n

Tactic:
congr

Result:
no goals

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
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
eq :
  ((G.mapHomologicalComplex c).map (nullHomotopicMap' (hσ' q))).f n =
    (nullHomotopicMap' fun i j hij => G.map (hσ' q i j hij)).f n
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)

Tactic:
simp only [Functor.mapHomologicalComplex_map_f, ← map_hσ'] at eq

Result:
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
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)

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
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)

Tactic:
have eq := HomologicalComplex.congr_hom (map_nullHomotopicMap' G (@hσ' _ _ _ X q)) n

Result:
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
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
eq :
  ((G.mapHomologicalComplex c).map (nullHomotopicMap' (hσ' q))).f n =
    (nullHomotopicMap' fun i j hij => G.map (hσ' q i j hij)).f n
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)

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
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n
⊢ (nullHomotopicMap' (hσ' q)).f n = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n

Tactic:
let h := (Functor.congr_obj (map_alternatingFaceMapComplex G) X).symm

Result:
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
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n
h : ((whiskering C D).obj G ⋙ alternatingFaceMapComplex D).obj X =
  (alternatingFaceMapComplex C ⋙ G.mapHomologicalComplex (ComplexShape.down ℕ)).obj X :=
  Eq.symm (Functor.congr_obj (map_alternatingFaceMapComplex G) X)
⊢ (nullHomotopicMap' (hσ' q)).f n = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n

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
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)

Tactic:
rw [eq]

Result:
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
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
eq : G.map ((nullHomotopicMap' (hσ' q)).f n) = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n
⊢ (nullHomotopicMap' (hσ' q)).f n = (nullHomotopicMap' fun i j hij => hσ' q i j hij).f n

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
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ (Hσ q).f n = G.map ((Hσ q).f n)

Tactic:
unfold Hσ

Result:
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
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n : ℕ
⊢ (nullHomotopicMap' (hσ' q)).f n = G.map ((nullHomotopicMap' (hσ' q)).f n)