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

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

Tactic:
rw [isIso_iff_yoneda_map_bijective] at h

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

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

Tactic:
intro hf

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

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ s ∈ 𝒢, Function.Surjective ((coyoneda.obj (op s)).map f)
⊢ 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𝒢 : IsDetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ s ∈ 𝒢, Function.Surjective ((coyoneda.obj (op s)).map f)
A : C
hA : A ∈ 𝒢
g : A ⟶ Y
⊢ ∃ x, x ≫ f = g

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

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

Tactic:
constructor

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

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

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

Tactic:
intro A _

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

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

Tactic:
exact hf A hA g

Result:
no goals

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

Tactic:
exact (h A).2

Result:
no goals

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

Tactic:
intro h

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

Proof state:
case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ s ∈ 𝒢, Function.Surjective ((coyoneda.obj (op s)).map f)
A : C
hA : A ∈ 𝒢
g : A ⟶ Y
⊢ ∀ (y₁ y₂ : A ⟶ X), y₁ ≫ f = g → y₂ ≫ f = 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𝒢 : IsDetecting 𝒢
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ s ∈ 𝒢, Function.Surjective ((coyoneda.obj (op s)).map f)
A : C
hA : A ∈ 𝒢
g : A ⟶ Y
l₁ l₂ : A ⟶ X
h₁ : l₁ ≫ f = g
h₂ : l₂ ≫ f = g
⊢ l₁ = l₂

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

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

Result:
no goals