ι : Type ?u.184152
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
⊢ (if 2 = 1 + 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁
ι : Type ?u.184152
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
⊢ HomologicalComplex.d (mk X₀ X₁ X₂ d₀ d₁ s succ) 2 1 = d₁
change ite (2 = 1 + 1) (𝟙 X₂ ≫ d₁) 0 = d₁
no goals
ι : Type ?u.184152
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
⊢ (if 2 = 1 + 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁
rw [if_pos rfl, Category.id_comp]