Commit 2025-08-11 13:56 7f0babde
View on Github →feat(Finset): insert a (s \ {a}) = s if a ∈ s (#28172)
This follows the existing Set lemma (and that one is made simp too).
From MiscYD
feat(Finset): insert a (s \ {a}) = s if a ∈ s (#28172)
This follows the existing Set lemma (and that one is made simp too).
From MiscYD