no goals
ι : Type ?u.191131
α : Type u_1
β : Type ?u.191137
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
s : Set α
ha : 0 ≤ a
hs : IsLUB s b
⊢ IsLUB ((fun b => b * a) '' s) (b * a)
simpa [mul_comm] using hs.mul_left ha