Formal target: Corpus.BergeFulkerson.conjecture
Every finite bridgeless cubic simple graph (Mathlib SimpleGraph with quantified Fintype and DecidableRel instances, IsRegularOfDegree 3, no edge an IsBridge) has a family Fin 6 → G.Subgraph of perfect matchings (Subgraph.IsPerfectMatching) such that for every edge the set of indices whose matching contains it has ncard exactly 2.
Exact formal statement
∀ {V : Type} [inst : Fintype.{0} V] (G : SimpleGraph.{0} V) [inst_1 : DecidableRel.{1, 1} (SimpleGraph.Adj.{0} G)],
SimpleGraph.IsRegularOfDegree.{0} G 3 →
Corpus.BergeFulkerson.Bridgeless G →
Exists.{1} fun M =>
And (∀ (i : Fin 6), SimpleGraph.Subgraph.IsPerfectMatching.{0} (M i))
(∀ (e : Sym2.{0} V),
Membership.mem.{0, 0} (SimpleGraph.edgeSet.{0} G) e →
Eq.{1}
(Set.ncard.{0}
(Set.ofPred.{0} fun i => Membership.mem.{0, 0} (SimpleGraph.Subgraph.edgeSet.{0} (M i)) e))
2)This target is a formal statement, not a proof of the problem.
Environment availability: available.