mathlib3

36f5ed00 - feat(scripts/modules_used): list imported modules which are actually used (#17507)

feat(scripts/modules_used): list imported modules which are actually used (#17507) ``` % lean --run scripts/modules_used.lean data.nat.order.basic order.synonym order.rel_classes order.monotone order.lattice order.heyting.basic order.bounded_order order.boolean_algebra order.basic logic.nontrivial logic.nonempty logic.is_empty logic.function.basic logic.equiv.defs logic.basic data.subtype data.set.basic data.nat.order.basic data.nat.cast.defs data.nat.basic algebra.ring.defs algebra.order.zero_le_one algebra.order.sub.defs algebra.order.sub.canonical algebra.order.ring.lemmas algebra.order.ring.defs algebra.order.ring.canonical algebra.order.monoid.lemmas algebra.order.monoid.defs algebra.order.monoid.canonical.defs algebra.order.monoid.cancel.defs algebra.group_with_zero.defs algebra.group.defs algebra.group.basic algebra.covariant_and_contravariant ``` Useful for identifying imports which can potentially be removed by splitting files. I'll separately incorporate this as a flag in `leanproject import-graph`, to highlight unused modules. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>