Simple set theory nonsense

Stream: Is there code for X?

[Adam Topaz]

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]

by ext; tauto!

[Anne Baanen]

Or by finish

[Reid Barton]

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

[Anne Baanen]

This works for me though:

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

[Adam Topaz]

Thanks. finish worked.

[Adam Topaz]

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

[Reid Barton]

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

[Adam Topaz]

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

[Adam Topaz]

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]

This fails too :(

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

[Adam Topaz]

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

That works!

[Reid Barton]

Adam Topaz said:

But this small example also fails:

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)