## Stream: new members

### Topic: Coercing "nested" types

#### AG (Jan 11 2022 at 04:39):

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 (Jan 11 2022 at 07:01):

@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 (Jan 12 2022 at 04:46):

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 (Jan 12 2022 at 04:59):

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


Last updated: Dec 20 2023 at 11:08 UTC