convert (Finset.range n).finite_toSet.biUnion fun i _ ↦ finite_length_eq α i
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n}.Finite
case h.e'_2
α : Type u_1
inst✝ : Finite α
n : ℕ
⊢ {l | l.length < n} = ⋃ i ∈ ↑(Finset.range n), {l | l.length = i}