How does Lean handle the equal operator on sets?

Stream: new members

[Andrew Lubrino]

I've been working through Velleman's suggested set theory proof problems in Proof Designer (except I'm doing the proofs in Lean and not Proof Designer). I'm stuck on #8. I'm not sure I understand how Lean handles the equality operator on sets. Can Lean solve the below problem with how it is currently stated? I've tried using eq.subst and iff.elim_leftand neither worked. I'm mainly looking for help where the sorry is placed now.

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


  example (h : A ∩ (B \ C) = ∅): A ∩ B ⊆ C :=
  assume x,
  assume h₁ : x ∈ A ∩ B,
  show x ∈ C, from
  by_contradiction
    (assume h₂ : x ∉ C,
    have h₃ : x ∈ B \ C, from and.intro h₁.right h₂,
    have h₄ : x ∈ A ∩ (B \ C), from and.intro h₁.left h₃,
    show x ∈ ∅, from sorry)

[Alex J. Best]

you can use docs#eq.subst directly here

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


  example (h : A ∩ (B \ C) = ∅): A ∩ B ⊆ C :=
  assume x,
  assume h₁ : x ∈ A ∩ B,
  show x ∈ C, from
  by_contradiction
    (assume h₂ : x ∉ C,
    have h₃ : x ∈ B \ C, from and.intro h₁.right h₂,
    have h₄ : x ∈ A ∩ (B \ C), from and.intro h₁.left h₃,
    show x ∈ ∅, from h.subst h₄)

[Andrew Lubrino]

That works. Thank you. I originally tried (and then tested it again after your response) the below and that doesn't work. What's the difference between the below and what you have above?

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


  example (h : A ∩ (B \ C) = ∅): A ∩ B ⊆ C :=
  assume x,
  assume h₁ : x ∈ A ∩ B,
  show x ∈ C, from
  by_contradiction
    (assume h₂ : x ∉ C,
    have h₃ : x ∈ B \ C, from and.intro h₁.right h₂,
    have h₄ : x ∈ A ∩ (B \ C), from and.intro h₁.left h₃,
    show x ∈ ∅, from eq.subst h h₄)

[Alex J. Best]

Huh, I'm actually not sure, I would have thought they would both work. It could be some elaboration order quirk, hopefully someone else can answer!

[Reid Barton]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Natural.20Numbers.20Game/near/199965854

[Reid Barton]

... seems related, except the conclusion here is the opposite?

[Reid Barton]

Maybe eq.subst should not have elab_as_eliminator, and could this be related to why the "stupid triangle" is so stupid?

[Andrew Lubrino]

Hmm. Weird. I'll just try both whenever I get an error like this in the future I guess.

Thanks!

[Reid Barton]

FWIW, pretty much everyone uses the rw tactic instead of using eq.subst directly.

[Andrew Lubrino]

Oh really? I'm still very much a beginner in Lean, so I'm not really too familiar with rw. I'm going to look into that and start using it more.