set equals empty set in hypothesis

Stream: new members

[Claus-Peter Becke]

I'm trying to prove the following assertion:

import data.set
import tactic.basic
open set

variable {U : Type}
variables A B C : set U
variable x : U

example (h1 : A ∩ (B \ C) = ∅) : A ∩ B ⊆ C :=
begin
    intro x,
    intro h2,
    cases h2 with h2 h3,
    ...
end

If I had the content of h1 as a goal I could apply the ext-tactic to rewrite the equality as an equivalence. I would like to achieve for example as a result an assertion as x \notin A \or x \notin B \or x \in C. With this hypothesis it would be possible to prove the goal. I don't find a way to rewrite h1.

[Ruben Van de Velde]

Looking at https://leanprover-community.github.io/mathlib_docs/data/set/basic.html, I started with

    rw set.eq_empty_iff_forall_not_mem at h1,
    have := h1 x,
    rw set.mem_inter_iff at this,

[Kevin Buzzard]

The ext tactic, if the goal is an equality s = t of sets, would just apply the theorem set.ext : ∀ {α : Type u} {a b : set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b. Because this is of the form P -> Q, it works great if Q is the goal, but can't be used if Q is the hypothesis. However there is a corresponding "if and only if" version, set.ext_iff : ∀ {α : Type u} {s t : set α}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t. So the way to do ext on a hypothesis which is an equality of two sets is rw set.ext_iff.
for
However, as Ruben points out, if you use extensionality directly on h1 : X = \empty you'll end up with the slightly annoying \forall a, a \in X \iff x \in \empty, and then you'd have to rewrite a proof of a \in \empty \iff false and then a proof of (P \iff false) \iff \not P and then maybe you want to rewrite \not a \in X to a \notin X -- stuff which mathematicians just do intuitively -- but can be a pain in theorem provers. What do you actually want? If you want an elementwise statement, you probably want something like "\forall a, a \notin X -- that's the step you want. You could look to see if it's there already:

example : A = ∅ → ∀ x, x ∉ A := by library_search

and indeed that statement, the one you may (or may not) want, is in the library; the library_search tactic says that the proof is eq_empty_iff_forall_not_mem.mp . That mp at the end means "we have the theorem eq_empty_iff_forall_not_mem , but it's an if and only if, and you only wanted one way (iff.mp is the P -> Q part of P <-> Q). Because it's an iff, this means you can rewrite it. That's some kind of algorithmic way to make progress here.

[Kevin Buzzard]

@Claus-Peter Becke

[Kevin Buzzard]

This is annoying -- why can't I get automation to do this?

[Kenny Lau]

have you tried simp with contextual

[Kevin Buzzard]

example (h1 : A ∩ (B \ C) = ∅) : A ∩ B ⊆ C :=
begin
    intro x,
    intro h2,
    cases h2 with h2 h3,
    rw set.eq_empty_iff_forall_not_mem at h1,
    specialize h1 x,
    rw mem_inter_iff at h1,
    rw mem_diff at h1,
    tauto!,
end

[Shing Tak Lam]

example (h1 : A ∩ (B \ C) = ∅) : A ∩ B ⊆ C :=
begin
  rwa [←inter_diff_assoc, diff_eq_empty] at h1
end

(need to change the data.set import to data.set.basic)

[Bryan Gin-ge Chen]

Wow, data.set doesn't import data.set.basic? If so, that should be fixed.

[Shing Tak Lam]

It does, I don't know what happened... :face_palm:

[Kevin Buzzard]

Aah so that's the trick -- never use extensionality at all.

[Kenny Lau]

I guess the trick is to generalize

[Claus-Peter Becke]

A lot of thanks for your very helpful comments, which supported to close the goal. Again I learned of how to deal better with Lean.