C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
X Y : C
f : X ⟶ Y
H : C
h : X ⟶ H
hG : IsCodetector H
hf : ∀ (h : X ⟶ H), ∃! h', f ≫ h' = h
hH : H ∈ {H}
⊢ ∃! h', f ≫ h' = h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
hG : IsCodetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
H : C
hH : H ∈ {G}
h : X ⟶ H
⊢ ∃! h', f ≫ h' = h
obtain rfl := Set.mem_singleton_iff.1 hH
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
X Y : C
f : X ⟶ Y
H : C
h : X ⟶ H
hG : IsCodetector H
hf : ∀ (h : X ⟶ H), ∃! h', f ≫ h' = h
hH : H ∈ {H}
⊢ ∃! h', f ≫ h' = h
exact hf h