## Stream: new members

### Topic: Help with proof on list membership

#### yokatta (Jul 03 2023 at 03:27):

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 (Jul 03 2023 at 09:01):

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 (Jul 03 2023 at 09:07):

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.

Last updated: Dec 20 2023 at 11:08 UTC