no goals
C : Type u₁
inst✝³ : Category C
X Y Z : C
D : Type u₂
inst✝² : Category D
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
h : mk f ≤ mk g
⊢ ofMkLEMk f g h ≫ g = f
simp [ofMkLEMk]