no goals
α : Type ?u.462617
inst✝¹ : LinearOrderedField α
a : α
k : Type u_1
inst✝ : LinearOrderedField k
x : k
hx : 0 < x
⊢ (fun y => x * y) '' Ioi 0 = Ioi 0
erw [(Units.mk0 x hx.ne').mulLeft.image_eq_preimage, preimage_const_mul_Ioi 0 (inv_pos.mpr hx),
  zero_div]