-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isDetecting_op_iff (𝒢 : Set C) : IsDetecting 𝒢.op ↔ IsCodetecting 𝒢

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢.op
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : Cᵒᵖ
hG : G ∈ 𝒢.op
h : G ⟶ op X
⊢ ∃! h', h' ≫ f.op = h

Tactic:
obtain ⟨t, ht, ht'⟩ := hf (unop G) (Set.mem_op.1 hG) h.unop

Result:
case refine_1.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢.op
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : Cᵒᵖ
hG : G ∈ 𝒢.op
h : G ⟶ op X
t : Y ⟶ unop G
ht : f ≫ t = h.unop
ht' : ∀ (y : Y ⟶ unop G), (fun h' => f ≫ h' = h.unop) y → y = t
⊢ ∃! h', h' ≫ f.op = h

Proof state:
case refine_1.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢.op
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : Cᵒᵖ
hG : G ∈ 𝒢.op
h : G ⟶ op X
t : Y ⟶ unop G
ht : f ≫ t = h.unop
ht' : ∀ (y : Y ⟶ unop G), (fun h' => f ≫ h' = h.unop) y → y = t
⊢ ∃! h', h' ≫ f.op = h

Tactic:
exact
  ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Tactic:
refine (isIso_unop_iff _).1 (h𝒢 _ fun G hG h => ?_)

Result:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : G ∈ 𝒢
h : unop Y ⟶ G
⊢ ∃! h', f.unop ≫ h' = h

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : G ∈ 𝒢
h : unop Y ⟶ G
⊢ ∃! h', f.unop ≫ h' = h

Tactic:
obtain ⟨t, ht, ht'⟩ := hf (op G) (Set.op_mem_op.2 hG) h.op

Result:
case refine_2.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : G ∈ 𝒢
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' => h' ≫ f = h.op) y → y = t
⊢ ∃! h', f.unop ≫ h' = h

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢.op
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

Tactic:
refine (isIso_op_iff _).1 (h𝒢 _ fun G hG h => ?_)

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢.op
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : Cᵒᵖ
hG : G ∈ 𝒢.op
h : G ⟶ op X
⊢ ∃! h', h' ≫ f.op = h

Proof state:
case refine_2.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : G ∈ 𝒢
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' => h' ≫ f = h.op) y → y = t
⊢ ∃! h', f.unop ≫ h' = h

Tactic:
refine ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩

Result:
case refine_2.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : G ∈ 𝒢
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' => h' ≫ f = h.op) y → y = t
y : unop X ⟶ G
hy : (fun h' => f.unop ≫ h' = h) y
⊢ (fun h' => h' ≫ f = h.op) y.op

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : G ∈ 𝒢
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' => h' ≫ f = h.op) y → y = t
y : unop X ⟶ G
hy : (fun h' => f.unop ≫ h' = h) y
⊢ (y.op ≫ f).unop = h.op.unop

Tactic:
simpa only using hy

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
⊢ IsDetecting 𝒢.op ↔ IsCodetecting 𝒢

Tactic:
refine ⟨fun h𝒢 X Y f hf => ?_, fun h𝒢 X Y f hf => ?_⟩

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢.op
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Proof state:
case refine_2.intro.intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ G ∈ 𝒢.op, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : G ∈ 𝒢
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' => h' ≫ f = h.op) y → y = t
y : unop X ⟶ G
hy : (fun h' => f.unop ≫ h' = h) y
⊢ (fun h' => h' ≫ f = h.op) y.op

Tactic:
exact Quiver.Hom.unop_inj (by simpa only using hy)

Result:
no goals