specialize hf (f x) ⟨hx.1, le_rfl⟩ ⟨hy.1, h⟩ ha hb hab
case inr
𝕜 : 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 : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
case inr
𝕜 : 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
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
hf : a • x + b • y ∈ {x_1 | x_1 ∈ s ∧ f x_1 ≤ f x}
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c