如何在Lean中证明有限树至少存在一个度数为1的顶点？

问题背景 #

我正在导入combinatorics.simple_graph.connectivity库，尝试证明有限树中存在度数为1的顶点。

自定义度数为1的顶点定义 #

def vertex_degree_one (v : V) :=
  ∃! (u : V), u ≠ v ∧ G.adj v u

待证引理形式化 #

lemma tree_exists_vertexDegreeOne (v : V) (hg : G.is_tree) (hfin : fintype G.support) (vertices : v ∈ G.support)
          : (∃ w ∈ G.support, @vertex_degree_one V G w) := --where w is that vertex with degree 1

注：G.support是图G中构成边的顶点集合，且已被定义为有限类型。

证明思路与卡点 #

计划采用反证法：假设每个顶点的度数至少为2，从顶点v₀出发，因度数≥2可走到v₁，同理走到v₂且v₂≠v₀，且v_{i-1}≠v_{i+1}。由于顶点集合有限，最终必然会回到某个已访问过的顶点形成环，与树无环的性质矛盾。

目前卡在如何在Lean中定义这条能最终形成环的有限路径，Lean图论相关资料较少，希望得到思路指引。

解决思路指引 #

• 用递归序列构造路径：定义一个顶点序列seq : ℕ → V，起始点为v，对每个n ≥ 0，seq (n+1)取seq n的邻点且不等于seq (n-1)（n≥1时）。由于每个顶点度数≥2，可通过classical.choice保证这样的邻点存在。
• 利用鸽巢原理找重复顶点：因为G.support有限，序列中必然存在i < j使得seq i = seq j，此时从seq i到seq j的子序列构成环。
• 结合树的无环性质导出矛盾：树的定义包含无环性（is_tree.no_cycles），构造出的环直接与该性质冲突，从而推翻“所有顶点度数≥2”的假设，证明原命题成立。

实现细节提示 #

1. 开启classical模式处理选择问题，避免构造性证明的限制；
2. 使用fintype.card或鸽巢原理相关引理证明序列中存在重复顶点；
3. 将重复顶点间的序列转化为simple_graph.cycle类型，再调用树无环的引理完成矛盾推导。

内容的提问来源于stack exchange，提问作者Timothy