List.get?_eq_get and List.get!_eq_get

Stream: std4

[Jakob von Raumer]

List.get?_eq_get and List.get!_eq_get are copies of the exact same lemma, the latter one doesn't actually refer to get!, but the best way to prove the actual List.get!_eq_get would be to shift getD_eq_get from mathlib4 to std4, how do I orchestrate that? First add it to std4?

[François G. Dorais]

Yes, please! The mathlib fix is trivial for such a small change. It's just a regular part of the bump merge so no worries.

[Jakob von Raumer]

Can someone give me (@javra) access rights to make a PR? @Mario Carneiro ?

[Alex J. Best]

Std often uses the more traditional github model of making PRs from forks btw (though who knows mario may give you access anyway :wink:)

[Jakob von Raumer]

Ah, k, thanks