C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
⊢ (if h : Δ = Δ then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ))
    else if h : Isδ₀ (𝟙 Δ) then HomologicalComplex.d K (len Δ) (len Δ) else 0) =
    𝟙 (HomologicalComplex.X K (len Δ))
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
⊢ mapMono K (𝟙 Δ) = 𝟙 (HomologicalComplex.X K (len Δ))
unfold mapMono
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
⊢ (if h : Δ = Δ then eqToHom (_ : HomologicalComplex.X K (len Δ) = HomologicalComplex.X K (len Δ))
    else if h : Isδ₀ (𝟙 Δ) then HomologicalComplex.d K (len Δ) (len Δ) else 0) =
    𝟙 (HomologicalComplex.X K (len Δ))
simp only [eq_self_iff_true, eqToHom_refl, dite_eq_ite, if_true]