no goals
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
inst✝ : HasPullbacks C
B : C
X Y : Subobject B
⊢ ofLE (X ⊓ Y) X (_ : (inf.obj X).obj Y ≤ X) ≫ MonoOver.arrow (representative.obj X) = arrow (X ⊓ Y)
simp