-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
intro : ∀ (val : Fintype V), ∃ (u : Set V), G.IsTutteViolator u
intro₁ :
  ∀ (val : Fintype V) (Gmax : SimpleGraph V) (hSubgraph : G ≤ Gmax) (hMatchingFree : Gmax.IsMatchingFree)
    (hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching), ∃ (u : Set V), G.IsTutteViolator u
intro₂ :
  ∀ (val : Fintype V) (Gmax : SimpleGraph V) (hSubgraph : G ≤ Gmax) (hMatchingFree : Gmax.IsMatchingFree)
    (hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching), Gmax.IsTutteViolator Gmax.universalVerts
intro₃ :
  ∀ (val : Fintype V) (Gmax : SimpleGraph V) (hSubgraph : G ≤ Gmax) (hMatchingFree : Gmax.IsMatchingFree)
    (hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching) (hc : ¬Gmax.IsTutteViolator Gmax.universalVerts),
    False
intro₄ :
  ∀ (val : Fintype V) (Gmax : SimpleGraph V) (hSubgraph : G ≤ Gmax) (hMatchingFree : Gmax.IsMatchingFree)
    (hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching)
    (hc :
      ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
          Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)),
    False
pos :
  ∀ (val : Fintype V) (Gmax : SimpleGraph V) (hSubgraph : G ≤ Gmax) (hMatchingFree : Gmax.IsMatchingFree)
    (hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching)
    (hc :
      ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
          Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1))
    (h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp),
    False
neg neg₁ :
  ∀ (val : Fintype V) (Gmax : SimpleGraph V) (hSubgraph : G ≤ Gmax) (hMatchingFree : Gmax.IsMatchingFree)
    (hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching)
    (hc :
      ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
          Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1))
    (h' : ∃ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp),
    False
⊢ ∃ (u : Set V), G.IsTutteViolator u

Tactic:
classical
  cases nonempty_fintype V
  -- It suffices to consider the edge-maximal case
  obtain ⟨Gmax, hSubgraph, hMatchingFree, hMaximal⟩ := exists_maximal_isMatchingFree h
  refine ⟨Gmax.universalVerts, .mono hSubgraph ?_⟩
  by_contra! hc
  simp only [IsTutteViolator, Set.ncard_eq_toFinset_card', Set.toFinset_card] at hc
  by_cases! h' : ∀ (K : ConnectedComponent Gmax.deleteUniversalVerts.coe),
      Gmax.deleteUniversalVerts.coe.IsClique K.supp
  · -- Deleting universal vertices splits the graph into cliques
    rw [Fintype.card_eq_nat_card] at hc
    simp_rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] at hc
    push Not at hc
    obtain ⟨M, hM⟩ := Subgraph.IsPerfectMatching.exists_of_isClique_supp hvEven
      (by simpa [IsTutteViolator] using hc) h'
    exact hMatchingFree M hM
  · -- Deleting universal vertices does not result in only cliques
    obtain ⟨K, hK⟩ := h'
    obtain ⟨x, y, hxy⟩ := (not_isClique_iff _).mp hK
    obtain ⟨p, hp⟩ := Reachable.exists_path_of_dist (K.connected_toSimpleGraph x y)
    obtain ⟨x, a, b, hxa, hxb, hnadjxb, hnxb⟩ := Walk.exists_adj_adj_not_adj_ne hp.2
      (p.reachable.one_lt_dist_of_ne_of_not_adj hxy.1 hxy.2)
    simp only [ConnectedComponent.toSimpleGraph, deleteUniversalVerts, universalVerts, ne_eq,
      Subgraph.induce_verts, Subgraph.verts_top, comap_adj, Function.Embedding.coe_subtype,
      Subgraph.coe_adj, Subgraph.induce_adj, Subtype.coe_prop, Subgraph.top_adj, true_and]
      at hxa hxb hnadjxb
    obtain ⟨c, hc⟩ : ∃ (c : V), (a : V) ≠ c ∧ ¬ Gmax.Adj c a := by
      simpa [universalVerts] using a.1.2.2
    have hbnec : b.val.val ≠ c := by rintro rfl; exact hc.2 hxb.symm
    obtain ⟨_, hG1⟩ := hMaximal _ <| left_lt_sup.mpr (by
      rw [edge_le_iff (v := x.1.1) (w := b.1.1)]
      simp [hnadjxb, Subtype.val_injective.ne <| Subtype.val_injective.ne hnxb])
    obtain ⟨_, hG2⟩ := hMaximal _ <| left_lt_sup.mpr (by
      rwa [edge_le_iff (v := a.1.1) (w := c), adj_comm, not_or])
    have hcnex : c ≠ x.val.val := by rintro rfl; exact hc.2 hxa
    obtain ⟨Mcon, hMcon⟩ := tutte_exists_isPerfectMatching_of_near_matchings hxa
      hxb hnadjxb (fun hadj ↦ hc.2 hadj.symm) (by lia) hcnex.symm hc.1 hbnec hG1 hG2
    exact hMatchingFree Mcon hMcon

Premises used: Iff.mpr, Subtype.coe_prop, SimpleGraph.Subgraph.induce_adj, SimpleGraph.Subgraph.verts_top, SimpleGraph.Subgraph.coe_adj, SimpleGraph.exists_maximal_isMatchingFree, Function.Embedding.coe_subtype, SimpleGraph.IsTutteViolator, SimpleGraph.ConnectedComponent.toSimpleGraph, Nat.card_coe_set_eq, left_lt_sup, Set.toFinset_card, ne_eq, Set.ncard_eq_toFinset_card', SimpleGraph.comap_adj, SimpleGraph.Subgraph.induce_verts, nonempty_fintype, SimpleGraph.Subgraph.top_adj, SimpleGraph.universalVerts, Not, SimpleGraph.deleteUniversalVerts, Fintype.card_eq_nat_card, true_and