∀ {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [inst : Preorder α] [inst_1 : (i : ι) → Preorder (β i)]
  [inst_2 : (i : ι) → SMul α (β i)] [inst_3 : (i : ι) → Zero (β i)] [∀ (i : ι), SMulPosMono α (β i)],
  SMulPosMono α ((i : ι) → β i)