snoc and cast

Stream: Is there code for X?

[Wrenna Robson]

Can anyone find a neat proof of this?

[Wrenna Robson]

import Mathlib.Data.Fin.Tuple.Basic

open Fin

theorem snoc_cast (bs : Fin k → β) (b : β) (h : k' + 1 = k + 1) (i : Fin (k' + 1)) :
    snoc (α := fun _ => β) bs b (cast h i) =
    snoc (α := fun _ => β) (fun i => bs (cast (Nat.succ_inj.mp h) i)) b i := sorry

[Yaël Dillies]

#mwe ?

[Wrenna Robson]

Uh, this is my mwe?

[Wrenna Robson]

I guess it lacks the imports.

[Wrenna Robson]

@Yaël Dillies is that better?

[Wrenna Robson]

Even more minimally, there's this:

theorem foobar (bs : Fin k → β) (h : k' = k) (f : (k : Nat) → (Fin k → β) → α) :
    f k' (fun i => bs (Fin.cast h i)) = f k bs := sorry

Not sure that needs any imports at all.

[Kevin Buzzard]

Wrenna Robson said:

Uh, this is my mwe?

It doesn't work in the web editor for me or locally. I was going to see if aesop worked but I can't get the code running.

[Wrenna Robson]

Oh, namespaces. There we go?

[Markus Himmel]

This seems to work:

import Mathlib.Data.Fin.Tuple.Basic

open Fin

theorem snoc_cast (bs : Fin k → β) (b : β) (h : k' + 1 = k + 1) (i : Fin (k' + 1)) :
    snoc (α := fun _ => β) bs b (cast h i) =
    snoc (α := fun _ => β) (fun i => bs (cast (Nat.succ_inj.mp h) i)) b i := by
  cases h
  simp

[Wrenna Robson]

theorem foobar (bs : Fin k → β) (h : k' = k) (f : (k : Nat) → (Fin k → β) → α) :
    f k' (fun i => bs (Fin.cast h i)) = f k bs := by aesop

[Wrenna Robson]

Didn't know you could do that with equalities.