I don't want to sound snarky, but since you mentioned that Redis does not document if/that "multiple key expiry is guaranteed to occur at the same time if keys have the same EXPIREAT setting", I am tempted to ask - why did you not check the implementation you're using? That's the unique selling point of using FOSS - you don't have rely on documentation or observational guesswork - you can wade in and really see for yourself! Redis' source code is especially readable in my opinion (thanks again, antirez, for creating this little load-bearing gem of a data structure server), so I would very much encourage you to try, even if C is not your particular forte :)
Because documentation is what is needs to be: A simplified and necessarily incomplete description of program behavior. It's a trade-off, since a complete and exhaustive description of all intricacies of potential program behavior would be at least as complex as the definition (= its source code) of said program.
If you happen to have a question that ends up on the wrong side of that trade-off between documentation's completeness and accessibility, you will have to descend into the depths that lie beneath. I believe the redis documentation actually strikes a rather OK balance in that regard.
That's a great suggestion, and OP should do this, but even if OP verifies behaviour today through code inspection, it's possible a future release could change it. The problem is that Redis doesn't want to make that guarantee so you can't rely on it.
Would Redis Keyspace Notifications [1] help in this case? Like a script that runs when a specific key expires, such that all other related keys can be deleted too.