Commit 2024-05-11 18:18 c212f77a

feat: lemmas relating Finset.univ and List.get (#11704) We add sufficient lemmas for the simplifier to prove ∀ (l : List α), Finset.univ.val.map l.get = ↑l, as well as the easier to apply phrasing ∀ (l : List α), Finset.univ.val.map (f <| l.get ·) = ↑(l.map f). We then add lemmas stating the corollaries for functions out of Finset which are built out of Multiset.map, such as Finset.image and Finset.prod.