list.nth_le and list.nth

Stream: Is there code for X?

[Martin Dvořák]

I cannot find the following lemma in mathlib. Have I been searching wrong? It looks so basic!

lemma nth__eq__nth___of___nth_le__eq__nth_eq {α : Type} {x y : list α}
    {i : ℕ} {i_lt_len_x : i < x.length} {i_lt_len_y : i < y.length}
    (x_ith_le__eq__y_ith_le : x.nth_le i i_lt_len_x = y.nth_le i i_lt_len_y) :
  x.nth i = y.nth i :=
begin
  sorry
end

[Junyan Xu]

import data.list.basic

lemma nth__eq__nth___of___nth_le__eq__nth_eq {α : Type} {x y : list α}
    {i : ℕ} {i_lt_len_x : i < x.length} {i_lt_len_y : i < y.length}
    (x_ith_le__eq__y_ith_le : x.nth_le i i_lt_len_x = y.nth_le i i_lt_len_y) :
  x.nth i = y.nth i :=
by rw [list.nth_le_nth i_lt_len_x, list.nth_le_nth i_lt_len_y, x_ith_le__eq__y_ith_le]

[Scott Morrison]

(Feel free to PR; it would be fine in mathlib.)

[Martin Dvořák]

Do you want to replace all sequences of underscores by a single underscore?

[Scott Morrison]

I guess there's no need to have the same i: you could conclude x.nth i = y.nth j with the same proof.

[Scott Morrison]

The statement should probably be written

lemma nth_eq_nth_of_nth_le_eq_nth_le {α : Type*} {x y : list α}
  {i : ℕ} {ix : i < x.length} {iy : i < y.length} (h : x.nth_le i ix = y.nth_le i iy) :
  x.nth i = y.nth i :=

[Scott Morrison]

(unless you do the i ≠ j generalisation...)

[Scott Morrison]

You can even omit the types of ix and iy entirely, although some might argue that is getting obfuscatory, rather than just golfing. :-)

[Martin Dvořák]

I won't omit the types.

[Martin Dvořák]

lemma nth_eq_nth_of_nth_le_eq_nth_le {α : Type*} {x y : list α}
  {i j : ℕ} {ix : i < x.length} {jy : j < y.length} (h : x.nth_le i ix = y.nth_le j jy) :
  x.nth i = y.nth j :=
by  rw [list.nth_le_nth ix, list.nth_le_nth jy, h]

works.

[Martin Dvořák]

https://github.com/leanprover-community/mathlib/pull/15688

[Scott Morrison]

Left a comment.

[Martin Dvořák]

Sorry for abusing this thread... Is this error due to something in my commits?
https://github.com/leanprover-community/mathlib/runs/7518315148?check_suite_focus=true

[Eric Wieser]

No, you should just restart the job

[Eric Wieser]

That has been happening quite a lot recently I think

[Martin Dvořák]

The job succeeded :-).

[Martin Dvořák]

Will somebody review my PR please?
https://github.com/leanprover-community/mathlib/pull/15688

[Alex J. Best]

FYI: The PR #queue is currently very long >100 PRs waiting, that's not to say that short PRs won't be reviewed more quickly, but having a maintainer look at it in less than 4 hours (when you added the label) is somewhat unlikely these days

[Martin Dvořák]

Sorry for my impatience. I was just afraid it would fall into oblivion, as a few of my older PRs did. I'll wait.