case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : IsIso ((yoneda.obj G).map f)
⊢ IsIso f

case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
h : ReflectsIsomorphisms (yoneda.obj G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
⊢ IsCodetector G ↔ ReflectsIsomorphisms (yoneda.obj G)
refine' ⟨fun hG => ⟨fun f hf => _⟩, fun h => (isCodetector_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 : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : IsIso ((yoneda.obj G).map f)
⊢ ∀ (h : B✝.unop ⟶ G), ∃! h', f.unop ≫ h' = h
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : IsIso ((yoneda.obj G).map f)
⊢ IsIso f
refine' (isIso_unop_iff _).1 (hG.def _ _)
no goals
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : IsIso ((yoneda.obj G).map f)
⊢ ∀ (h : B✝.unop ⟶ G), ∃! h', f.unop ≫ h' = h
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
h : ReflectsIsomorphisms (yoneda.obj G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f.op
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
h : ReflectsIsomorphisms (yoneda.obj G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f
rw [← isIso_op_iff]
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
h : ReflectsIsomorphisms (yoneda.obj G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso ((yoneda.obj G).map f.op)
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
h : ReflectsIsomorphisms (yoneda.obj G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f.op
suffices IsIso ((yoneda.obj G).map f.op) by
  exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h
no goals
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
G : C
h : ReflectsIsomorphisms (yoneda.obj G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso ((yoneda.obj G).map f.op)
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 (yoneda.obj G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
this : IsIso ((yoneda.obj G).map f.op)
⊢ IsIso f.op
exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h