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