How do I map a list along with proof of membership?

Stream: new members

[Marko Grdinić]

def list_dice := [1,2,3,4,5,6]
def list_claim := [(1,2), (1,3), (1,4), (1,5), (1,6), (1,1), (2,2), (2,3), (2,4), (2,5), (2,6), (2,1)]

inductive Action
| Claim (claim : {n // n ∈ list_claim}) : Action
| Dudo : Action

def actions : list Action :=
    let claims : list Action :=
        list_claim.map (fun x,
            Action.Claim ⟨ x, sorry ⟩
            ) in
    Action.Dudo :: claims

I've defined an inductive type like this and now I also want to turn it into a list. That having said, I have no idea how to provide the proof of membership. The x is opaque, so I do not have the necessary information to prove this.

How should I approach this?

[Marc Huisinga]

you can attach the proof of membership before mapping https://github.com/leanprover-community/mathlib/blob/24dd80b0db5f2adbefd3b00709b4a445fc18fb9b/src/data/list/basic.lean#L1720
(edited to provide permalink ;))

[Marko Grdinić]

Thank you.