C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : Factors P g
⊢ (f ≫ factorThru P g h) ≫ arrow P = factorThru P (f ≫ g) (_ : Factors P (f ≫ g)) ≫ arrow P
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : Factors P g
⊢ f ≫ factorThru P g h = factorThru P (f ≫ g) (_ : Factors P (f ≫ g))
apply (cancel_mono P.arrow).mp
no goals
C : Type u₁
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : Factors P g
⊢ (f ≫ factorThru P g h) ≫ arrow P = factorThru P (f ≫ g) (_ : Factors P (f ≫ g)) ≫ arrow P
simp