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