case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso ((coyoneda.obj G.op).map f)
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h

case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
h : ReflectsIsomorphisms (coyoneda.obj G.op)
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
⊢ IsDetector G ↔ ReflectsIsomorphisms (coyoneda.obj G.op)
refine'
  ⟨fun hG => ⟨fun f hf => hG.def _ fun h => _⟩, fun h =>
    (isDetector_def _).2 fun X Y f hf => _⟩
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : ∀ (b : (coyoneda.obj G.op).obj B✝), ∃! a, (coyoneda.obj G.op).map f a = b
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso ((coyoneda.obj G.op).map f)
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h
rw [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
no goals
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : ∀ (b : (coyoneda.obj G.op).obj B✝), ∃! a, (coyoneda.obj G.op).map f a = b
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h
exact hf h
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
h : ReflectsIsomorphisms (coyoneda.obj G.op)
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso ((coyoneda.obj G.op).map f)
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
h : ReflectsIsomorphisms (coyoneda.obj G.op)
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
suffices IsIso ((coyoneda.obj (op G)).map f) by
  exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h
no goals
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
h : ReflectsIsomorphisms (coyoneda.obj G.op)
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso ((coyoneda.obj G.op).map f)
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
h : ReflectsIsomorphisms (coyoneda.obj G.op)
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
this : IsIso ((coyoneda.obj G.op).map f)
⊢ IsIso f
exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h