Formalizing Possibly Infinite Trees of Bounded Degree

As Lean does not sup­port coin­duc­tive types di­rect­ly, for­mal­iz­ing in­fi­nite lists and in­fi­nite trees re­quires some "cre­ativ­i­ty". As a byprod­uct of one of our on­go­ing works, we for­mal­ized pos­si­bly in­fi­nite trees of bound­ed de­gree in Lean. In this work­shop, we will re­pro­duce this idea and present the de­f­i­n­i­tion from scratch (even with­out math­lib). We will work to­wards show­ing a spe­cial case of König's Lem­ma: if each branch in such a tree is fi­nite, then there are only fi­nite­ly many branch­es.