subtype of fintype

Stream: new members

[Shimon Cohen]

I have two related qustions
first:
why sub_bool is not rdeucable to fintype? there is a way to make every definition of somthing that reducable to fintype also reducable to fintype? how to prove the commented line - fintype (sub_bool)?

import data.fintype.basic
import data.fintype.card

open fintype

def sub_bool := {x : bool // x = true}
-- instance : fintype (sub_bool) := sorry
#check card ({x : bool // x = true})
#check card (sub_bool)

second:
In the following code even the subtype it self is not reduced to fintype.

import data.fintype.basic
import data.fintype.card

open fintype
variables (V : Type*) (n : ℕ)

def set_pow := {s : finset V // card s = n}
#check card ({s : finset V // card s = n})

It's looks like that subtype is reducable to fintype only if the predicate is decidable_pred, How to fix it?

[Eric Wieser]

Whenever you make a def foo := bar, Lean forgets (almost) everything it knows about bar when you work with foo

[Eric Wieser]

If you use @[reducible] def then it does not

[Shimon Cohen]

anything about this?
second:
In the following code even the subtype it self is not reduced to fintype.

import data.fintype.basic
import data.fintype.card

open fintype
variables (V : Type*) (n : ℕ)

def set_pow := {s : finset V // card s = n}
#check card ({s : finset V // card s = n})

It's looks like that subtype is reducable to fintype only if the predicate is decidable_pred, How to fix it?

[Adam Topaz]

Your set_pow is not finite in general... Do you want to assume that V is finite?

[Shimon Cohen]

adding [fintype V] to the variables not solve it

import data.fintype.basic
import data.fintype.card

open fintype

variables (V : Type*) [fintype V] (n : ℕ)
@[reducible] def set_pow := {s : finset V // card s = n}
#check card ({s : finset V // s.card = n})
#check card (set_pow V n)

[Eric Wieser]

import data.fintype.powerset

[Shimon Cohen]

what about this?
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/graphs.20edge_finset/near/363950165
there is a way to include (reduciable) constarins on the type? for example to change this ({s : finset V // s.card = n}) so s will have [decidable_eq] - In this way I coould request explicitly everything that I need insteed of dealing with how to make lean infer it implicity