finite): add `finite_to_set` lemmas to simp set (#18026)

Commit

2 years ago

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.

Author

kmill

Parents

f2528722

mathlib3 8a8ac5bb - refactor(data/set/finite): add `finite_to_set` lemmas to simp set (#18026)

mathlib3
8a8ac5bb - refactor(data/set/finite): add `finite_to_set` lemmas to simp set (#18026)