-- Mathlib/Algebra/Homology/Homotopy.lean
theorem nullHomotopicMap'_comp (hom : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) (g : D ⟶ E) :
    nullHomotopicMap' hom ≫ g = nullHomotopicMap' fun i j hij => hom i j hij ≫ g.f j

Proof state:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n : ι
⊢ (nullHomotopicMap fun i j => (dite (c.Rel j i) (hom i j) fun x => 0) ≫ g.f j).f n =
    (nullHomotopicMap' fun i j hij => hom i j hij ≫ g.f j).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 E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n : ι
⊢ (fun i j => (dite (c.Rel j i) (hom i j) fun x => 0) ≫ g.f j) = fun i j =>
    dite (c.Rel j i) ((fun i j hij => hom i j hij ≫ g.f j) 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 E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n : ι
⊢ (fun i j => (dite (c.Rel j i) (hom i j) fun x => 0) ≫ g.f j) = fun i j =>
    dite (c.Rel j i) ((fun i j hij => hom i j hij ≫ g.f j) 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 E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n i j : ι
⊢ (dite (c.Rel j i) (hom i j) fun x => 0) ≫ g.f j =
    dite (c.Rel j i) ((fun i j hij => hom i j hij ≫ g.f j) i j) fun x => 0

Proof state:
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n i j : ι
h✝ : ¬c.Rel j i
⊢ 0 ≫ g.f j = 0

Tactic:
rw [zero_comp]

Result:
no goals

Proof state:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n : ι
⊢ (nullHomotopicMap' hom ≫ g).f n = (nullHomotopicMap' fun i j hij => hom i j hij ≫ g.f j).f n

Tactic:
erw [nullHomotopicMap_comp]

Result:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n : ι
⊢ (nullHomotopicMap fun i j => (dite (c.Rel j i) (hom i j) fun x => 0) ≫ g.f j).f n =
    (nullHomotopicMap' fun i j hij => hom i j hij ≫ g.f j).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
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
⊢ nullHomotopicMap' hom ≫ g = nullHomotopicMap' fun i j hij => hom i j hij ≫ g.f j

Tactic:
ext n

Result:
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n : ι
⊢ (nullHomotopicMap' hom ≫ g).f n = (nullHomotopicMap' fun i j hij => hom i j hij ≫ g.f j).f n

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 E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n i j : ι
⊢ (dite (c.Rel j i) (hom i j) fun x => 0) ≫ g.f j =
    dite (c.Rel j i) ((fun i j hij => hom i j hij ≫ g.f j) 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 E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n i j : ι
h✝ : c.Rel j i
⊢ hom i j h✝ ≫ g.f j = (fun i j hij => hom i j hij ≫ g.f j) i j h✝

case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n i j : ι
h✝ : ¬c.Rel j i
⊢ 0 ≫ g.f j = 0

Proof state:
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
n i j : ι
h✝ : c.Rel j i
⊢ hom i j h✝ ≫ g.f j = (fun i j hij => hom i j hij ≫ g.f j) i j h✝

Tactic:
rfl

Result:
no goals