List.append error on cases

Stream: lean4

[Kevin Buzzard]

inductive Mem (a : α) : List α → Prop where
  | intro (as bs) : Mem a (as ++ (a :: bs))

infix:50 " ∈ " => Mem

theorem not_mem_nil (a : α) : ¬ (a ∈ []) := by
  intro h
  cases h
/-
dependent elimination failed, failed to solve equation
  [] = List.reverseAux (List.reverse as✝) (a :: bs✝)
-/

I cannot prove this theorem! Whatever I try either doesn't work at all or gives me this surprising message about List.reverse. Have I just made a dumb error? This is from exercise 5 of the Ullrich/von Raumer KIT course.

[Kevin Buzzard]

Aah! Much less surprising now I've looked up the definition of List.append:

protected def append (as bs : List α) : List α :=
  reverseAux as.reverse bs

Lean is taking things apart too much -- I just want to be left with as and bs with [] = as ++ (a :: bs) and I'll take it from there, but I can't get it to stop unfolding. I've tried tactic mode and term mode but I can't get it :-/

[Kevin Buzzard]

Aah -- I now realise that I have the same problem in Lean 3 so probably this isn't a Lean 4 issue at all.

[Kevin Buzzard]

OK got it: I need to make other API first. This is indeed nothing to do with Lean 4.

theorem Mem_iff (a : α) (L : List α) :
  a ∈ L ↔ ∃ as bs, L = as ++ (a :: bs) :=
⟨λ ⟨as, bs⟩ => ⟨as, bs, rfl⟩, λ ⟨as, bs, hL⟩ => hL.symm ▸ Mem.intro as bs⟩

theorem not_mem_nil (a : α) : ¬ (a ∈ []) := by
  rw [Mem_iff]
  intro ⟨as, bs, h⟩
  ...