## Stream: new members

### Topic: fin coe struggle

#### Anatole Dedecker (Aug 24 2020 at 07:31):

Okay so I must be missing something but I can't find how to prove this :sad:

import tactic

lemma foo (n : ℕ) : ((n : fin n.succ) : ℕ) = n :=
begin
sorry,
end


#### Kevin Buzzard (Aug 24 2020 at 07:35):

What's the definition of the coercion? If this proof is not refl then I think it says that you shouldn't be using the coercion

#### Kevin Buzzard (Aug 24 2020 at 07:36):

I mean the coercion from fin to fin. There are perfectly well defined maps between fins which will behave very well, but recently people have been using some far less well behaved maps eg +1 and then complaining that everything is horrible because there are secret %(n+1) operators involved

#### Shing Tak Lam (Aug 24 2020 at 07:38):

import tactic

lemma foo (n : ℕ) : ((n : fin n.succ) : ℕ) = n :=
fin.coe_coe_of_lt (nat.lt_succ_self _)


#### Anatole Dedecker (Aug 24 2020 at 07:38):

Thanks ! I should have searched better I guess...

#### Anatole Dedecker (Aug 24 2020 at 07:40):

Kevin Buzzard said:

I mean the coercion from fin to fin. There are perfectly well defined maps between fins which will behave very well, but recently people have been using some far less well behaved maps eg +1 and then complaining that everything is horrible because there are secret %(n+1) operators involved

I know these coercions are trickier than most other (e.g norm_cast can't deal with them), but this example should be true anyway (and it is indeed)

#### Kyle Miller (Aug 24 2020 at 07:41):

Kevin Buzzard said:

What's the definition of the coercion?

It looks like it's fin.val (nat.cast n), with some type hinting in there somewhere.

#### Kyle Miller (Aug 24 2020 at 07:43):

That means foo is n % (n + 1) = n. (Not definitionally, though.)

#### Kevin Buzzard (Aug 24 2020 at 07:49):

Any map that uses % somehow is going to be hard to work with. None of the natural maps from fin n to fin (n+1) use %

#### Reid Barton (Aug 24 2020 at 12:31):

It's probably better to use fin.last n instead of whatever introduced (n : fin n.succ).

Last updated: May 11 2021 at 00:31 UTC