Should `Set.diff_subset_iff`/`sdiff_le_iff` be `@[simp]`?

Stream: mathlib4

[Jovan Gerbscheid]

In #32983 I tried to unify the notion of ≤ with ⊆. But this got stuck because

diff_subset_iff {s t u : Set α} : s \ t ⊆ u ↔ s ⊆ t ∪ u

Is not a simp lemma, while

sdiff_le_iff : a \ b ≤ c ↔ a ≤ b ⊔ c

Is a simp lemma. And changing wither of these two things will break some proofs.

Is it desirable to have this mismatch in simp lemmas, or just an accident?

[Aaron Liu]

how do we decide whether to make something a simp lemma

[Aaron Liu]

I noticed docs#Set.image_subset_iff is a simp lemma but docs#Set.subset_kernImage_iff is not

[Kevin Buzzard]

Aaron Liu said:

how do we decide whether to make something a simp lemma

First you decide what the simp normal form is and then you make your simp lemmas accordingly, I guess.

This had a weird consequence in group theory because if you said to a group theorist "what do you think of $g/h$" they would say "what the heck is /, that is an ambiguous and unused symbol" but if you said "well what do you think of $gh^{-1}$ then they'd say "I see that everywhere". And then if you say to them "and what do you think of "$a + (-b)$" they would say "what is that monstrosity, do you just mean $a-b$?". Somehow the fact that additive groups are often commutative and multiplicative groups often are not means that the sensible form is different in the two domains.