## Stream: Is there code for X?

### Topic: Simple set theory nonsense

#### Adam Topaz (Oct 06 2020 at 15:11):

Is there some tactic that will solve goals of the form

C ∩ (A ∩ B) = A ∩ (B ∩ C)


where A B C : set X ?

#### Simon Hudon (Oct 06 2020 at 15:13):

by ext; tauto!

#### Anne Baanen (Oct 06 2020 at 15:13):

Or by finish

#### Reid Barton (Oct 06 2020 at 15:13):

I think @Chris Hughes also had some incantation that involved finish with some extra arguments

#### Anne Baanen (Oct 06 2020 at 15:15):

This works for me though:

example {α : Type*} {a b c : set α} : c ∩ (a ∩ b) = a ∩ (b ∩ c) := by finish


#### Adam Topaz (Oct 06 2020 at 15:15):

Thanks. finish worked.

#### Adam Topaz (Oct 06 2020 at 15:16):

It had a hard time with this though AA ∩ Q ∩ (AA ∩ Q1) = AA ∩ (Q ∩ Q1).

#### Reid Barton (Oct 06 2020 at 15:18):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/set.20tactic/near/186732870

#### Adam Topaz (Oct 06 2020 at 15:24):

To be fair, I'm using it in a proof that's ~130 lines long, and it fails with a deterministic timeout.

#### Adam Topaz (Oct 06 2020 at 15:26):

But this small example also fails:

example {α : Type*} (a b c : set α) : a ∩ b ∩ (a ∩ c) = a ∩ (b ∩ c) := by finish [set.ext_iff]


#### Adam Topaz (Oct 06 2020 at 15:26):

This fails too :(

example {α : Type*} (a b c : set α) : a ∩ b ∩ (a ∩ c) = a ∩ (b ∩ c) := by ext; tauto!


#### Adam Topaz (Oct 06 2020 at 15:27):

example {α : Type*} (a b c : set α) : a ∩ b ∩ (a ∩ c) = a ∩ (b ∩ c) := by tidy


That works!

#### Reid Barton (Oct 06 2020 at 15:28):

example {α : Type*} (a b c : set α) : a ∩ b ∩ (a ∩ c) = a ∩ (b ∩ c) := by finish [set.ext_iff]

Interesting, I thought I tried that exact example, but actually what I tried was c ∩ (a ∩ b) = (c ∩ a) ∩ (b ∩ c)