tactic for set triviality

Stream: Is there code for X?

[Kevin Buzzard]

This took me 4 lines longer than I wanted:

import Mathlib

example (I : Type) (i : I) (X Y : Set I) (hX : X ⊆ {i}) (hY : i ∉ Y) : X ∩ Y = ∅ := by
  rw [Set.eq_empty_iff_forall_notMem]
  intro j ⟨hjX, hjY⟩
  apply hY
  apply hX at hjX
  simp_all

hint couldn't solve it. I was hoping that tauto_set would do it but it didn't. In my application the reason I want X ∩ Y = ∅ as the conclusion is that I wrote a lemma which had X ∩ Y = ∅ as a hypothesis. Should I be using Disjoint X Y instead?

[Jireh Loreaux]

The answer to your last question is definitely "yes"

[Etienne Marion]

Here's a one liner for fun:

import Mathlib

example (I : Type) (i : I) (X Y : Set I) (hX : X ⊆ {i}) (hY : i ∉ Y) : X ∩ Y = ∅ :=
  Set.subset_eq_empty (Set.inter_subset_inter_left Y hX) (Set.singleton_inter_eq_empty.2 hY)

[Jireh Loreaux]

I don't understand why this doesn't work:

import Mathlib

example (I : Type) (i : I) (X Y : Set I) (hX : X ⊆ {i}) (hY : i ∉ Y) : Disjoint X Y := by
  rw [Set.disjoint_left]
  aesop

[Jireh Loreaux]

But this does:

import Mathlib

example (I : Type) (i : I) (X Y : Set I) (hX : X ⊆ {i}) (hY : i ∉ Y) : Disjoint X Y := by
  rw [Set.disjoint_left]
  exact?

[Andrew Yang]

import Mathlib

example (I : Type) (i : I) (X Y : Set I) (hX : X ⊆ {i}) (hY : i ∉ Y) : X ∩ Y = ∅ := by
  aesop (add simp Set.subset_singleton_iff_eq) (erase Set.subset_singleton_iff)

[Kevin Buzzard]

Jireh Loreaux said:

The answer to your last question is definitely "yes"

Then should I expect simp to turn X ∩ Y = ∅ into Disjoint X Y?

It's frustrating that all solutions posted require you to know the name of at least one lemma.

[Andrew Yang]

I think my solution is more of an argument that aesop should use Set.subset_singleton_iff_eq instead of Set.subset_singleton_iff as simp lemma because aesop seems to be unable to use the RHS of Set.subset_singleton_iff.

[Jireh Loreaux]

Kevin Buzzard said:

Then should I expect simp to turn X ∩ Y = ∅ into Disjoint X Y?

Seems plausible, but I'm not sure.

[Jireh Loreaux]

Kevin Buzzard said:

It's frustrating that all solutions posted require you to know the name of at least one lemma.

Agreed. There is this to maybe look forward to.

import Mathlib

attribute [grind] Set.subset_singleton_iff Set.disjoint_right

example (I : Type) (i : I) (X Y : Set I) (hX : X ⊆ {i}) (hY : i ∉ Y) : Disjoint X Y := by
  grind

I'm not sure if these are reasonable grind lemmas or not though.

[Yaël Dillies]

Jireh Loreaux said:

Kevin Buzzard said:

Then should I expect simp to turn X ∩ Y = ∅ into Disjoint X Y?

Seems plausible, but I'm not sure.

This was tried in #23371 (which @Jireh Loreaux reviewed), but benchmark isn't happy

[Chase Norman]

(deleted)