Commit 2023-01-01 15:14 8a8ac5bb

View on Github →

refactor(data/set/finite): add finite_to_set lemmas to simp set (#18026) Making these be simp lemmas allows simp discharge such simple set.finite side-goals.

Estimated changes

Modified src/data/set/finite.lean

modified theorem finset.finite_to_set

modified theorem list.finite_to_set

modified theorem multiset.finite_to_set