Some basic trouble with Fin n

Stream: Is there code for X?

[Dhyan Aranha]

I'm trying to prove the following basic statement whose slogan could be " if I pad a finite sum with zeros nothing changes"

--Extend by 0
def ext0 {A : Type*} [CommRing A] (  m n : ℕ) (g : Fin m → A) : Fin n → A := fun i =>
  if h : i.val < m then g ⟨i.val, h⟩ else 0

lemma Pad_0 {A: Type*} [CommRing A] (m n :ℕ) (g : Fin m → A) (h : m ≤ n) :
  ∑ i : Fin m, g i = ∑ i : Fin n, ext0 m n g i

However my code is getting long and convoluted which makes me suspect that I'm going about this all wrong. (In general I struggle with arguments about summing over Fin n :P)

What I'm trying to do (let me try and spare you the headache of copy-pasting my crappy code):

1) First make a bijection trunc_map n m of Fin m with the subtype trunc n m := { x : Fin n // x.val < m} of Fin n.

2) Second use this bijection to try use apply Finset.sum_bij, to get something of the form

∑ i : Fin m, g i = ∑ i : trunc n m, g (trunc_map n m i)

3) Now I need to find a way to relate ∑ i : trunc n m, g (trunc_map n m i) to ∑ i : Fin n, ext0 m n g i here I get pretty stuck. Probably I want to use something like  Finset.sum_subset, but trunc n m is a subtype and not a subset and I also have to somehow reconcile g (trunc_map n m ) with ext0 m n g which are two functions defined on different types!

Any comments and advice would be greatly appreciated!

[Ruben Van de Velde]

Summing over a Finset Nat is probably easier

[Eric Wieser]

lemma Pad_0 {A: Type*} [CommRing A] (m n :ℕ) (g : Fin m → A) (h : m ≤ n) :
    ∑ i : Fin m, g i = ∑ i : Fin n, ext0 m n g i := by
  obtain ⟨k, rfl⟩ := exists_add_of_le h
  rw [← finSumFinEquiv.sum_comp]
  simp [ext0]

[Dhyan Aranha]

Thanks Eric!