Tactic Requests

Stream: mathlib4

[Kenny Lau]

If anyone has any request at all for any tactic, it might be useful to say them here so that we just have a list going here in case anyone is feeling helpful in the future :slight_smile:

[Patrick Massot]

This thread idea already exists at #general > "Missing Tactics" list