Order reversing bijection on fin n

Stream: new members

[Antoine Labelle]

This may be a stupid question, but I was wondering what was the simplest way to denote the element n-1-i given i : fin n. If I just write it as such Lean complains because n is of type nat so it doesn't know how to subtract something from it.
I noticed that Lean accepts ⟨n-1-i, _⟩, but adds n-1-i<n as a new goal. That seems to work but feels too convoluted but something that should be simple.
Is the order-reversing bijection i ↦ n-1-i on fin n already defined somewhere, and if not what is the best way to work with it?

[Yakov Pechersky]

fin.last n - i

[Antoine Labelle]

Thanks!

[Eric Wieser]

Or I think docs#equiv.sub_left (fin.last n) if you want the bijection

[Antoine Labelle]

equiv.sub_left is protected, can I still use it? Lean gives me an "unknown identifier" message even if I import data.equiv.mul_add.

[Alex J. Best]

Yes, check out attr#protected, it should still be usable, just you always need to use its full name. If you post a full example we can try and see what's wrong.

[Antoine Labelle]

Here is my code

import data.finset.sort
import data.equiv.mul_add

open_locale big_operators

theorem imo1994 (n : ℕ) (m : ℕ) (A : finset ℕ) (hm : A.card = m + 1)
  (hrange : ∀ a ∈ A, a ≥ 1 ∧ a ≤ n) (hadd : ∀ a b ∈ A, a + b ≤ n → a + b ∈ A) :
  (n+1)/2 ≤ (∑ x in A, x)/(m+1) :=
begin
  have a := finset.order_emb_of_fin A hm,
  set flip := equiv.sub_left (fin.last m),
end

[Alex J. Best]

I don't see any errors with this in the web editor (https://leanprover-community.github.io/lean-web-editor/#code=import%20data.equiv.mul_add%0Aimport%20algebra.big_operators%0Aimport%20data.finset.sort%0A%0Aopen_locale%20big_operators%0A%0Atheorem%20imo1994%20%28n%20%3A%20%E2%84%95%29%20%28m%20%3A%20%E2%84%95%29%20%28A%20%3A%20finset%20%E2%84%95%29%20%28hm%20%3A%20A.card%20%3D%20m%20%2B%201%29%0A%20%20%28hrange%20%3A%20%E2%88%80%20a%20%E2%88%88%20A%2C%20a%20%E2%89%A5%201%20%E2%88%A7%20a%20%E2%89%A4%20n%29%20%28hadd%20%3A%20%E2%88%80%20a%20b%20%E2%88%88%20A%2C%20a%20%2B%20b%20%E2%89%A4%20n%20%E2%86%92%20a%20%2B%20b%20%E2%88%88%20A%29%20%3A%0A%20%20%28n%2B1%29%2F2%20%E2%89%A4%20%28%E2%88%91%20x%20in%20A%2C%20x%29%2F%28m%2B1%29%20%3A%3D%0Abegin%0A%20%20have%20a%20%3A%3D%20finset.order_emb_of_fin%20A%20hm%2C%0A%20%20set%20flip%20%3A%3D%20equiv.sub_left%20%28fin.last%20m%29%2C%0A%20%20%0Aend)

[Alex J. Best]

You also need a newline after the first set of backticks, like so

```
import blah

lemma foo := trivial
```

[Antoine Labelle]

Weird, do you have any idea why it wouldn't work for me in VScode? Could I have problems with my installation of mathlib?

[Alex J. Best]

Yes, that could be the case, when did you install lean/mathlib? Maybe it just needs an update?

[Antoine Labelle]

Oh yeah, an upgrade worked :sweat_smile: . Thanks for the help!