case h
C : Type u₁
inst✝¹ : Category C
X✝ Y Z : C
D : Type u₂
inst✝ : Category D
X : C
P : Subobject X
h : Factors P (arrow P)
⊢ factorThru P (arrow P) h ≫ arrow P = 𝟙 (underlying.obj P) ≫ arrow P
C : Type u₁
inst✝¹ : Category C
X✝ Y Z : C
D : Type u₂
inst✝ : Category D
X : C
P : Subobject X
h : Factors P (arrow P)
⊢ factorThru P (arrow P) h = 𝟙 (underlying.obj P)
ext
no goals
case h
C : Type u₁
inst✝¹ : Category C
X✝ Y Z : C
D : Type u₂
inst✝ : Category D
X : C
P : Subobject X
h : Factors P (arrow P)
⊢ factorThru P (arrow P) h ≫ arrow P = 𝟙 (underlying.obj P) ≫ arrow P
simp