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

State before:
α : Type u
β : Type v
γ : Type w
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