-- Mathlib/CategoryTheory/Generator/Basic.lean
lemma IsCodetecting.isIso_iff_of_epi {𝒢 : Set C} (h𝒢 : IsCodetecting 𝒢)
    {X Y : C} (f : X ⟶ Y) [Epi f] :
    IsIso f ↔ ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)

Proof state:
case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)
A : C
hA : A ∈ 𝒢
g : X ⟶ A
⊢ ∀ (y₁ y₂ : Y ⟶ A), f ≫ y₁ = g → f ≫ y₂ = g → y₁ = y₂

Tactic:
intro l₁ l₂ h₁ h₂

Result:
case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)
A : C
hA : A ∈ 𝒢
g : X ⟶ A
l₁ l₂ : Y ⟶ A
h₁ : f ≫ l₁ = g
h₂ : f ≫ l₂ = g
⊢ l₁ = l₂

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ IsIso f ↔ ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ IsIso f → ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ (∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)) → IsIso f

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)
⊢ IsIso f

Tactic:
refine h𝒢 _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)

Result:
case mpr.refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)
A : C
hA : A ∈ 𝒢
g : X ⟶ A
⊢ ∃ x, f ≫ x = g

case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)
A : C
hA : A ∈ 𝒢
g : X ⟶ A
⊢ ∀ (y₁ y₂ : Y ⟶ A), f ≫ y₁ = g → f ≫ y₂ = g → y₁ = y₂

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ (∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)) → IsIso f

Tactic:
intro hf

Result:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)
⊢ IsIso f

Proof state:
case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)
A : C
hA : A ∈ 𝒢
g : X ⟶ A
l₁ l₂ : Y ⟶ A
h₁ : f ≫ l₁ = g
h₂ : f ≫ l₂ = g
⊢ l₁ = l₂

Tactic:
rw [← cancel_epi f, h₁, h₂]

Result:
no goals

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : IsIso f
⊢ ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)

Tactic:
rw [isIso_iff_coyoneda_map_bijective] at h

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : ∀ (T : C), Function.Bijective fun x => f ≫ x
⊢ ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : ∀ (T : C), Function.Bijective fun x => f ≫ x
⊢ ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)

Tactic:
intro A _

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : ∀ (T : C), Function.Bijective fun x => f ≫ x
A : C
a✝ : A ∈ 𝒢
⊢ Function.Surjective ((yoneda.obj A).map f.op)

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
⊢ IsIso f → ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)

Tactic:
intro h

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : IsIso f
⊢ ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : ∀ (T : C), Function.Bijective fun x => f ≫ x
A : C
a✝ : A ∈ 𝒢
⊢ Function.Surjective ((yoneda.obj A).map f.op)

Tactic:
exact (h A).2

Result:
no goals

Proof state:
case mpr.refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op)
A : C
hA : A ∈ 𝒢
g : X ⟶ A
⊢ ∃ x, f ≫ x = g

Tactic:
exact hf A hA g

Result:
no goals