How to synthesize Vector Membership

Stream: new members

[Vivek Rajesh Joshi]

Why is lean not able to synthesize Vector membership here despite being spoonfed?

import Mathlib.Data.Matrix.Notation

variable (F : Type) [Field F]

def Vector.Mem (a : α) : Vector α n → Prop := fun v => v.toList.Mem a

instance : Membership α (Vector α n) where
  mem := Vector.Mem

#synth Membership F (Vector F 2)

#eval 1 ∈ [1,2]
#eval 1 ∈ (⟨[1,2],rfl⟩ : Vector Nat 2)

[Bbbbbbbbba]

#check (⟨[1,2],rfl⟩ : Vector Nat 2) does not actually give Vector Nat 2 but { l // l.length = 2 }, so it seems that Vector Nat 2 got evaluated somehow

[Vivek Rajesh Joshi]

Okay, why does that happen then, despite explicitly giving Lean the type? And how to circumvent it?

[Bbbbbbbbba]

This seems to circumvent the current problem, although Lean now complains that it doesn't know how to decide 1 ∈ v.

def v : Vector Nat 2 := ⟨[1,2],rfl⟩
#eval 1 ∈ v

[Vivek Rajesh Joshi]

I need the synthesis to prove this theorem:

theorem Vector.eq_of_mem_singleton {a b : F} (h : let v := (⟨[b],rfl⟩ : Vector F 1); a ∈ v) : a = b := by sorry

Looks like it's not working even with a local definition

[Bbbbbbbbba]

theorem Vector.eq_of_mem_singleton {a b : F} (h : let v : Vector F 1 := ⟨[b],rfl⟩; a ∈ v) : a = b := by sorry

[Vivek Rajesh Joshi]

That works, thanks!