mathlib

a540d79b - chore(archive/sensitivity): Clean up function coercion in sensitivity proof (depends on #2756) (#2758)

chore(archive/sensitivity): Clean up function coercion in sensitivity proof (depends on #2756) (#2758) This formalizes the proof of an old conjecture: `is_awesome Gabriel`. I also took the opportunity to remove type class struggling, which I think is related to the proof of `is_awesome Floris`. I think @jcommelin should also update this sensitivity file to use his sum notations if applicable. Co-authored-by: Johan Commelin <johan@commelin.net>