Effort of formalizing simple Lemma on Perfect Matchings?

Stream: graph theory

[Mario Krenn]

Hi! Is it possible to estimate the effort/time it would take someone with good Lean experience to formalize certain proofs? I am specifically interested to know how long you guess it would take to formalize a statement on perfect matchings:

Let's consider (not necessary simple) graphs with only disjoint perfect matchings (i.e. every edge only appears in at most one of the perfect matchings).

Then, if such a graph has 4 vertices, it can have maximally 3 perfect matchings (K_4 is an example). If it has more than 4 vertices, it can have maximally 2 perfect matchings (C_{2n} is an example).

The proof seems rather straight forward, see: https://mathoverflow.net/questions/267002/graphs-with-only-disjoint-perfect-matchings)

Could you give a rough estimation how time it would take an good lean user (for example, one of Kevin's trained undergrads) to formalize the proof of this statement? Thanks a lot, and thanks for your exciting works :)
(i mentioned this statement before, @Kyle Miller actually started to formalize the statement: https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/matchings/near/243576742)

[Kyle Miller]

#8737 has things like paths, cycles, and hamiltonian cycles. It also has things for splitting paths and cycles. There isn't anything relating matchings and cycles yet, though.

It seems plausible to me that the theorem could be formalized within a few weeks. (It also seems plausible that there are people that can do it within a couple days.)

[Kyle Miller]

Manipulating these fragments of paths seems like it could be rather tedious, or at least a simpler manipulation was in my attempt at this lemma (see also its supporting lemma immediately above it)

[Yaël Dillies]

The result itself doesn't sound too hard, but we're missing a shear amount of graph theory basics.

[Kyle Miller]

@Yaël Dillies When you mention that graph theory basics are missing, are you meaning things that would cause trouble for proving this theorem about disjoint perfect matchings? or is it just a general comment?

I could be wrong, but it seems like the basics for it are more or less there (if not merged yet...), and the theorem would be at most another #8737, though probably more like half as much (while trying to use the project to generate more general library code).

[Yaël Dillies]

I meant unmerged :grinning_face_with_smiling_eyes: It will still take some time before your marvelous branch hits master.