-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem eq_of_le_of_isDetecting {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X : C} (P Q : Subobject X)
    (h₁ : P ≤ Q) (h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f) : P = Q

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
⊢ IsIso (P.ofLE Q h₁)

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

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
⊢ ∃! h', h' ≫ P.ofLE Q h₁ = f

Proof state:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
g : G ⟶ underlying.obj P
hg : g ≫ P.ofLE Q h₁ = f
⊢ g = P.factorThru (f ≫ Q.arrow) this

Tactic:
simp only [← cancel_mono (Subobject.ofLE _ _ h₁), ← cancel_mono Q.arrow, hg, Category.assoc,
  ofLE_arrow, factorThru_arrow]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
this : IsIso (P.ofLE Q h₁)
⊢ P = Q

Tactic:
exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))

Result:
no goals

Proof state:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
⊢ (fun h' => h' ≫ P.ofLE Q h₁ = f) (P.factorThru (f ≫ Q.arrow) this)

Tactic:
simp only [← cancel_mono Q.arrow, Category.assoc, ofLE_arrow, factorThru_arrow]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
this : IsIso (P.ofLE Q h₁)
⊢ inv (P.ofLE Q h₁) ≫ P.arrow = Q.arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
⊢ ∃! h', h' ≫ P.ofLE Q h₁ = f

Tactic:
have : P.Factors (f ≫ Q.arrow) := h₂ _ hG ((factors_iff _ _).2 ⟨_, rfl⟩)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
⊢ ∃! h', h' ≫ P.ofLE Q h₁ = f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
⊢ ∃! h', h' ≫ P.ofLE Q h₁ = f

Tactic:
refine ⟨factorThru _ _ this, ?_, fun g (hg : g ≫ _ = f) => ?_⟩

Result:
case refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
⊢ (fun h' => h' ≫ P.ofLE Q h₁ = f) (P.factorThru (f ≫ Q.arrow) this)

case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : P.Factors (f ≫ Q.arrow)
g : G ⟶ underlying.obj P
hg : g ≫ P.ofLE Q h₁ = f
⊢ g = P.factorThru (f ≫ Q.arrow) this

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
⊢ P = Q

Tactic:
suffices IsIso (ofLE _ _ h₁) by exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
⊢ IsIso (P.ofLE Q h₁)