Theorem: List.get_take (Fifteen/Data/List/Basic.lean)

State before:
α : Type u
β : Type v
l : List α
n i : Nat
hi : i < length (take n l)
hi' : i < length l
⊢ get (take n l) { val := i, isLt := hi } = get l { val := i, isLt := hi' }
Tactic:
rw [get_of_eq (l.take_append_drop n).symm, get_append_left]
State after:
no goals