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

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

Tactic:
erw [comp_nullHomotopicMap]

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

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

Tactic:
rfl

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

Tactic:
rw [comp_zero]

Result:
no goals

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