-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem IsSeparating.isDetecting [Balanced C] {𝒢 : Set C} (h𝒢 : IsSeparating 𝒢) :
    IsDetecting 𝒢

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

Tactic:
refine
  (isIso_iff_mono_and_epi _).2 ⟨⟨fun g h hgh => h𝒢 _ _ fun G hG i => ?_⟩, ⟨fun g h hgh => ?_⟩⟩

Result:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : G ∈ 𝒢
i : G ⟶ Z✝
⊢ i ≫ g = i ≫ h

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
⊢ g = h

Proof state:
case refine_2.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
G : C
hG : G ∈ 𝒢
t : G ⟶ X
⊢ (t ≫ f) ≫ g = (t ≫ f) ≫ h

Tactic:
rw [Category.assoc, hgh, Category.assoc]

Result:
no goals

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : G ∈ 𝒢
i : G ⟶ Z✝
⊢ i ≫ g = i ≫ h

Tactic:
obtain ⟨t, -, ht⟩ := hf G hG (i ≫ g ≫ f)

Result:
case refine_1.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : G ∈ 𝒢
i : G ⟶ Z✝
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun h' => h' ≫ f = i ≫ g ≫ f) y → y = t
⊢ i ≫ g = i ≫ h

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
⊢ g = h

Tactic:
refine h𝒢 _ _ fun G hG i => ?_

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
G : C
hG : G ∈ 𝒢
i : G ⟶ Y
⊢ i ≫ g = i ≫ h

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
G : C
hG : G ∈ 𝒢
i : G ⟶ Y
⊢ i ≫ g = i ≫ h

Tactic:
obtain ⟨t, rfl, -⟩ := hf G hG i

Result:
case refine_2.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
G : C
hG : G ∈ 𝒢
t : G ⟶ X
⊢ (t ≫ f) ≫ g = (t ≫ f) ≫ h

Proof state:
case refine_1.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : G ∈ 𝒢
i : G ⟶ Z✝
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun h' => h' ≫ f = i ≫ g ≫ f) y → y = t
⊢ i ≫ g = i ≫ h

Tactic:
rw [ht (i ≫ g) (Category.assoc _ _ _), ht (i ≫ h) (hgh.symm ▸ Category.assoc _ _ _)]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
⊢ IsDetecting 𝒢

Tactic:
intro X Y f hf

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