C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
⊢ ofMkLEMk f f (_ : mk f ≤ mk f) ≫ f = 𝟙 A₁ ≫ f
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
⊢ ofMkLEMk f f (_ : mk f ≤ mk f) = 𝟙 A₁
apply (cancel_mono f).mp
no goals
C : Type u₁
inst✝² : Category C
X Y Z : C
D : Type u₂
inst✝¹ : Category D
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
⊢ ofMkLEMk f f (_ : mk f ≤ mk f) ≫ f = 𝟙 A₁ ≫ f
simp