simpa using List.getI_eq_get ((List.range n).map f) (n := i) (by simpa using h)
α✝ : Type u
inst✝⁴ : DecidableEq α✝
β : Type v
inst✝³ : DecidableEq β
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
i n : ℕ
inst✝ : Inhabited α
f : ℕ → α
h : i < n
⊢ (map f (range n)).getI i = f i
no goals