Naming `subset_insert_iff` for Set and Finset

Stream: mathlib4

[SnO2WMaN]

Currently, Finset.subset_insert_iff states that s ⊆ insert a t ↔ s.erase a ⊆ t. However, Set.subset_insert_iff states that s s ⊆ insert x t ↔ s ⊆ t ∨ x ∈ s ∧ s \ {x} ⊆ t. I think this naming is confusing because I thought it should be same (or similar) statement (and maybe, there's no similar Finset's statement for Set), and perhaps, it doesn't seem to be following mathlib's naming convention. I thought these should be renamed, how about?

[Yury G. Kudryashov]

The similar statement is true for Sets.

[Yury G. Kudryashov]

We should sync the API here, probably renaming the current Set statement to something like subset_insert_cases