case refine'_1
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
⊢ f = default

case refine'_2
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
⊢ f = default
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
⊢ IsZero zero
refine' ⟨fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩⟩
no goals
case refine'_1
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
⊢ f = default

case refine'_2
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
⊢ f = default
all_goals
  ext
  dsimp [zero]
  apply Subsingleton.elim
case refine'_2.h
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ Hom.f f i✝ = Hom.f default i✝
case refine'_2
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
⊢ f = default
ext
case refine'_2.h
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ Hom.f f i✝ = 0
case refine'_2.h
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ Hom.f f i✝ = Hom.f default i✝
dsimp [zero]
no goals
case refine'_2.h
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ Hom.f f i✝ = 0
apply Subsingleton.elim