Prove isEmpty lemma

Stream: new members

[Mikaël Mayer]

I can't get to prove this simple lemma. As you guess, I'm new to Lean. And ChatGPT nor claude are helpful

abbrev Map (α β : Type) := List (α × β)

namespace Map

def isEmpty {α β : Type} : Map α β → Bool
  | []      => true
  | _ :: _  => false

theorem isEmpty_append {α β : Type} (a b : Map α β) :
    isEmpty (a ++ b) = isEmpty a && isEmpty b := by
  cases a <;> simp [isEmpty]

end Map

I tried all kinds of proofs there, but I'm always stuck with decide things and rewrites that are wrong. Help appreciated.

[Matthew Jasper]

You're missing parentheses, the conclusion should be

isEmpty (a ++ b) = (isEmpty a && isEmpty b)

[Robin Arnez]

You can hover over the expression to see how their precedence works out

[Robin Arnez]

Screenshot 2025-07-29 141046.png