ι : Type ?u.332610
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₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
succ' : (t : (X₀ : V) × (X₁ : V) × (X₀ ⟶ X₁)) → (X₂ : V) ×' (d : t.snd.fst ⟶ X₂) ×' t.snd.snd ≫ d = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
ι : Type ?u.332610
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₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
succ' : (t : (X₀ : V) × (X₁ : V) × (X₀ ⟶ X₁)) → (X₂ : V) ×' (d : t.snd.fst ⟶ X₂) ×' t.snd.snd ≫ d = 0
⊢ HomologicalComplex.d (mk' X₀ X₁ d₀ succ') 0 1 = d₀
change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀
no goals
ι : Type ?u.332610
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₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
succ' : (t : (X₀ : V) × (X₁ : V) × (X₀ ⟶ X₁)) → (X₂ : V) ×' (d : t.snd.fst ⟶ X₂) ×' t.snd.snd ≫ d = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
rw [if_pos rfl, Category.comp_id]