no goals
ι : Type ?u.197224
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
n : ℕ
l : List α
h : n < length l
⊢ dropLast (take n l) = take (pred n) l
simp [dropLast_eq_take, min_eq_left_of_lt h, take_take, pred_le]