Formalization of Cayleys theorem

Stream: mathlib4

[TanteMariane]

I'm a lean-beginner, trying to formalize the recursion proof of Cayleys theorem for the number of labeled trees on n vertices. The proof shows a more general statement about the number of labeled forests "rooted" in a fixed vertex set roots of size k, lets call this set of forests A. Rooted means that exactly one element of roots is in each connected component of the forest.

def is_forest_with_roots_in_set {α : Type} [Fintype α] (G : SimpleGraph α)
  (roots : Finset α) : Prop :=
  G.IsAcyclic ∧ ConnectedComponent.Represents
    roots (Set.univ : Set G.ConnectedComponent)

def forest_set {α : Type} [Fintype α]
  (roots : Finset α) := {G | is_forest_with_roots_in_set G roots}

I defined the function f, that takes a SimpleGraph and just deletes a fixed vertex w.

def f (G : SimpleGraph α) : SimpleGraph {v | v ≠ w} :=
  G.induce {v | v ≠ w}

lemma f_inj (G G' : SimpleGraph α) :
  (f (w := w) G = f G' ∧ ∀ u : α, (G.Adj u w ↔ G'.Adj u w)) → G = G' := by

I showed that f maps a forest rooted in roots, to the set of all forests that are rooted in

$$roots\setminus \{w\} \cup \{\text{neighbors w}\}$$

Lets call this set B_{neighbors w}.

noncomputable def new_roots (roots : Finset α) (G : SimpleGraph α) :
  Finset {v | v ≠ w} := (roots ∪ G.neighborFinset w).subtype (fun v => v ≠ w)

theorem f_maps_to {hw : w ∈ roots} (G : SimpleGraph α) (hG : G ∈ forest_set roots) :
  f G ∈ forest_set (new_roots (w := w) roots G) := by ...

By induction, we know the size of all the B-sets. And we see that to "build" the set A, we first choose the neighbors of w, and then choose a forest from B_{neighbors w}.

Now I need to somehow state a bijection that formalizes this. I tried to do it with a Sigma-type like

def valid_neighbor_sets_i (i : ℕ) (w : α) (roots : Finset α) : Type :=
  {N : Finset {v | v ≠ w} // Disjoint N (coer roots) ∧ N.card = i}

Σ N : valid_neighbor_sets_i i w roots, forest_set (N.1 ∪ (coer roots))

where the second components depends on the first component (the choice of the neighbors).
This was messy, and I got stuck when trying to destruct this symbol ≍ (I looked it up and it is an HEq heterogeneous equality).
So I wanted to ask here if someone knows a clean way to do this.
Another idea is that I fix a valid_neighbor_set and show that f induces a bijection BETWEEN the forests of A, where the neighbor-set of w is equal to valid_neighbor_set, AND the set B_{valid_neighbor_set}.

[Notification Bot]

This topic was moved here from #lean4 > Formalization of Cayleys theorem by Michael Rothgang.

[Michael Rothgang]

Hi and welcome to zulip! I moved your topic to the mathlib4 channel, where it is much more likely to be read by the right people. #lean4 is for questions about the Lean prover; this channel is better for questions about formalising mathematics in it.