Theorem: List.getI_map_range (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : 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
Tactic:
simpa using List.getI_eq_get ((List.range n).map f) (n := i) (by simpa using h)
State after:
no goals

State before:
α✝ : Type u
inst✝⁴ : DecidableEq α✝
β : Type v
inst✝³ : DecidableEq β
α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
i n : ℕ
inst✝ : Inhabited α
f : ℕ → α
h : i < n
⊢ i < (map f (range n)).length
Tactic:
simpa using h
State after:
no goals