Help with proof on list membership

Stream: new members

[yokatta]

I'm trying to complete the following proof:

import Mathlib.Data.List.Basic

theorem foo {α : Type} {as : List α} {ms : List { a // a ∈ as }} (nodup : List.Nodup ms) : ms.length ≤ as.length := by
  cases nodup with
  | nil => simp only [List.length_nil, zero_le]
  | cons p nodup =>
      rename_i m ms
      rw [List.length_cons]
      have h := foo nodup

      show ms.length < as.length
      sorry

but am not sure how to proceed. Intuitively, I can convince myself by imagining a mapping between the two lists where the map from ms to as has to be injective, but it seems like there should be an easier way of proving it?

[Martin Dvořák]

I don't know how to finish your proof, but if I were working on it, I would start as follows:

lemma qux {α : Type} {ms : List α} (nodup : List.Nodup ms) {as : List α} (subt : ∀ x ∈ ms, x ∈ as) :
  ms.length ≤ as.length :=
by
  revert as
  induction ms with
  | nil => simp
  | cons m ms ih =>
      intros as hyp
      -- apply `ih` to the list `as` without the element `m`
      sorry

[Martin Dvořák]

What I want to say is that I'd perform induction on ms but I cannot have as fixed. I want to work with ∀ as in the induction step.