Is there a better way to reason about List.ofFn?

Stream: new members

[Ching-Tsun Chou]

Is there a better way to prove the following trivial result? I am not happy with what I came up with, especially the the stupid calc sequence. All I wanted to do was to somehow unfold an equality between two lambda expressions into a ∀-quantified equality, but I couldn't figure out a better way to do that.

example {X : Type*} {xs xs' : ℕ → X} {m n n' : ℕ}
    (h : List.ofFn (fun k : Fin (m - n) ↦ xs (k + n)) = List.ofFn (fun k : Fin n' ↦ xs' k)) :
    n' = m - n ∧ ∀ k < m - n, xs' k = xs (k + n) := by
  simp [List.ofFn_inj'] at h
  obtain ⟨rfl, h2⟩ := h
  simp at h2
  simp ; intro k h_k
  calc _ = (fun k : Fin (m - n) ↦ xs' ↑k) ⟨k, h_k⟩ := by simp
       _ = (fun k : Fin (m - n) ↦ xs (↑k + n)) ⟨k, h_k⟩ := by rw [h2]
       _ = _ := by simp

[Aaron Liu]

import Mathlib

example {X : Type*} {xs xs' : ℕ → X} {m n n' : ℕ}
    (h : List.ofFn (fun k : Fin (m - n) ↦ xs (k + n)) = List.ofFn (fun k : Fin n' ↦ xs' k)) :
    n' = m - n ∧ ∀ k < m - n, xs' k = xs (k + n) := by
  symm at h
  rw [List.ofFn_inj', Sigma.mk.injEq] at h
  obtain ⟨rfl, h2⟩ := h
  rw [heq_eq_eq, funext_iff] at h2
  simpa [Fin.forall_iff] using h2

[Ching-Tsun Chou]

Thanks! funext_iff is what I needed. I knew there must be a result like that in mathlib but could not find it. simp? only found heq_eq_eq.