C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
X Y : C
f g : X ⟶ Y
H : C
h : Y ⟶ H
hG : IsCoseparator H
hfg : ∀ (h : Y ⟶ H), f ≫ h = g ≫ h
hH : H ∈ {H}
⊢ f ≫ h = g ≫ h
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
hG : IsCoseparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
H : C
hH : H ∈ {G}
h : Y ⟶ H
⊢ f ≫ h = g ≫ 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 g : X ⟶ Y
H : C
h : Y ⟶ H
hG : IsCoseparator H
hfg : ∀ (h : Y ⟶ H), f ≫ h = g ≫ h
hH : H ∈ {H}
⊢ f ≫ h = g ≫ h
exact hfg h