no goals
ι : Type ?u.132337
α : Type u_1
β : Type ?u.132343
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
s : Set α
ha : 0 ≤ a
hs : IsGLB s b
⊢ IsGLB ((fun b => b * a) '' s) (b * a)
simpa [mul_comm] using hs.mul_left ha