∀ {α : Type u_2} {𝕜 : Type u_6} [inst : Preorder 𝕜] [inst_1 : Zero 𝕜] [inst_2 : Mul 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [ContinuousMul 𝕜] {l : Filter α} {f : α → 𝕜} {b c : 𝕜},
  0 < b →
    ∀ [MulPosStrictMono 𝕜],
      Filter.Tendsto f l (nhdsWithin c (Set.Iio c)) →
        Filter.Tendsto (fun a => f a * b) l (nhdsWithin (c * b) (Set.Iio (c * b)))