mathlib

14dcfe0c - chore(*): assorted lemmas (#4566)

chore(*): assorted lemmas (#4566) Non-bc changes: * make some lemmas use `coe` instead of `subtype.val`; * make the arguments of `range_comp` explicit, reorder them.