C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ (if h : Δ' = Δ then eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ))
      else if h : Isδ₀ i then HomologicalComplex.d K (len Δ') (len Δ) else 0) ≫
      HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫
      if h : Δ' = Δ then eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ))
      else if h : Isδ₀ i then HomologicalComplex.d K' (len Δ') (len Δ) else 0
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ mapMono K i ≫ HomologicalComplex.Hom.f f (len Δ) = HomologicalComplex.Hom.f f (len Δ') ≫ mapMono K' i
unfold mapMono
case inl
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : Δ' = Δ
⊢ eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ)) ≫ HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫
      eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ))

case inr.inl
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : Isδ₀ i
⊢ HomologicalComplex.d K (len Δ') (len Δ) ≫ HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫ HomologicalComplex.d K' (len Δ') (len Δ)

case inr.inr
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : ¬Isδ₀ i
⊢ 0 ≫ HomologicalComplex.Hom.f f (len Δ) = HomologicalComplex.Hom.f f (len Δ') ≫ 0
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ (if h : Δ' = Δ then eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ))
      else if h : Isδ₀ i then HomologicalComplex.d K (len Δ') (len Δ) else 0) ≫
      HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫
      if h : Δ' = Δ then eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ))
      else if h : Isδ₀ i then HomologicalComplex.d K' (len Δ') (len Δ) else 0
split_ifs with h
case inl
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ'
inst✝ : Mono i
⊢ eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ')) ≫
      HomologicalComplex.Hom.f f (len Δ') =
    HomologicalComplex.Hom.f f (len Δ') ≫
      eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ'))
case inl
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : Δ' = Δ
⊢ eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ)) ≫ HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫
      eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ))
subst h
no goals
case inl
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ'
inst✝ : Mono i
⊢ eqToHom (_ : HomologicalComplex.X K (len Δ') = HomologicalComplex.X K (len Δ')) ≫
      HomologicalComplex.Hom.f f (len Δ') =
    HomologicalComplex.Hom.f f (len Δ') ≫
      eqToHom (_ : HomologicalComplex.X K' (len Δ') = HomologicalComplex.X K' (len Δ'))
simp only [id_comp, eqToHom_refl, comp_id]
no goals
case inr.inl
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : Isδ₀ i
⊢ HomologicalComplex.d K (len Δ') (len Δ) ≫ HomologicalComplex.Hom.f f (len Δ) =
    HomologicalComplex.Hom.f f (len Δ') ≫ HomologicalComplex.d K' (len Δ') (len Δ)
rw [HomologicalComplex.Hom.comm]
no goals
case inr.inr
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
h : ¬Δ' = Δ
h✝ : ¬Isδ₀ i
⊢ 0 ≫ HomologicalComplex.Hom.f f (len Δ) = HomologicalComplex.Hom.f f (len Δ') ≫ 0
rw [zero_comp, comp_zero]