Lean not unfolding definition

Stream: new members

[Vivek Rajesh Joshi]

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

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

@[simp] theorem Vector.mem_cons {a b : α} {l : Vector α n} : a ∈ (Vector.cons b l) ↔ a = b ∨ a ∈ l := by
  constructor
  intro h

Lean refuses to unfold Vector.Mem at h no matter what tactic I use. What do I do?

[Kyle Miller]

It can be a little overreaching, but one tactic you can use (from mathlib) is unfold_projs, which is for unfolding these sorts of instances.

[Kyle Miller]

The normal way to do this though, without tactics, is to define a _def theorem for the instance.

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

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

theorem Vector.mem_def (v : Vector α n) : a ∈ v ↔ v.toList.Mem a := Iff.rfl

Then you can rewrite with Vector.mem_def.

[Vivek Rajesh Joshi]

Got it, thanks!