C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
⊢ IsDetecting 𝒢
intro X Y f hf
case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), 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 C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
⊢ g = h
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
refine'
  (isIso_iff_mono_and_epi _).2 ⟨⟨fun g h hgh => h𝒢 _ _ fun G hG i => _⟩, ⟨fun g h hgh => _⟩⟩
case refine'_1.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), 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
case refine'_1
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), 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
obtain ⟨t, -, ht⟩ := hf G hG (i ≫ g ≫ f)
no goals
case refine'_1.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), 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
rw [ht (i ≫ g) (Category.assoc _ _ _), ht (i ≫ h) (hgh.symm ▸ Category.assoc _ _ _)]
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), 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
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
⊢ g = h
refine' h𝒢 _ _ fun G hG i => _
case refine'_2.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), 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
case refine'_2
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), 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
obtain ⟨t, rfl, -⟩ := hf G hG i
no goals
case refine'_2.intro.intro
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), 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
rw [Category.assoc, hgh, Category.assoc]