fin succ proof coercing to `n + 1`

Stream: new members

[Yakov Pechersky]

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]

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]

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]

the code you posted doesn't say anything about %

[Kevin Buzzard]

Addition on fin uses % IIRC

[Johan Commelin]

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

[Johan Commelin]

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

[Jalex Stark]

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