simp_all [Set.subset_def]
ι : Type u_2
F : Type u_1
inst✝¹ : UnaryModalOperator ι F
inst✝ : DecidableEq F
i : ι
n : ℕ
p q : F
s t : Set F
h : s ⊆ t
⊢ Set.premultimop i n s ⊆ Set.premultimop i n t
no goals