Prove List.map conserves length

Stream: lean4

[Alex Sweeney]

I'm trying to prove that List.map conserves the length of the list, and I actually managed to prove that as a lemma, but I'm stuck on what feels like should be the easy part.

lemma map_length {α β : Type} (f : α → β) (l : List α) : l.length = (l.map f).length :=
  l.recOn
    (by rfl)
    (by simp [List.map])

def Board.fromNats (cells : List Nat) (h : cells.length = 81) : Board :=
  let map_fn := (fun n => CellValue.ofNat n)
  ⟨cells.map map_fn, by sorry⟩ -- Prove List.length cells.map (...) = 81

How do I use my lemma to prove List.length (cells.map map_fn) = 81?

[Marcus Rossel]

def Board.fromNats (cells : List Nat) (h : cells.length = 81) : Board :=
  let map_fn := (fun n => CellValue.ofNat n)
  have : List.length (cells.map map_fn) = 81 := h ▸ (map_length map_fn cells).symm
  ⟨cells.map map_fn, this⟩

Next time please try to post a #mwe.