-- Mathlib/Algebra/Homology/Homotopy.lean
theorem map_nullHomotopicMap' {W : Type*} [Category W] [Preadditive W] (G : V ⥤ W) [G.Additive]
    (hom : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) :
    (G.mapHomologicalComplex c).map (nullHomotopicMap' hom) =
      nullHomotopicMap' fun i j hij => by exact G.map (hom i j hij)

Proof state:
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n i j : ι
h✝ : c.Rel j i
⊢ G.map (hom i j h✝) = (fun i j hij => G.map (hom i j hij)) i j h✝

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (G.mapHomologicalComplex c).map (nullHomotopicMap' hom) = nullHomotopicMap' fun i j hij => G.map (hom i j hij)

Tactic:
ext n

Result:
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n : ι
⊢ ((G.mapHomologicalComplex c).map (nullHomotopicMap' hom)).f n =
    (nullHomotopicMap' fun i j hij => G.map (hom i j hij)).f n

Proof state:
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.121675, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
i j : ι
hij : c.Rel j i
⊢ ((G.mapHomologicalComplex c).obj C).X i ⟶ ((G.mapHomologicalComplex c).obj D).X j

Tactic:
exact G.map (hom i j hij)

Result:
no goals

Proof state:
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n i j : ι
h✝ : ¬c.Rel j i
⊢ G.map 0 = 0

Tactic:
rw [G.map_zero]

Result:
no goals

Proof state:
case h.e_self.e_hom.h.h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n i j : ι
⊢ G.map (dite (c.Rel j i) (hom i j) fun x => 0) = dite (c.Rel j i) ((fun i j hij => G.map (hom i j hij)) i j) fun x => 0

Tactic:
split_ifs

Result:
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n i j : ι
h✝ : c.Rel j i
⊢ G.map (hom i j h✝) = (fun i j hij => G.map (hom i j hij)) i j h✝

case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n i j : ι
h✝ : ¬c.Rel j i
⊢ G.map 0 = 0

Proof state:
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n : ι
⊢ (nullHomotopicMap fun i j => G.map (dite (c.Rel j i) (hom i j) fun x => 0)).f n =
    (nullHomotopicMap' fun i j hij => G.map (hom i j hij)).f n

Tactic:
congr

Result:
case h.e_self.e_hom
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n : ι
⊢ (fun i j => G.map (dite (c.Rel j i) (hom i j) fun x => 0)) = fun i j =>
    dite (c.Rel j i) ((fun i j hij => G.map (hom i j hij)) i j) fun x => 0

Proof state:
case h.e_self.e_hom
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n : ι
⊢ (fun i j => G.map (dite (c.Rel j i) (hom i j) fun x => 0)) = fun i j =>
    dite (c.Rel j i) ((fun i j hij => G.map (hom i j hij)) i j) fun x => 0

Tactic:
ext i j

Result:
case h.e_self.e_hom.h.h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n i j : ι
⊢ G.map (dite (c.Rel j i) (hom i j) fun x => 0) = dite (c.Rel j i) ((fun i j hij => G.map (hom i j hij)) i j) fun x => 0

Proof state:
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n : ι
⊢ ((G.mapHomologicalComplex c).map (nullHomotopicMap' hom)).f n =
    (nullHomotopicMap' fun i j hij => G.map (hom i j hij)).f n

Tactic:
erw [map_nullHomotopicMap]

Result:
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
n : ι
⊢ (nullHomotopicMap fun i j => G.map (dite (c.Rel j i) (hom i j) fun x => 0)).f n =
    (nullHomotopicMap' fun i j hij => G.map (hom i j hij)).f n