As Lean does not support coinductive types directly, formalizing infinite lists and infinite trees requires some "creativity". As a byproduct of one of our ongoing works, we formalized possibly infinite trees of bounded degree in Lean. In this workshop, we will reproduce this idea and present the definition from scratch (even without mathlib). We will work towards showing a special case of König's Lemma: if each branch in such a tree is finite, then there are only finitely many branches.