## Stream: general

### Topic: distributing intersection over intersection

#### Bernd Losert (Jan 12 2022 at 00:20):

lemma foobar (A B C : set X) : A ∩ B ∩ C = (A ∩ C) ∩ (B ∩ C) :=
calc
A ∩ B ∩ C = A ∩ B ∩ (C ∩ C) : by rw ← (set.inter_self C)
... = (A ∩ C) ∩ (B ∩ C) : by simp -- Doesn't work.


Is there a special tactic for proving this sort of thing?

#### Bernd Losert (Jan 12 2022 at 00:25):

https://leanprover-community.github.io/mathlib_docs/order/lattice.html#inf_inf_inf_comm <-- This looks like it could help.

#### Bernd Losert (Jan 12 2022 at 00:25):

Doesn't work though:

error: rewrite tactic failed, did not find instance of the pattern in the target expression
A ⊓ B ⊓ (C ⊓ C)


#### Alex J. Best (Jan 12 2022 at 00:27):

One trick for this sort of thing is to apply tactic#ext and simp to convert it into a first order logic problem, then hit it with a logic solver like tactic#tauto

lemma foobar {X : Type*} (A B C : set X) : A ∩ B ∩ C = (A ∩ C) ∩ (B ∩ C) :=
by { ext, simp, tauto }


#### Bernd Losert (Jan 12 2022 at 00:30):

Nice trick.

Last updated: Aug 03 2023 at 10:10 UTC