unfolding specific instance

Stream: new members

[Miroslav Olšák]

Is it possible to tell lean to unfold only a specific instance of a typeclass function? This typically happens when I have my own instance of a typeclass, so I need to dig inside, but then there are also other instances of the same typeclass in the library. For example, what I mean:

example (l : list ℕ) (s : set ℕ) (n : ℕ)
  : (n ∈ l) = (n ∈ s) :=
begin
  unfold has_mem.mem /- somehow only for set -/, unfold set.mem,
  sorry
end

I would like it to end up with the goal n ∈ l = s n. I tried unfold set.has_mem.mem but that fails.

[Kevin Buzzard]

You can use change to get there manually

[Kevin Buzzard]

Or you can zoom into the term in conv mode and just unfold the part you want

[Miroslav Olšák]

change (or show) can be impractical in practice when I deal with more complex terms, I don't know conv mode (I can look at it)

[Miroslav Olšák]

I just thought whether it could be possible to directly target an instance, it feels quite natural to me.

[Miroslav Olšák]

Otherwise, I can write my own unfolding lemmata, I guess.

[Kevin Buzzard]

I can't get unfold to work in conv mode. change you can make easier by using wildcards:

example (l : list ℕ) (s : set ℕ) (n : ℕ)
  : (n ∈ l) = (n ∈ s) :=
begin
  change _ = s _,
  -- ⊢ n ∈ l = s n
  sorry
end

[Kevin Buzzard]

But rw works

[Kevin Buzzard]

lemma set.has_mem_def {α : Type*} (s : set α) (a : α) : a ∈ s = s a := rfl

example (l : list ℕ) (s : set ℕ) (n : ℕ)
  : (n ∈ l) = (n ∈ s) :=
begin
  rw set.has_mem_def,
  -- ⊢ n ∈ l = s n
  sorry
end

[Miroslav Olšák]

OK, I will do it this way, that is what I meant with writing custom unfolding lemmata.