## Stream: new members

### Topic: fin succ proof coercing to n + 1

#### Yakov Pechersky (Jul 28 2020 at 19:46):

Is there some fin n coercion lemma that is missing? Or should I be using fin.cast_succ? In the following proof. I don't know how to remove % (n + 1) even if I have a hypothesis of i < n.

import tactic.linarith

example {n : ℕ} (i : fin n) : ((i : fin (n + 1)) + 1) = i.succ :=
begin
cases i with i h,
induction i with k hk,
simp [fin.succ],
cases n, linarith, refl,
cases n, linarith,
simp [fin.succ],
/-
case nat.succ, nat.succ
k n : ℕ,
hk : ∀ (h : k < n.succ), ↑⟨k, h⟩ + 1 = ⟨k, h⟩.succ,
h : k.succ < n.succ
⊢ ↑k + 1 + 1 = ⟨k.succ.succ, _⟩
-/
sorry,
end


#### Yakov Pechersky (Jul 28 2020 at 20:15):

Even this is confusing me. I'm unable to use h with hi.

example (i n : ℕ) (h : i < n) : (i : fin (n + 1)).val = i :=
begin
induction i with i hi,
simp,
sorry,
end


#### Kevin Buzzard (Jul 28 2020 at 20:48):

I don't think you need induction to prove this. There's bound to be a lemma in the library saying that if i<j then i%j=i, it will be called mod_lt or something

#### Jalex Stark (Jul 28 2020 at 20:50):

the code you posted doesn't say anything about %

#### Kevin Buzzard (Jul 28 2020 at 20:53):

Addition on fin uses % IIRC

#### Johan Commelin (Jul 28 2020 at 20:59):

I would avoid the cast from nat to fin (n+1). It isn't "nice" (imho)

#### Johan Commelin (Jul 28 2020 at 21:00):

But if you really need to, you can do it. The file zmod.lean will show you how to deal with it.

#### Jalex Stark (Jul 28 2020 at 21:03):

I had to guess that the lemma I wanted started with fin.coe_. I spent about a minute trying other things before making this guess.

example (i n : ℕ) (h : i < n) : (i : fin (n + 1)).val = i :=
begin
apply fin.coe_coe_of_lt, linarith,
end


Last updated: May 13 2021 at 18:26 UTC