C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ 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.d K (len Δ) (len Δ')
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ mapMono K i = HomologicalComplex.d K (len Δ) (len Δ')
unfold mapMono
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ Δ ≠ Δ'
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ 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.d K (len Δ) (len Δ')
suffices Δ ≠ Δ' by
  simp only [dif_neg this, dif_pos hi]
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ'' : SimplexCategory
i : Δ ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ False
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ Δ ≠ Δ'
rintro rfl
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ'' : SimplexCategory
i : Δ ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
⊢ False
simpa only [self_eq_add_right, Nat.one_ne_zero] using hi.1
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
hi : Isδ₀ i
this : Δ ≠ Δ'
⊢ (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.d K (len Δ) (len Δ')
simp only [dif_neg this, dif_pos hi]