∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α} {t : Set β}, MonotoneOn g t → MonotoneOn f s → Set.MapsTo f s t → MonotoneOn (g ∘ f) s