# Zulip Chat Archive

## Stream: new members

### Topic: Using list.fin_range

#### Zhangir Azerbayev (Aug 05 2020 at 19:24):

I need to prove the following lemma.

```
lemma {q : nat} : list.fin_range q.succ = 0 :: list.map fin.succ (list.fin_range q)
```

There are very few lemmas about `list.fin_range`

, so it seems inevitable that any proof would have to work with the underlying `list.pmap`

. Induction on `q`

hasn't worked for me because that approach requires splitting the last element of a list from the rest. I've also tried hitting the goal with `ext`

but that hasn't given me anything I can figure out how to work with. Does anyone have suggestions for how to proceed?

#### Kevin Buzzard (Aug 05 2020 at 22:32):

I thought

```
lemma list.eq_of_nth_le_eq (α : Type) (A B : list α) (n : ℕ) (hAn : n = A.length) (hBn : n = B.length)
(h : ∀ (i : ℕ) (hi : i < n), A.nth_le i (hAn ▸ hi) = B.nth_le i (hBn ▸ hi)) : A = B :=
begin
sorry
end
```

might help, but I didn't prove that and even with it I couldn't make much progress. I'm not great at this stuff. @Mario Carneiro ?

#### Mario Carneiro (Aug 05 2020 at 22:35):

that looks like an extensionality lemma to me

#### Mario Carneiro (Aug 05 2020 at 22:35):

is there anything like `list.nth_le_ext`

?

#### Mario Carneiro (Aug 05 2020 at 22:36):

`list.ext_le`

#### Mario Carneiro (Aug 05 2020 at 22:38):

```
lemma list.eq_of_nth_le_eq (α : Type) (A B : list α) (n : ℕ) (hAn : n = A.length) (hBn : n = B.length)
(h : ∀ (i : ℕ) (hi : i < n), A.nth_le i (hAn ▸ hi) = B.nth_le i (hBn ▸ hi)) : A = B :=
list.ext_le (hAn.symm.trans hBn) $ λ i h1 h2, h i (by rwa hAn)
```

#### Kevin Buzzard (Aug 05 2020 at 22:39):

only problem is that it doesn't help ;-)

#### Mario Carneiro (Aug 05 2020 at 22:50):

```
namespace list
theorem pmap_map {α β γ} {p : β → Prop} (g : ∀ b, p b → γ) (f : α → β)
(l H) : pmap g (map f l) H = pmap (λ a h, g (f a) h) l (λ a h, H _ (mem_map_of_mem _ h)) :=
by induction l; [refl, simp only [*, pmap, map]]; split; refl
example {q : nat} : fin_range q.succ = 0 :: map fin.succ (fin_range q) :=
begin
unfold fin_range,
rw [map_pmap],
simp_rw [range_succ_eq_map],
rw [pmap],
congr' 1,
rw pmap_map,
apply pmap_congr,
intros, refl,
end
end list
```

#### Reid Barton (Aug 05 2020 at 22:50):

I think a better strategy should be to use the fact that `list.map fin.val`

is injective and use `range_succ_eq_map`

#### Reid Barton (Aug 05 2020 at 22:50):

oops too slow

#### Zhangir Azerbayev (Aug 06 2020 at 00:20):

Thank you @Mario Carneiro ! With that we have a sorry-free proof that the canonical map from $M^q$ into $\Lambda (M)$ is multilinear.

Last updated: May 08 2021 at 09:11 UTC