Vlad Tsyrklevich

No, I'm talking about an application flow that revokes it's own access after authorization. It 1) gets authorized, 2) performs its operation, and 3) revokes it's own access (not just...

I hadn't seen that thread, thanks for the feedback! I tried to integrate all of your changes, with some minor modifications of my own to wording where I thought appropriate....

I'll repost this [comment](https://github.com/leanprover-community/mathlib4/pull/32531#issuecomment-3656805740) since I'm not sure if you've seen it: mathlib generally wants maximum generality for the results it includes. I am not familiar with the proof of...

Also, I have not deeply looked at the argument to see whether it makes sense, but: you are directly using the combinatorial Hall's marriage theorem--have you seen that there is...