Theorem: QuasiconcaveOn.monotone_comp (Sion/Concavexity.lean)

State before:
𝕜 : 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
⊢ QuasiconcaveOn 𝕜 s (g ∘ f)
Tactic:
apply QuasiconvexOn.monotone_comp (β := βᵒᵈ) (γ := γᵒᵈ) (f := f) _ hf
State after:
𝕜 : 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

State before:
𝕜 : 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
Tactic:
rw [← monotone_dual_iff]
State after:
𝕜 : 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)

State before:
𝕜 : 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)
Tactic:
exact hg
State after:
no goals