C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
⊢ IsIso (ofLE P Q h₁)
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
⊢ P = Q
suffices IsIso (ofLE _ _ h₁) by exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
⊢ ∃! h', h' ≫ ofLE P Q h₁ = f
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
⊢ IsIso (ofLE P Q h₁)
refine' h𝒢 _ fun G hG f => _
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : Factors P (f ≫ arrow Q)
⊢ ∃! h', h' ≫ ofLE P Q h₁ = f
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
⊢ ∃! h', h' ≫ ofLE P Q h₁ = f
have : P.Factors (f ≫ Q.arrow) := h₂ _ hG ((factors_iff _ _).2 ⟨_, rfl⟩)
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : Factors P (f ≫ arrow Q)
⊢ (fun h' => h' ≫ ofLE P Q h₁ = f) (factorThru P (f ≫ arrow Q) this)

case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : Factors P (f ≫ arrow Q)
g : G ⟶ underlying.obj P
hg : g ≫ ofLE P Q h₁ = f
⊢ g = factorThru P (f ≫ arrow Q) this
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : Factors P (f ≫ arrow Q)
⊢ ∃! h', h' ≫ ofLE P Q h₁ = f
refine' ⟨factorThru _ _ this, _, fun g (hg : g ≫ _ = f) => _⟩
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
this : IsIso (ofLE P Q h₁)
⊢ P = Q
exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
this : IsIso (ofLE P Q h₁)
⊢ inv (ofLE P Q h₁) ≫ arrow P = arrow Q
simp
no goals
case refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : Factors P (f ≫ arrow Q)
⊢ (fun h' => h' ≫ ofLE P Q h₁ = f) (factorThru P (f ≫ arrow Q) this)
simp only [← cancel_mono Q.arrow, Category.assoc, ofLE_arrow, factorThru_arrow]
no goals
case refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : Factors P (f ≫ arrow Q)
g : G ⟶ underlying.obj P
hg : g ≫ ofLE P Q h₁ = f
⊢ g = factorThru P (f ≫ arrow Q) this
simp only [← cancel_mono (Subobject.ofLE _ _ h₁), ← cancel_mono Q.arrow, hg, Category.assoc,
  ofLE_arrow, factorThru_arrow]