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
⊢ MonoOver.Factors (representative.obj P) f → MonoOver.Factors (representative.obj Q) f
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
⊢ Factors P f → Factors Q f
simp only [factors_iff]
no goals
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
⊢ MonoOver.Factors (representative.obj P) f → MonoOver.Factors (representative.obj Q) f
exact fun ⟨u, hu⟩ => ⟨u ≫ ofLE _ _ h, by simp [← hu]⟩
no goals
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
x✝ : MonoOver.Factors (representative.obj P) f
u : Z ⟶ (representative.obj P).obj.left
hu : u ≫ MonoOver.arrow (representative.obj P) = f
⊢ (u ≫ ofLE P Q h) ≫ MonoOver.arrow (representative.obj Q) = f
simp [← hu]