fin coe proof

Stream: new members

[Patrick Thomas]

Is there a way forward here?

def function.update_fin
    {α β : Type}
    [decidable_eq α]
    (σ : α → β) :
    Π (n : ℕ), (fin n → α) → (fin n → β) → (α → β)
| 0 _ _ := σ
| (n + 1) f g :=
    function.update
        (function.update_fin n (fun (i : fin n), (f i)) (fun (i : fin n), (g i)))
        (f n) (g n)

example
    {α β : Type}
    [decidable_eq α]
    (σ : α → β)
    (n : ℕ)
    (xs : fin n → α)
    (ys : fin n → β)
    (x : α)
    (h1 : ∀ (i : fin n), x ≠ xs i) :
    function.update_fin σ n xs ys x = σ x :=
begin
    induction n,
    case nat.zero
  {
        unfold function.update_fin
    },
  case nat.succ : n ih
  {
        unfold function.update_fin,
        specialize h1 ↑n,
        simp only [function.update_noteq h1],
        apply ih (fun (i : fin n), xs (↑i)) (fun (i : fin n), ys (↑i)),
        intro i,
        sorry
    },
end