no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
inst✝¹ : HasPullbacks C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h : (fun P => {f | Subobject.Factors P f.snd}) P = (fun P => {f | Subobject.Factors P f.snd}) Q
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Subobject.Factors P f ↔ Subobject.Factors Q f
simpa [Set.ext_iff] using h