C : Type u
inst✝¹ : Category C
ι : Type u_1
s : ι → C
inst✝ : HasZeroMorphisms C
o : HomOrthogonal s
i j : ι
w : i ≠ j
f : s i ⟶ s j
this : Subsingleton (s i ⟶ s j)
⊢ f = 0
C : Type u
inst✝¹ : Category C
ι : Type u_1
s : ι → C
inst✝ : HasZeroMorphisms C
o : HomOrthogonal s
i j : ι
w : i ≠ j
f : s i ⟶ s j
⊢ f = 0
haveI := o i j w
no goals
C : Type u
inst✝¹ : Category C
ι : Type u_1
s : ι → C
inst✝ : HasZeroMorphisms C
o : HomOrthogonal s
i j : ι
w : i ≠ j
f : s i ⟶ s j
this : Subsingleton (s i ⟶ s j)
⊢ f = 0
apply Subsingleton.elim