case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsSeparating (Set.op 𝒢)
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
⊢ IsSeparating (Set.op 𝒢) ↔ IsCoseparating 𝒢
refine' ⟨fun h𝒢 X Y f g hfg => _, fun h𝒢 X Y f g hfg => _⟩
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsSeparating (Set.op 𝒢)
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : G ⟶ Y.op
⊢ (h ≫ f.op).unop = (h ≫ g.op).unop
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsSeparating (Set.op 𝒢)
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
refine' Quiver.Hom.op_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.unop_inj _)
no goals
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsSeparating (Set.op 𝒢)
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : G ⟶ Y.op
⊢ (h ≫ f.op).unop = (h ≫ g.op).unop
simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ (Set.mem_op.1 hG) _
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : G ∈ 𝒢
h : X.unop ⟶ G
⊢ (f.unop ≫ h).op = (g.unop ≫ h).op
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
refine' Quiver.Hom.unop_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.op_inj _)
no goals
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : G ∈ 𝒢
h : X.unop ⟶ G
⊢ (f.unop ≫ h).op = (g.unop ≫ h).op
simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ (Set.op_mem_op.2 hG) _