Coercing "nested" types

Stream: new members

[AG]

How does one coerce nested types in lean?

For example, I can coerce a finset to a set no problem…

def my_def (F : set α): Prop :=
  true

lemma my_lemma (F : finset α) : my_def F :=
  by trivial

But Lean throws an error when I try to coerce a finset of finsets to a set of sets…

def my_def' (F : set (set α)): Prop :=
  true

lemma my_lemma' (F : finset (finset α)) : my_def' F :=
  by trivial

The error says: Type mismatch at application my_def' F. Term F has type finset (finset α) but is expected to have type set (set α).

[Johan Commelin]

@AG You'll have to choose an intermediate step. Do you want to pass through finset (set α) or through set (finset α).
Anyway, I expect that coe '' F or F.image coe should work.

[AG]

Oh that makes sense, thank you. It seems I can get to the intermediary easily enough by writing it as (F : set (finset α)) or @coe (finset (finset α)) (set (finset α)) _ F, but how exactly do I use coe to get the inner type to be a set as well?

In particular, if I set parameter F : finset (finset α), then

• #check @coe (finset (finset α)) (set (finset α)) _ F works fine
• but #check @coe (finset (finset α)) (finset (set α)) _ F throws an error.

[AG]

Oh just got something that did it! Thank you again.

set.image (@coe (finset α) (set α) _) (F : set (finset α))

It turns out Lean can even go through the intermediary for you with

set.image (@coe (finset α) (set α) _) F