α : Type u
m : ℕ
f : Fin m → α
⊢ ofFn f = ofFn fun i => f (↑(Fin.cast (_ : m = m)) i)
α : Type u
m n : ℕ
h : m = n
f : Fin m → α
⊢ ofFn f = ofFn fun i => f (↑(Fin.cast (_ : n = m)) i)
subst h
no goals
α : Type u
m : ℕ
f : Fin m → α
⊢ ofFn f = ofFn fun i => f (↑(Fin.cast (_ : m = m)) i)
simp_rw [Fin.cast_refl, OrderIso.refl_apply]