α : Type u_1
i : Nat
l : List α
h : length l ≤ i
this : take i l ++ drop i l = l
⊢ take i l = l
α : Type u_1
i : Nat
l : List α
h : length l ≤ i
⊢ take i l = l
have := take_append_drop i l
α : Type u_1
i : Nat
l : List α
h : length l ≤ i
this : take i l = l
⊢ take i l = l
α : Type u_1
i : Nat
l : List α
h : length l ≤ i
this : take i l ++ drop i l = l
⊢ take i l = l
rw [drop_length_le h, append_nil] at this
no goals
α : Type u_1
i : Nat
l : List α
h : length l ≤ i
this : take i l = l
⊢ take i l = l
exact this