Commit 2024-09-17 19:29 f926760e
View on Github →chore(Data/Finset/Image): simplify proof of filter_mem_image_eq_image (#16821)
Simplify this proof - it's really just a combination of three existing facts.
The lemma filter_mem_image_eq_image is used nowhere in mathlib, so I wouldn't have an objection to deleting it instead...