rw [← monotone_dual_iff]
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Monotone g
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconcaveOn 𝕜 s f
⊢ Monotone (⇑OrderDual.toDual ∘ g ∘ ⇑OrderDual.ofDual)