Sets

Stream: general

[Wouter Smeenk]

Why is Set ℤ needed here:

import Mathlib.Init.Set

variable {x₁ x₂ x₃
          x₄ x₅ x₆
          x₇ x₈ x₉ s: ℤ}

example : ∀ x, x ∈ ({ x₁, x₂, x₃,
                      x₄, x₅, x₆,
                      x₇, x₈, x₉ } : Set ℤ)  → x = x → False := by
    sorry

If I replace Set ℤ with _ I get:

typeclass instance problem is stuck, it is often due to metavariables
  Insert ℤ (?m.270 x)

Why is this? Is there a better way to create this statement? I want to state something which holds for each of the variables.

[Eric Wieser]

Without Set ℤ lean doesn't know whether you mean Set or Finset

[Henrik Böving]

Its because all of the notation that you have here is generic. The element of notation can for example also be used for lists and the collection notation could also be used for collections other than mathematical sets (like say HashSets) so Lean cannot know without you telling it that you actually mean a mathematical set here.

For an alternative way you could always use a list and fold over that I guess? But the actual mathlib users might have a better idea

[Wouter Smeenk]

Ah this does work indeed:

example : ∀ x, x ∈ [ x₁, x₂, x₃,
                     x₄, x₅, x₆,
                     x₇, x₈, x₉ ]  → x = x → False := by
    sorry

[Eric Wieser]

What's the problem with your original version?

[Wouter Smeenk]

It is more verbose with the Set Z.

[Eric Wieser]

Sure, but it's probably easier to prove things about