distributing intersection over intersection

Stream: general

[Bernd Losert]

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]

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

[Bernd Losert]

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]

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]

Nice trick.