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

case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
⊢ IsCodetecting (Set.op 𝒢) ↔ IsDetecting 𝒢
refine' ⟨fun h𝒢 X Y f hf => _, fun h𝒢 X Y f hf => _⟩
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsCodetecting (Set.op 𝒢)
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : Y.op ⟶ G
⊢ ∃! h', f.op ≫ h' = h
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsCodetecting (Set.op 𝒢)
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
refine' (isIso_op_iff _).1 (h𝒢 _ fun G hG h => _)
case refine'_1.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsCodetecting (Set.op 𝒢)
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : Y.op ⟶ G
t : G.unop ⟶ X
ht : t ≫ f = h.unop
ht' : ∀ (y : G.unop ⟶ X), (fun h' => h' ≫ f = h.unop) y → y = t
⊢ ∃! h', f.op ≫ h' = h
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsCodetecting (Set.op 𝒢)
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : Y.op ⟶ G
⊢ ∃! h', f.op ≫ h' = h
obtain ⟨t, ht, ht'⟩ := hf (unop G) (Set.mem_op.1 hG) h.unop
no goals
case refine'_1.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsCodetecting (Set.op 𝒢)
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : Y.op ⟶ G
t : G.unop ⟶ X
ht : t ≫ f = h.unop
ht' : ∀ (y : G.unop ⟶ X), (fun h' => h' ≫ f = h.unop) y → y = t
⊢ ∃! h', f.op ≫ h' = h
exact
  ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : G ∈ 𝒢
h : G ⟶ X.unop
⊢ ∃! h', h' ≫ f.unop = h
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f
refine' (isIso_unop_iff _).1 (h𝒢 _ fun G hG h => _)
case refine'_2.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : G ∈ 𝒢
h : G ⟶ X.unop
t : Y ⟶ G.op
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ G.op), (fun h' => f ≫ h' = h.op) y → y = t
⊢ ∃! h', h' ≫ f.unop = h
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : G ∈ 𝒢
h : G ⟶ X.unop
⊢ ∃! h', h' ≫ f.unop = h
obtain ⟨t, ht, ht'⟩ := hf (op G) (Set.op_mem_op.2 hG) h.op
case refine'_2.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : G ∈ 𝒢
h : G ⟶ X.unop
t : Y ⟶ G.op
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ G.op), (fun h' => f ≫ h' = h.op) y → y = t
y : G ⟶ Y.unop
hy : (fun h' => h' ≫ f.unop = h) y
⊢ (fun h' => f ≫ h' = h.op) y.op
case refine'_2.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : G ∈ 𝒢
h : G ⟶ X.unop
t : Y ⟶ G.op
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ G.op), (fun h' => f ≫ h' = h.op) y → y = t
⊢ ∃! h', h' ≫ f.unop = h
refine' ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ _)⟩
no goals
case refine'_2.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : G ∈ 𝒢
h : G ⟶ X.unop
t : Y ⟶ G.op
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ G.op), (fun h' => f ≫ h' = h.op) y → y = t
y : G ⟶ Y.unop
hy : (fun h' => h' ≫ f.unop = h) y
⊢ (fun h' => f ≫ h' = h.op) y.op
exact Quiver.Hom.unop_inj (by simpa only using hy)
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : G ∈ 𝒢
h : G ⟶ X.unop
t : Y ⟶ G.op
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ G.op), (fun h' => f ≫ h' = h.op) y → y = t
y : G ⟶ Y.unop
hy : (fun h' => h' ≫ f.unop = h) y
⊢ (f ≫ y.op).unop = h.op.unop
simpa only using hy