Proving membership to a set builder

Stream: new members

[Giovanni Mascellani]

Hi, I am trying to find in mathlib4 some fact similar to x ∈ y ↔ a ∈ Finset.Icc a b ∧ f x given that y is defined as {x ∈ Finset.Icc a b | f x}, but I am failing completely. Anybody could give me a hint? Thanks!

[Riccardo Brasca]

Can you write a #mwe? Thanks!

[Daniel Weber]

Does docs#Finset.mem_filter work?

import Mathlib

example (f : α → Prop) [DecidablePred f] [Preorder α] [LocallyFiniteOrder α] : x ∈ {x ∈ Finset.Icc a b | f x} ↔ x ∈ Finset.Icc a b ∧ f x := by
  exact Finset.mem_filter

[Ruben Van de Velde]

Daniel, I think the goal was to help Giovanni ask questions in a way that's easy to answer :)

[Yaël Dillies]

Sorry, we currently don't have unified naming around set builder notation. We'll hopefully get there eventually!

[Kyle Miller]

A slight definitional equality abuse in Daniel's suggestion is that it's unfolding the definition of membership and SetOf. To go through rewrites, there's docs#Set.mem_setOf_eq

[Daniel Weber]

Kyle Miller said:

A slight definitional equality abuse in Daniel's suggestion is that it's unfolding the definition of membership and SetOf. To go through rewrites, there's docs#Set.mem_setOf_eq

This is a Finset, so there's no setOf here

[Giovanni Mascellani]

Ok, I got my answer, but for the future would this have worked as a MWE?

import Mathlib
example (x a b : ℕ)
  : x ∈ {x ∈ Finset.Icc a b | 10 ∣ x} ↔ x ∈ Finset.Icc a b ∧ 10 ∣ x := by
  sorry

Relatedly, why doesn't this work? It complains that it cannot synthesize Membership ℕ { x // x ∈ filter (fun x ↦ 10 ∣ x) (Icc a b) }:

import Mathlib
example (x a b : ℕ) (y : {x ∈ Finset.Icc a b | 10 ∣ x})
  : x ∈ y ↔ x ∈ Finset.Icc a b ∧ 10 ∣ x := by
  sorry

Thanks again!

[Kyle Miller]

#mwe suggests including imports too; a rule of thumb is that the "view in Lean 4 playground" link in the upper right-hand corner of a code block should work.

[Giovanni Mascellani]

Good point, I fixed my MWE.

[Daniel Weber]

Giovanni Mascellani said:

Relatedly, why doesn't this work? It complains that it cannot synthesize Membership ℕ { x // x ∈ filter (fun x ↦ 10 ∣ x) (Icc a b) }:

import Mathlib
example (x a b : ℕ) (y : {x ∈ Finset.Icc a b | 10 ∣ x})
  : x ∈ y ↔ x ∈ Finset.Icc a b ∧ 10 ∣ x := by
  sorry

Thanks again!

y : {x ∈ Finset.Icc a b | 10 ∣ x} means that y is a term of type {x ∈ Finset.Icc a b | 10 ∣ x}, which means (approximately) that y is a natural number in the set, so x ∈ y doesn't make sense

[Daniel Weber]

(deleted)

[Giovanni Mascellani]

Right, rookie mistake!

[Riccardo Brasca]

Note that

import Mathlib
example (x a b : ℕ) : x ∈ {x ∈ Finset.Icc a b | 10 ∣ x} ↔ x ∈ Finset.Icc a b ∧ 10 ∣ x := by
  exact?

works, suggesting exact Finset.mem_filter.

[Giovanni Mascellani]

Right, I had tried apply?, but probably in a context that was broken for other reasons, and forgot to invalidate my assumption when I got the context right.