case w
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : ∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom
i : ι
⊢ (isoApp (isoOfComponents f) i).hom = (f i).hom
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : ∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom
i : ι
⊢ isoApp (isoOfComponents f) i = f i
ext
no goals
case w
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : ∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom
i : ι
⊢ (isoApp (isoOfComponents f) i).hom = (f i).hom
simp