C : Type u₁
inst✝¹ : Category C
X✝ Y Z : C
D : Type u₂
inst✝ : Category D
B : C
X : Subobject B
⊢ ofLE X X (_ : X ≤ X) ≫ arrow X = 𝟙 (underlying.obj X) ≫ arrow X
C : Type u₁
inst✝¹ : Category C
X✝ Y Z : C
D : Type u₂
inst✝ : Category D
B : C
X : Subobject B
⊢ ofLE X X (_ : X ≤ X) = 𝟙 (underlying.obj X)
apply (cancel_mono X.arrow).mp
no goals
C : Type u₁
inst✝¹ : Category C
X✝ Y Z : C
D : Type u₂
inst✝ : Category D
B : C
X : Subobject B
⊢ ofLE X X (_ : X ≤ X) ≫ arrow X = 𝟙 (underlying.obj X) ≫ arrow X
simp