no goals
α : Type u_1
inst✝ : LinearOrderedField α
a✝ a : α
h : 0 < a
b c : α
⊢ (fun x x_1 => x * x_1) a '' Ioo b c = Ioo (a * b) (a * c)
convert image_mul_right_Ioo b c h using 1 <;> simp only [mul_comm _ a]