Tutte's theorem statement

Stream: mathlib4

[Pim Otte]

I wanna try and prove Tutte's theorem. I've come to the following statement. Before I move in and try to prove it, does anyone see anything that's problematic or unidiomatic? The eventual goal is a PR to mathlib, so anything with that in mind is welcome specifically:)

import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Combinatorics.SimpleGraph.Matching
import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Combinatorics.SimpleGraph.Subgraph
import Mathlib.Data.Fintype.Powerset
import Mathlib.Data.Set.Card

namespace SimpleGraph

variable {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj]

instance (u : ConnectedComponent G) : Fintype (u.supp) := sorry

def ConnectedComponent.card (u : ConnectedComponent G) : Nat := Fintype.card u.supp

def OddConnectedComponents (U : SimpleGraph.Subgraph G) : Type _
   := {component : SimpleGraph.ConnectedComponent U.coe // Odd (component.card)}

instance (U : Subgraph G) [DecidableEq V] : Fintype (OddConnectedComponents U) := sorry

def numOddComponents [DecidableEq V] (U : Subgraph G) : Nat := Fintype.card (OddConnectedComponents U)

def tutte [DecidableEq V] : (∃ (M : Subgraph G) , M.IsPerfectMatching) ↔ (∀ (u : Set V),
      numOddComponents (Subgraph.induce (G.toSubgraph G (le_rfl)) u) ≤ u.ncard) :=
  sorry

[Martin Dvořák]

Very cool you work on Tutte's theorem!

[Alex J. Best]

Can you use SimpleGraph.induce in place of Subgraph.induce (G.toSubgraph G (le_rfl)) ?

[Alex J. Best]

Maybe its more work in the long run, but just checking you also considered that option

[Pim Otte]

I hadn't, I can't really oversee the consequences, but it does look more clean:

import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Combinatorics.SimpleGraph.Matching
import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Combinatorics.SimpleGraph.Subgraph
import Mathlib.Data.Fintype.Powerset
import Mathlib.Data.Set.Card

namespace SimpleGraph

variable {V : Type u} [Fintype V] {u : Set V}

instance (cc : ConnectedComponent G) : Fintype (cc.supp) := sorry

def ConnectedComponent.card (cc : ConnectedComponent G) : Nat := Fintype.card cc.supp

def OddConnectedComponents (G : SimpleGraph u) : Type _
   := {component : ConnectedComponent G // Odd (component.card)}

instance (G : SimpleGraph u) [DecidableEq V] : Fintype (OddConnectedComponents G) := sorry

def numOddComponents [DecidableEq V] {u : Set V} (G : SimpleGraph u) : Nat := Fintype.card (OddConnectedComponents G)

def tutte [DecidableEq V] : (∃ (M : Subgraph G) , M.IsPerfectMatching) ↔ (∀ (u : Set V),
      numOddComponents (SimpleGraph.induce u G) ≤ u.ncard) :=
  sorry

[Kyle Miller]

@Pim Otte I think this might be how I'd set things up:

import Mathlib.Combinatorics.SimpleGraph.Matching
import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Data.Set.Card

namespace SimpleGraph

variable {V : Type*} {G : SimpleGraph V}

/-- A connected component is *odd* if it has an add number of vertices
in its support. -/
-- Note: only connected components with finitely many vertices can be odd.
def ConnectedComponent.isOdd (c : G.ConnectedComponent) : Prop :=
  Odd (Nat.card c.supp)

noncomputable def cardOddComponents (G : SimpleGraph V) : Nat :=
  Set.ncard {c : G.ConnectedComponent | c.isOdd}

def tutte [Finite V] :
    (∃ (M : Subgraph G) , M.IsPerfectMatching) ↔
      (∀ (u : Set V),
        cardOddComponents ((⊤ : G.Subgraph).deleteVerts u).coe ≤ u.ncard) :=
  sorry

[Kyle Miller]

(I changed this to deleting vertices rather than inducing a subgraph, which is what I think is the statement of Tutte's theorem.)

[Kyle Miller]

Here are some extra things that might be useful at some point.

lemma ConnectedComponent.isOdd_iff (c : G.ConnectedComponent) [Fintype c.supp] :
    c.isOdd ↔ Odd (Fintype.card c.supp) := by
  rw [isOdd, Nat.card_eq_fintype_card]

-- Follows from other instances:
--instance (u : ConnectedComponent G) : Fintype u.supp := inferInstance

/-- This is `Quot.recOn` specialized to connected components.
For convenience, it strengthens the assumptions in the hypothesis
to provide a path between the vertices. -/
@[elab_as_elim]
def ConnectedComponent.recOn
    {motive : G.ConnectedComponent → Sort*}
    (c : G.ConnectedComponent)
    (f : (v : V) → motive (G.connectedComponentMk v))
    (h : ∀ (u v : V) (p : G.Walk u v) (_ : p.IsPath),
      ConnectedComponent.sound p.reachable ▸ f u = f v) :
    motive c :=
  Quot.recOn c f (fun u v r => r.elim_path fun p => h u v p p.2)

instance [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
    (c : G.ConnectedComponent) (v : V) : Decidable (v ∈ c.supp) :=
  c.recOn
    (fun w => by simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]; infer_instance)
    (fun _ _ _ _ => Subsingleton.elim _ _)

[Pim Otte]

Awesome, thanks, I'll see if I can build on this:) (oops@the deleting instead of subgraph, that's kind of critical)

[Pim Otte]

@Kyle Miller I'm making some small steps, but I can't get the instance you mention should follow from others. Any pointers?

import Mathlib.Combinatorics.SimpleGraph.Matching
import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Data.Set.Card
import Mathlib.Data.Set.Finite

namespace SimpleGraph

variable {V : Type*} {G : SimpleGraph V}

-- Follows from other instances?
instance [Finite V] [Fintype V] (u : ConnectedComponent G) : Fintype u.supp := inferInstance

[Kyle Miller]

@Pim Otte Oops, I must have copy-pasted some things out of order. Here:

import Mathlib.Combinatorics.SimpleGraph.Matching
import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Data.Set.Card
import Mathlib.Data.Set.Finite

namespace SimpleGraph

variable {V : Type*} {G : SimpleGraph V}

/-- This is `Quot.recOn` specialized to connected components.
For convenience, it strengthens the assumptions in the hypothesis
to provide a path between the vertices. -/
@[elab_as_elim]
def ConnectedComponent.recOn
    {motive : G.ConnectedComponent → Sort*}
    (c : G.ConnectedComponent)
    (f : (v : V) → motive (G.connectedComponentMk v))
    (h : ∀ (u v : V) (p : G.Walk u v) (_ : p.IsPath),
      ConnectedComponent.sound p.reachable ▸ f u = f v) :
    motive c :=
  Quot.recOn c f (fun u v r => r.elim_path fun p => h u v p p.2)

instance [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
    (c : G.ConnectedComponent) (v : V) : Decidable (v ∈ c.supp) :=
  c.recOn
    (fun w => by simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]; infer_instance)
    (fun _ _ _ _ => Subsingleton.elim _ _)

instance [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (u : ConnectedComponent G) :
    Fintype u.supp := inferInstance

[Kyle Miller]

There's probably a better instance, but this one is fine if you're working with finite graphs mathematically and you're not actually interested #evaling things like the cardinality of the support. It takes a bit of untangling to see what's going on, but the way that u.supp is a fintype here is that (1) it's a subset of the fintype V and (2) there's an algorithm for telling whether or not a given v is an element of u.supp, so one can enumerate the support by filtering V according to this algorithm. This algorithm isn't very efficient: it chooses a basepoint for u and enumerates all walks starting from u up to length card V - 1 and sees if v is ever one of the endpoints.

[Pim Otte]

I've been working on this every once in a while, and it seems like a good time to ask for a little feedback and help.

The current concrete problem I'm running into is that I don't know how to really connect (Subgraph.coe (⊤ : Subgraph G)) with G to prove the have heven : .... Rewriting the statements of the lemma's somehow got some Lean.Internal stuff to enter the context, which kind of made me think I might be barking up the wrong tree. I'm very open to pointers specifically about this or my general approach/structure/cleaner proofs etc.

import Mathlib.Combinatorics.SimpleGraph.Matching
import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Data.Set.Card
import Mathlib.Data.Set.Finite

namespace SimpleGraph

variable {V : Type*} {G : SimpleGraph V}

/-- A connected component is *odd* if it has an add number of vertices
in its support. -/
-- Note: only connected components with finitely many vertices can be odd.
def ConnectedComponent.isOdd (c : G.ConnectedComponent) : Prop :=
  Odd (Nat.card c.supp)

noncomputable def cardOddComponents (G : SimpleGraph V) : Nat :=
  Set.ncard {c : G.ConnectedComponent | c.isOdd}

lemma ConnectedComponent.isOdd_iff (c : G.ConnectedComponent) [Fintype c.supp] :
    c.isOdd ↔ Odd (Fintype.card c.supp) := by
  rw [isOdd, Nat.card_eq_fintype_card]

/-- This is `Quot.recOn` specialized to connected components.
For convenience, it strengthens the assumptions in the hypothesis
to provide a path between the vertices. -/
@[elab_as_elim]
def ConnectedComponent.recOn
    {motive : G.ConnectedComponent → Sort*}
    (c : G.ConnectedComponent)
    (f : (v : V) → motive (G.connectedComponentMk v))
    (h : ∀ (u v : V) (p : G.Walk u v) (_ : p.IsPath),
      ConnectedComponent.sound p.reachable ▸ f u = f v) :
    motive c :=
  Quot.recOn c f (fun u v r => r.elim_path fun p => h u v p p.2)

instance [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
    (c : G.ConnectedComponent) (v : V) : Decidable (v ∈ c.supp) :=
  c.recOn
    (fun w => by simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]; infer_instance)
    (fun _ _ _ _ => Subsingleton.elim _ _)

instance myInst2 [r : DecidableRel G.Adj] : DecidableRel (Subgraph.coe (⊤ : Subgraph G)).Adj := by
  intro x y
  cases (r x y) with
  | isFalse nh => {
    exact .isFalse (by
      intro w
      exact nh (Subgraph.coe_adj_sub _ _ _ w)
      )
  }
  | isTrue h => {
    exact .isTrue (by
      apply (Subgraph.coe_adj_sub _ _ _ _)
      exact h
    )
  }

instance myInst [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (u : ConnectedComponent G) :
    Fintype u.supp := inferInstance


lemma SimpleGraph.PerfectMatchingInducesMatchingOnComponent [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
  (M : Subgraph G) (hM : Subgraph.IsPerfectMatching M) (c : ConnectedComponent G) : (Subgraph.IsMatching (M.induce c.supp)) := by
    intro v hv
    have vM : v ∈ M.verts := by
      apply hM.2
    have h := hM.1 vM
    obtain ⟨ w, hw ⟩ := h
    use w
    dsimp at *
    constructor
    · constructor
      · assumption
      · constructor
        · rw [ConnectedComponent.mem_supp_iff]
          rw [ConnectedComponent.mem_supp_iff] at hv
          rw [← hv]
          apply ConnectedComponent.connectedComponentMk_eq_of_adj
          apply M.adj_sub
          rw [Subgraph.adj_comm]
          exact hw.1
        · exact hw.1
    · intro y hy
      apply hw.2
      exact hy.2.2
    done

lemma SimpleGraph.PerfectMatchingConnectedComponentEven [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
  (M : Subgraph G) (hM : Subgraph.IsPerfectMatching M) (c : ConnectedComponent G) : Even (Fintype.card ↑(ConnectedComponent.supp c)) := by
    classical
    have h : Even (M.induce c.supp).verts.toFinset.card := by exact Subgraph.IsMatching.even_card (SimpleGraph.PerfectMatchingInducesMatchingOnComponent M hM c)
    obtain ⟨ k , hk ⟩ := h
    use k
    rw [← hk, Subgraph.induce_verts, @Fintype.card_ofFinset]
    congr
    simp only [ConnectedComponent.mem_supp_iff, Finset.mem_univ, forall_true_left]
    exact Set.filter_mem_univ_eq_toFinset fun x => connectedComponentMk G x = c

    done
def tutte [Fintype V] [DecidableEq V] [DecidableRel G.Adj] :
    (∃ (M : Subgraph G) , M.IsPerfectMatching) ↔
      (∀ (u : Set V),
        cardOddComponents ((⊤ : G.Subgraph).deleteVerts u).coe ≤ u.ncard) := by
  constructor
  {
    rintro ⟨M, hM⟩ u
    exact Set.Finite.induction_on u.toFinite
      (by
        have h : (⊤ : G.Subgraph).deleteVerts ∅ = ⊤ := by simp
        rw [h]
        have h2 : @Set.ncard V ∅ = 0 := by simp
        rw [h2, cardOddComponents]
        simp only [Subgraph.verts_top, nonpos_iff_eq_zero]
        rw [← h2]
        have h3 :  {c | @ConnectedComponent.isOdd _ (Subgraph.coe ⊤) c} = ∅ := by
          simp [Set.ext_iff]
          intro c
          rw [@ConnectedComponent.isOdd_iff _ _ _ (@myInst _ _ _ _ (myInst2 : DecidableRel (Subgraph.coe (⊤ : Subgraph G)).Adj) c)]
          intro hodd
          have heven : Even (Fintype.card ↑(ConnectedComponent.supp c)) := by
            apply SimpleGraph.PerfectMatchingConnectedComponentEven M hM c
          exact Nat.odd_iff_not_even.mp hodd heven

          done
        simp [h3]
      )
        _
    sorry
  }
  {
    cases nonempty_fintype V
    intro h
    sorry
  }

[Kyle Miller]

@Pim Otte There's one tricky dependent type obstacle along the way, but you can get around it with generalize (to be able to simplify deleteVerts on the empty set) and subst (to apply the simplification. The rest is using some library lemmas for connected components over equivalences, as well as being comfortable with moving between different notions of cardinality (and using classical).

Here's the first by:

      (by
        suffices : {c : ((⊤ : G.Subgraph).deleteVerts ∅).coe.ConnectedComponent | c.isOdd} = ∅
        · rw [cardOddComponents, this]
          simp
        generalize hH : ((⊤ : G.Subgraph).deleteVerts ∅) = H
        simp only [Subgraph.deleteVerts_empty] at hH
        subst hH
        ext c
        simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.mem_setOf_eq,
          Set.mem_empty_iff_false, iff_false]
        rw [ConnectedComponent.isOdd, Nat.odd_iff_not_even, not_not]
        classical
        rw [Nat.card_eq_fintype_card]
        have := SimpleGraph.PerfectMatchingConnectedComponentEven M hM
                  (Iso.connectedComponentEquiv Subgraph.topEquiv c)
        convert this using 1
        apply Fintype.card_congr
        exact ConnectedComponent.isoEquivSupp Subgraph.topEquiv c
      )

[Kyle Miller]

Subgraph.topEquiv is the isomorphism between a graph as a subgraph of itself and the graph

[Pim Otte]

I'm now running into a curious problem, which I have isolated. The #check below outputs Subgraph.induce M (Lean.Internal.coeM (ConnectedComponent.supp c)) : Subgraph G. The Lean.Internal.coeM seems weird, the docs seem to say that it's only for internal use, but I don't think I'm doing anything out there. Any pointers?

import Mathlib.Combinatorics.SimpleGraph.Matching
import Mathlib.Combinatorics.SimpleGraph.Connectivity

namespace SimpleGraph

variable [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
  (M : Subgraph G) (hM : Subgraph.IsPerfectMatching M) (u : Set V)(c : ConnectedComponent ((⊤ : G.Subgraph).deleteVerts u).coe)

#check (M.induce c.supp)

[Floris van Doorn]

This usually occurs when you have a coercion coe : A -> B, and you treat an element of Set A as an element of Set B.

[Floris van Doorn]

Although I think this was fixed recently. I get Subgraph.induce M (Subtype.val '' ConnectedComponent.supp c) : Subgraph G.

[Floris van Doorn]

#8413

[Pim Otte]

Ah, yes, a mathlib update solved it, thanks!

[Pim Otte]

A lot of ungolfed code, but, the first direction is done:) (I ended up dropping the induction on u)

import Mathlib.Combinatorics.SimpleGraph.Matching
import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Data.Set.Card
import Mathlib.Data.Set.Finite

import LeanInfer

namespace SimpleGraph

variable {V : Type*} {G : SimpleGraph V}

/-- A connected component is *odd* if it has an add number of vertices
in its support. -/
-- Note: only connected components with finitely many vertices can be odd.
def ConnectedComponent.isOdd (c : G.ConnectedComponent) : Prop :=
  Odd (Nat.card c.supp)

noncomputable def cardOddComponents (G : SimpleGraph V) : Nat :=
  Set.ncard {c : G.ConnectedComponent | c.isOdd}

lemma ConnectedComponent.isOdd_iff (c : G.ConnectedComponent) [Fintype c.supp] :
    c.isOdd ↔ Odd (Fintype.card c.supp) := by
  rw [isOdd, Nat.card_eq_fintype_card]

/-- This is `Quot.recOn` specialized to connected components.
For convenience, it strengthens the assumptions in the hypothesis
to provide a path between the vertices. -/
@[elab_as_elim]
def ConnectedComponent.recOn
    {motive : G.ConnectedComponent → Sort*}
    (c : G.ConnectedComponent)
    (f : (v : V) → motive (G.connectedComponentMk v))
    (h : ∀ (u v : V) (p : G.Walk u v) (_ : p.IsPath),
      ConnectedComponent.sound p.reachable ▸ f u = f v) :
    motive c :=
  Quot.recOn c f (fun u v r => r.elim_path fun p => h u v p p.2)

instance [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
    (c : G.ConnectedComponent) (v : V) : Decidable (v ∈ c.supp) :=
  c.recOn
    (fun w => by simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]; infer_instance)
    (fun _ _ _ _ => Subsingleton.elim _ _)



lemma deleteVerts_verts_notmem_deleted [r : DecidableRel G.Adj] (a : ((⊤ : G.Subgraph).deleteVerts u).verts) : a.val ∉ u := a.prop.2


instance myInst3 [r : DecidableRel G.Adj] : DecidableRel (((⊤ : G.Subgraph).deleteVerts u).coe).Adj := by
  intro x y
  cases (r x y) with
  | isFalse nh => {
    exact .isFalse (by
      intro w
      exact nh (Subgraph.coe_adj_sub _ _ _ w)
      )
  }
  | isTrue h => {
    exact .isTrue (by
      apply (SimpleGraph.Subgraph.Adj.coe)
      apply Subgraph.deleteVerts_adj.mpr
      constructor
      · trivial
      constructor
      · exact deleteVerts_verts_notmem_deleted x
      constructor
      · trivial
      constructor
      · exact deleteVerts_verts_notmem_deleted y
      exact h
      done

    )
  }

instance myInst2 [r : DecidableRel G.Adj] : DecidableRel (Subgraph.coe (⊤ : Subgraph G)).Adj := by
  intro x y
  cases (r x y) with
  | isFalse nh => {
    exact .isFalse (by
      intro w
      exact nh (Subgraph.coe_adj_sub _ _ _ w)
      )
  }
  | isTrue h => {
    exact .isTrue (by
      apply (Subgraph.coe_adj_sub _ _ _ _)
      exact h
    )
  }

instance myInst [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (u : ConnectedComponent G) :
    Fintype u.supp := inferInstance


lemma SimpleGraph.PerfectMatchingInducesMatchingOnComponent [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
  (M : Subgraph G) (hM : Subgraph.IsPerfectMatching M) (c : ConnectedComponent G) : (Subgraph.IsMatching (M.induce c.supp)) := by
    intro v hv
    have vM : v ∈ M.verts := by
      apply hM.2
    have h := hM.1 vM
    obtain ⟨ w, hw ⟩ := h
    use w
    dsimp at *
    constructor
    · constructor
      · assumption
      · constructor
        · rw [ConnectedComponent.mem_supp_iff]
          rw [ConnectedComponent.mem_supp_iff] at hv
          rw [← hv]
          apply ConnectedComponent.connectedComponentMk_eq_of_adj
          apply M.adj_sub
          rw [Subgraph.adj_comm]
          exact hw.1
        · exact hw.1
    · intro y hy
      apply hw.2
      exact hy.2.2
    done


lemma SimpleGraph.PerfectMatchingConnectedComponentEven [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
  (M : Subgraph G) (hM : Subgraph.IsPerfectMatching M) (c : ConnectedComponent G) : Even (Fintype.card ↑(ConnectedComponent.supp c)) := by
    classical
    have h : Even (M.induce c.supp).verts.toFinset.card := by exact Subgraph.IsMatching.even_card (SimpleGraph.PerfectMatchingInducesMatchingOnComponent M hM c)
    obtain ⟨ k , hk ⟩ := h
    use k
    rw [← hk, Subgraph.induce_verts, @Fintype.card_ofFinset]
    congr
    simp only [ConnectedComponent.mem_supp_iff, Finset.mem_univ, forall_true_left]
    exact Set.filter_mem_univ_eq_toFinset fun x => connectedComponentMk G x = c

    done

noncomputable instance myInst5 [Fintype V] [DecidableEq V] (u : Set V) : Fintype u := by
  exact Fintype.ofFinite ↑u

noncomputable instance myInst4 [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
    (u : Set V) [Fintype u]:
    Fintype ((⊤ : G.Subgraph).deleteVerts u).verts := by
      simp only [Subgraph.induce_verts, Subgraph.verts_top]
      infer_instance


theorem mem_supp_of_adj (C : G.ConnectedComponent) (v w : V) (hv : v ∈ C.supp) (hadj : G.Adj v w) :
       w ∈ C.supp := by

      rw [ConnectedComponent.mem_supp_iff]
      rw [← (ConnectedComponent.mem_supp_iff _ _).mp hv]
      exact ConnectedComponent.connectedComponentMk_eq_of_adj (adj_symm G hadj)


theorem mem_supp_of_adj' [Fintype V] [DecidableEq V] [DecidableRel G.Adj]  (c : ConnectedComponent ((⊤ : Subgraph G).deleteVerts u).coe)
      (v w : V) (hv : v ∈ Subtype.val '' c.supp) (hw : w ∈ ((⊤ : Subgraph G).deleteVerts  u).verts)
      (hadj : G.Adj v w) :
       w ∈ Subtype.val '' c.supp := by
      rw [Set.mem_image]
      obtain ⟨ v' , hv' ⟩ := hv
      use ⟨ w , ⟨ by trivial , by refine Set.not_mem_of_mem_diff hw ⟩ ⟩
      rw [ConnectedComponent.mem_supp_iff]
      constructor
      · rw [← (ConnectedComponent.mem_supp_iff _ _).mp hv'.1]
        apply ConnectedComponent.connectedComponentMk_eq_of_adj
        apply SimpleGraph.Subgraph.Adj.coe
        rw [Subgraph.deleteVerts_adj]
        constructor
        · exact trivial
        · constructor
          · exact Set.not_mem_of_mem_diff hw
          · constructor
            · exact trivial
            · constructor
              · exact deleteVerts_verts_notmem_deleted v'
              · rw [Subgraph.top_adj]
                rw [hv'.2]
                exact adj_symm G hadj


      · dsimp

lemma OddComponentHasNodeMatchedOutside [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
  (M : Subgraph G) (hM : Subgraph.IsPerfectMatching M) (u : Set V) (c : ConnectedComponent ((⊤ : Subgraph G).deleteVerts u).coe)
  (codd : c.isOdd) : ∃ (w : Set.Elem u) (v : Set.Elem ((⊤ : G.Subgraph).deleteVerts u).verts) ,  M.Adj v w ∧ v ∈ c.supp := by
      rw [ConnectedComponent.isOdd_iff] at codd

      by_contra' h


      have h' : (Subgraph.IsMatching (M.induce c.supp)) := by
        intro v hv
        obtain ⟨ w , hw ⟩ := hM.1 (hM.2 v)
        obtain ⟨ v' , hv' ⟩ := hv
        use w
        dsimp at *
        constructor
        · constructor
          · exact ⟨ v' , hv' ⟩
          · constructor
            · have h'' : w ∉ u := by
                intro hw'
                apply h ⟨ w , hw' ⟩ v' _
                · exact hv'.1
                rw [hv'.2]
                exact hw.1
                done

              apply mem_supp_of_adj' c v' w ⟨ v' , ⟨ hv'.1 , rfl ⟩ ⟩ ⟨ by trivial , h'' ⟩
              rw [hv'.2]
              exact Subgraph.adj_sub _ hw.1
            · exact hw.1
        · intro y hy
          apply hw.2
          exact hy.2.2
        done

      apply Nat.odd_iff_not_even.mp codd
      have h'' := Subgraph.IsMatching.even_card h'
      simp only [Subgraph.induce_verts, Subgraph.verts_top] at h''
      unfold Fintype.card
      rw [Nat.even_iff] at h'' ⊢
      rw [← h'']
      rw [ Set.toFinset_image ]
      rw [Finset.card_image_of_injective _ (Subtype.val_injective)]
      simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.toFinset_card]
      rfl


def tutte [Fintype V] [Inhabited V] [DecidableEq V] [DecidableRel G.Adj] :
    (∃ (M : Subgraph G) , M.IsPerfectMatching) ↔
      (∀ (u : Set V),
        cardOddComponents ((⊤ : G.Subgraph).deleteVerts u).coe ≤ u.ncard) := by
  constructor
  {
    rintro ⟨M, hM⟩ u
    unfold cardOddComponents
    let f : {c : ConnectedComponent ((⊤ : Subgraph G).deleteVerts u).coe | ConnectedComponent.isOdd c} → u :=
      fun c => Exists.choose (OddComponentHasNodeMatchedOutside M hM u c c.2)

    let g : ConnectedComponent ((⊤ : Subgraph G).deleteVerts u).coe → V := fun c =>
      if h : Odd (Fintype.card c.supp) then f ⟨ c , (by
            rw [← ConnectedComponent.isOdd_iff] at h
            exact h
      ) ⟩ else default

    exact Set.ncard_le_ncard_of_injOn g (by
      intro a ha
      dsimp at ha
      have h : g a = f ⟨ a , ha ⟩ := by
        rw [dite_eq_iff]
        left
        use (ConnectedComponent.isOdd_iff _).mp ha
        done
      rw [h]
      dsimp
      rw [Set.mem_def]
      simp only [ConnectedComponent.mem_supp_iff, Subtype.exists, Set.mem_diff, Set.mem_univ,
        true_and, exists_and_left]
      apply Subtype.prop
      ) (by
        intro x hx y hy hxy
        have h : g x = f ⟨ x , hx ⟩ := by
          rw [dite_eq_iff]
          left
          use (ConnectedComponent.isOdd_iff _).mp hx
          done
        have h' : g y = f ⟨ y , hy ⟩ := by
          rw [dite_eq_iff]
          left
          use (ConnectedComponent.isOdd_iff _).mp hy
          done
        rw [h, h'] at hxy

        dsimp at hxy
        obtain ⟨ v , hv ⟩ := (OddComponentHasNodeMatchedOutside M hM u x hx).choose_spec
        obtain ⟨ v' , hv' ⟩ := (OddComponentHasNodeMatchedOutside M hM u y hy).choose_spec


        have ⟨ w , hw ⟩ := (Subgraph.isPerfectMatching_iff M).mp hM (f ⟨ x , hx ⟩)
        have h'' := hw.2 _ hv.1.symm
        rw [hxy] at hw
        have h''' := hw.2 _ hv'.1.symm
        rw [← h'''] at h''
        rw [← ((ConnectedComponent.mem_supp_iff x v).mp hv.2)]
        rw [← ((ConnectedComponent.mem_supp_iff y v').mp hv'.2)]
        rw [Subtype.val_injective h'']
      ) (Set.toFinite u)
  }
  {
    sorry
  }

[Pim Otte]

I've been mapping out the other direction The proof on wikipedia seems fairly direct and suitable. Every proof does start with some reasoning why it's okay to take G as edge-maximal, and I was wondering how to approach that. I came up with the statement below:

    have hEdgeMaximal : ∀ (v w : V), ¬ G.Adj v w → ∃ (M : Subgraph ((⊤ : Subgraph G).deleteVerts {v , w}).coe), M.IsPerfectMatching
      := sorry

This still needs a little shaving because I can't really assume G itself is edge maximal, but in any case I can think of two other approaches: 1. Adding the edge instead of removing the nodes. (This is what the paper proofs do, but I think this is equivalent and better supported. 2. Somehow using the lattice structure. This seems really elegant, but I have no idea if it's possible to set something up along the lines of "an edge-maximal G that has no perfect matching".

@Kyle Miller Do you have some intuition on which of these approaches is most suitable/idiomatic?

[Kyle Miller]

Deleting vertices sets you up for dependent type problems, so if you can formulate the argument in terms of edges easily enough, I think you'll run into fewer type theory issues. For adding an edge to a graph, you can take the sup with docs#SimpleGraph.subgraphOfAdj, though you could also define the positive version of docs#SimpleGraph.deleteEdges that uses Sym2.ToRel s for the Adj relation. (Note that you might not want to talk about edges themselves at all if you can help it, since their undirected nature can make things combinatorially complicated.)

I'm not sure it's correct, but a lattice version of edge maximality of G might be "for all graphs G' : SimpleGraph V such that G < G' then there exists M : Subgraph G' such that M.IsPerfectMatching"

[Pim Otte]

@Kyle Miller I've made some progress, do you have any thoughts or pointers on the sorry's or the structure I've built?:)

import Mathlib.Combinatorics.SimpleGraph.Matching
import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Data.Set.Card
import Mathlib.Data.Set.Finite

namespace SimpleGraph

variable {V : Type*} {G : SimpleGraph V}

/-- A connected component is *odd* if it has an add number of vertices
in its support. -/
-- Note: only connected components with finitely many vertices can be odd.
def ConnectedComponent.isOdd (c : G.ConnectedComponent) : Prop :=
  Odd (Nat.card c.supp)

noncomputable def cardOddComponents (G : SimpleGraph V) : Nat :=
  Set.ncard {c : G.ConnectedComponent | c.isOdd}

lemma ConnectedComponent.isOdd_iff (c : G.ConnectedComponent) [Fintype c.supp] :
    c.isOdd ↔ Odd (Fintype.card c.supp) := by
  rw [isOdd, Nat.card_eq_fintype_card]

/-- This is `Quot.recOn` specialized to connected components.
For convenience, it strengthens the assumptions in the hypothesis
to provide a path between the vertices. -/
@[elab_as_elim]
def ConnectedComponent.recOn
    {motive : G.ConnectedComponent → Sort*}
    (c : G.ConnectedComponent)
    (f : (v : V) → motive (G.connectedComponentMk v))
    (h : ∀ (u v : V) (p : G.Walk u v) (_ : p.IsPath),
      ConnectedComponent.sound p.reachable ▸ f u = f v) :
    motive c :=
  Quot.recOn c f (fun u v r => r.elim_path fun p => h u v p p.2)

instance [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
    (c : G.ConnectedComponent) (v : V) : Decidable (v ∈ c.supp) :=
  c.recOn
    (fun w => by simp only [ConnectedComponent.mem_supp_iff, ConnectedComponent.eq]; infer_instance)
    (fun _ _ _ _ => Subsingleton.elim _ _)


instance myInst [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (u : ConnectedComponent G) :
    Fintype u.supp := inferInstance



lemma oddComponentsIncrease [Fintype V] [Inhabited V] [DecidableEq V]  (G G' : SimpleGraph V)
    (h : G ≤  G') (u : Set V) [Finite u]:
    cardOddComponents ((⊤ : Subgraph G').deleteVerts u).coe ≤ cardOddComponents ((⊤ : Subgraph G).deleteVerts u).coe := by
      -- I left out [DecideableRel G.Adj] [Decidable G'.Adj] because it would be nice if this can be done without it
      -- it would need to proved for Gmax

      -- Seems doable but involved
      let g : ConnectedComponent ((⊤ : Subgraph G').deleteVerts u).coe → ConnectedComponent ((⊤ : Subgraph G).deleteVerts u).coe := sorry

      haveI : Finite (ConnectedComponent ((⊤ : Subgraph G).deleteVerts u).coe) := sorry

      exact Set.ncard_le_ncard_of_injOn g (by sorry) (by sorry)

def tutte [Fintype V] [Inhabited V] [DecidableEq V] [DecidableRel G.Adj] :
    (∃ (M : Subgraph G) , M.IsPerfectMatching) ↔
      (∀ (u : Set V),
        cardOddComponents ((⊤ : G.Subgraph).deleteVerts u).coe ≤ u.ncard) := by
  constructor
  {
    -- actually solved, omitted for brevity
    sorry
  }
  {
    contrapose!
    intro h

    have ⟨ Gmax , hGmax ⟩ : ∃ (G' : SimpleGraph V),
      G ≤ G' ∧
      (∀ (M : Subgraph G'), ¬ M.IsPerfectMatching)  ∧
      ∀ (G'' : SimpleGraph V), G' < G'' → ∃ (M : Subgraph G''), M.IsPerfectMatching := by
        by_contra' hc
        have ⟨ H , hH ⟩ := hc G (Eq.ge rfl) h
        have ⟨ H' , hH' ⟩ := hc H (le_of_lt hH.1) hH.2
        -- This sorry is kind of stumping me. I kind of want to make the argument
        -- that we can't have an infinite chain of strictly larger graphs.
        sorry

    suffices : ∃ u, Set.ncard u < cardOddComponents ((⊤ : Subgraph Gmax).deleteVerts u).coe
    · obtain ⟨u, hu ⟩ := this
      use u
      exact lt_of_lt_of_le hu (by
        exact oddComponentsIncrease G Gmax hGmax.1 u
        )

    let S : Set V := {v | G.degree v = Fintype.card V - 1}

    let Gsplit := ((⊤ : Subgraph Gmax).deleteVerts S)
    have ⟨K, v, w, hKvw ⟩ : ∃ (K : ConnectedComponent Gsplit.coe) (v w :  Set.Elem Gsplit.verts),
      v ∈ K.supp ∧ w ∈ K.supp ∧ v ≠ w ∧ ¬ Gmax.Adj v w := sorry

    sorry
  }