## 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.

@[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):

docs#HImp.himp

Last updated: Dec 20 2023 at 11:08 UTC