# Zulip Chat Archive

## Stream: new members

### Topic: Basic set equalities (e.g. `(s \ t)ᶜ = sᶜ ∪ t`)

#### Adomas Baliuka (Nov 03 2023 at 21:21):

I needed the set equality `(s \ t)ᶜ = sᶜ ∪ t`

, which doesn't seem to be in Mathlib, although it seems common (Wikipedia's "Set Complement" mentions it). That should mean it's very easy?! I did it eventually (see below for completeness) but isn't there a simple way to prove this in one line? The tactics I usually try `exact?, aesop, simp_all, rfl, trivial, apply?`

couldn't do it...

```
import Mathlib
open Set
variable {s t : Set α} {x : α}
lemma mem_and_notmem_of_in_diff : x ∈ s \ t ↔ (x ∈ s ∧ x ∉ t) := by simp
lemma mem_and_notmem_of_notin_diff : x ∉ s \ t ↔ (x ∉ s ∨ x ∈ t) := by
have := Iff.not (@mem_and_notmem_of_in_diff α s t x)
push_neg at this
convert this -- I was hoping to be done here...
constructor
intro h xins
simp_all only [false_or]
intro h
by_cases xins : x ∈ s
· right; exact h xins
· left; assumption
lemma compl_diff_eq_union_compl : (s \ t)ᶜ = sᶜ ∪ t := by
ext x
constructor
· intro h
have := (Set.mem_compl_iff (s \ t) x).mp h
exact mem_and_notmem_of_notin_diff.mp this
· intro h
simp at h
apply mem_compl
apply mem_and_notmem_of_notin_diff.mpr
exact h
```

#### Riccardo Brasca (Nov 03 2023 at 21:49):

This

```
import Mathlib
open Set
variable {s t : Set α} {x : α}
lemma compl_diff_eq_union_compl : (s \ t)ᶜ = sᶜ ∪ t := by
nth_rewrite 2 [← compl_compl t]
rw [← compl_inter]
rfl
```

also works, let me see if I find the exact statement you want.

#### Joël Riou (Nov 03 2023 at 21:53):

Alternatively, we can do

```
import Mathlib.Data.Set.Basic
lemma compl_diff_eq_union_compl {α : Type*} (s t : Set α) :
(s \ t)ᶜ = sᶜ ∪ t := by
ext x
simp only [compl_sdiff, Set.mem_union, Set.mem_compl_iff]
tauto
```

#### Adomas Baliuka (Nov 03 2023 at 21:54):

How did you do this so quickly? I don't assume it's by having all these lemma names memorized.

#### Joël Riou (Nov 03 2023 at 21:55):

I did `ext; simp?; tauto`

!

#### Riccardo Brasca (Nov 03 2023 at 21:57):

```
import Mathlib
open Set
variable {s t : Set α} {x : α}
lemma compl_diff_eq_union_compl : (s \ t)ᶜ = sᶜ ∪ t := by
simp [himp_eq, Set.union_comm]
```

#### Riccardo Brasca (Nov 03 2023 at 21:58):

OK let's stop the golfing competition... but it's a result we surely want.

#### Adomas Baliuka (Nov 03 2023 at 21:59):

Thanks! I guess the takeaway for me is to add `simp?`

to my "list of things to try". (Could one make a multi-threaded tactic that just tries all of `exact?, aesop, simp_all, rfl, trivial, apply?, simp?`

at the same time and shows the first hit (or fails)?)

Actually, maybe my goal does exist in Mathlib after all as `compl_sdiff`

. It uses a "Heyting implication" (the reason I didn't find it using loogle), which I've never heard of before...

#### Riccardo Brasca (Nov 03 2023 at 22:02):

Yeah, this is a more serious question. Heyting implication is something in Boolean algebra (and `Set α`

is a Boolean algebra), so `simp`

is applying docs#compl_sdiff, that says

```
(x \ y)ᶜ = x ⇨ y
```

Now, for sets it is completely ridiculous to say that the RHS is simpler than the LHS.

#### Riccardo Brasca (Nov 03 2023 at 22:06):

@Yaël Dillies what do you think? (pinging you because git blames you as the author of `compl_sdiff`

, but it can be wrong).

#### Yaël Dillies (Nov 03 2023 at 22:29):

Riccardo Brasca said:

Now, for sets it is completely ridiculous to say that the RHS is simpler than the LHS.

You're free to add

```
@[simp] lemma Set.himp_eq (s t : Set α) : s ⇨ t = t ∪ sᶜ := himp_eq
```

#### Yaël Dillies (Nov 03 2023 at 22:32):

I think it's a bit of a shame since `s ⇨ t`

has a very nice interpretation: elements of `s ⇨ t`

exactly are the elements `a`

such that `a ∈ s → a ∈ t`

.

#### Eric Wieser (Nov 03 2023 at 23:05):

That seems like it might be a good example to add to the docstring for `himp`

#### Yaël Dillies (Nov 03 2023 at 23:15):

I swear I wrote that example in a docstring somewhere already, but I'm happy to make it more prominent!

#### Eric Wieser (Nov 03 2023 at 23:31):

Last updated: Dec 20 2023 at 11:08 UTC