awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc_1 :
  ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
      Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x_1 y : (↑K.supp : Type u_1)
hxy :
  x_1 ≠ y ∧
    ¬Gmax.deleteUniversalVerts.coe.Adj (↑x_1 : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
        (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
p : K.toSimpleGraph.Walk x_1 y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x_1 y
x a b : ↥K
hnxb : x ≠ b
hxa :
  Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hxb :
  Gmax.Adj (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hnadjxb :
  ¬Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
      (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
c : V
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c ∧
    ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
hbnec : (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c
w :
  (Gmax ⊔
      edge (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)).Subgraph
hG1 : w.IsPerfectMatching
rwa :
  ¬((↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) = c ∨
      Gmax.Adj (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) c)
⊢ ¬edge (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) c ≤ Gmax
have rwa₁ : ¬((↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) = c ∨
    Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V))
Tactic: rwa [edge_le_iff (v := a.1.1) (w := c), adj_comm, not_or]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc_1 :
  ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
      Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x_1 y : (↑K.supp : Type u_1)
hxy :
  x_1 ≠ y ∧
    ¬Gmax.deleteUniversalVerts.coe.Adj (↑x_1 : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
        (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
p : K.toSimpleGraph.Walk x_1 y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x_1 y
x a b : ↥K
hnxb : x ≠ b
hxa :
  Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hxb :
  Gmax.Adj (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hnadjxb :
  ¬Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
      (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
c : V
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c ∧
    ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
hbnec : (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c
w :
  (Gmax ⊔
      edge (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)).Subgraph
hG1 : w.IsPerfectMatching
rwa :
  ¬((↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) = c ∨
      Gmax.Adj (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) c)
rwa₁ :
  ¬((↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) = c ∨
      Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V))
⊢ ¬edge (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) c ≤ Gmax
have rwa₂ : ¬(↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) = c ∧
  ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
Tactic: rwa [edge_le_iff (v := a.1.1) (w := c), adj_comm, not_or]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc_1 :
  ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
      Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x_1 y : (↑K.supp : Type u_1)
hxy :
  x_1 ≠ y ∧
    ¬Gmax.deleteUniversalVerts.coe.Adj (↑x_1 : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
        (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
p : K.toSimpleGraph.Walk x_1 y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x_1 y
x a b : ↥K
hnxb : x ≠ b
hxa :
  Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hxb :
  Gmax.Adj (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hnadjxb :
  ¬Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
      (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
c : V
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c ∧
    ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
hbnec : (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c
w :
  (Gmax ⊔
      edge (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)).Subgraph
hG1 : w.IsPerfectMatching
⊢ False
have neg : ∀ (w : (Gmax ⊔ edge (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) c).Subgraph)
  (hG2 : w.IsPerfectMatching), False
Tactic: obtain ⟨_, hG2⟩ := hMaximal _ <| left_lt_sup.mpr (by
      rwa [edge_le_iff (v := a.1.1) (w := c), adj_comm, not_or])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc_1 :
  ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
      Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x_1 y : (↑K.supp : Type u_1)
hxy :
  x_1 ≠ y ∧
    ¬Gmax.deleteUniversalVerts.coe.Adj (↑x_1 : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
        (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
p : K.toSimpleGraph.Walk x_1 y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x_1 y
x a b : ↥K
hnxb : x ≠ b
hxa :
  Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hxb :
  Gmax.Adj (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hnadjxb :
  ¬Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
      (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
c : V
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c ∧
    ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
hbnec : (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c
w :
  (Gmax ⊔
      edge (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)).Subgraph
hG1 : w.IsPerfectMatching
w_1 : (Gmax ⊔ edge (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) c).Subgraph
hG2 : w_1.IsPerfectMatching
⊢ False
have hcnex : c ≠ (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
Tactic: have hcnex : c ≠ x.val.val := by rintro rfl; exact hc.2 hxa
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc_1 :
  ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
      Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x_1 y : (↑K.supp : Type u_1)
hxy :
  x_1 ≠ y ∧
    ¬Gmax.deleteUniversalVerts.coe.Adj (↑x_1 : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
        (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
p : K.toSimpleGraph.Walk x_1 y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x_1 y
x a b : ↥K
hnxb : x ≠ b
hxa :
  Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hxb :
  Gmax.Adj (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hnadjxb :
  ¬Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
      (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
c : V
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c ∧
    ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
hbnec : (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c
w :
  (Gmax ⊔
      edge (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)).Subgraph
hG1 : w.IsPerfectMatching
w_1 : (Gmax ⊔ edge (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) c).Subgraph
hG2 : w_1.IsPerfectMatching
hcnex : c ≠ (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
⊢ False
have neg : ∀ (Mcon : Gmax.Subgraph) (hMcon : Mcon.IsPerfectMatching), False
Tactic: 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
⊢ ∃ (u : Set V), G.IsTutteViolator u
have intro : ∀ (val : Fintype V), ∃ (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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
⊢ ∃ (u : Set V), G.IsTutteViolator u
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
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
⊢ ∃ (u : Set V), G.IsTutteViolator u
have 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
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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
⊢ (∃ (M : G.Subgraph), M.IsPerfectMatching) ↔ ∀ (u : Set V), ¬G.IsTutteViolator u
have refine : (∀ (u : Set V), ¬G.IsTutteViolator u) → ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: refine ⟨by rintro ⟨M, hM⟩; apply not_isTutteViolator_of_isPerfectMatching hM, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
⊢ (∀ (u : Set V), ¬G.IsTutteViolator u) → ∃ (M : G.Subgraph), M.IsPerfectMatching
have contrapose! : (∀ (M : G.Subgraph), ¬M.IsPerfectMatching) → ∃ (u : Set V), G.IsTutteViolator u
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
⊢ ∃ (u : Set V), G.IsTutteViolator u
have pos : ∀ (hvOdd : Odd (Nat.card V)), ∃ (u : Set V), G.IsTutteViolator u
Tactic: by_cases hvOdd : Odd (Nat.card V)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
pos : ∀ (hvOdd : Odd (Nat.card V)), ∃ (u : Set V), G.IsTutteViolator u
⊢ ∃ (u : Set V), G.IsTutteViolator u
have neg : ∀ (hvOdd : ¬Odd (Nat.card V)), ∃ (u : Set V), G.IsTutteViolator u
Tactic: by_cases hvOdd : Odd (Nat.card V)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
⊢ (∃ (M : G.Subgraph), M.IsPerfectMatching) ↔ ∀ (u : Set V), ¬G.IsTutteViolator u
have refine : (∀ (u : Set V), ¬G.IsTutteViolator u) → ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: classical
  refine ⟨by rintro ⟨M, hM⟩; apply not_isTutteViolator_of_isPerfectMatching hM, ?_⟩
  contrapose!
  intro h
  by_cases hvOdd : Odd (Nat.card V)
  · exact ⟨∅, .empty hvOdd⟩
  · exact exists_isTutteViolator h (Nat.not_odd_iff_even.mp hvOdd)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
refine : (∀ (u : Set V), ¬G.IsTutteViolator u) → ∃ (M : G.Subgraph), M.IsPerfectMatching
⊢ (∃ (M : G.Subgraph), M.IsPerfectMatching) ↔ ∀ (u : Set V), ¬G.IsTutteViolator u
have refine₁ : (∀ (M : G.Subgraph), ¬M.IsPerfectMatching) → ∃ (u : Set V), G.IsTutteViolator u
Tactic: classical
  refine ⟨by rintro ⟨M, hM⟩; apply not_isTutteViolator_of_isPerfectMatching hM, ?_⟩
  contrapose!
  intro h
  by_cases hvOdd : Odd (Nat.card V)
  · exact ⟨∅, .empty hvOdd⟩
  · exact exists_isTutteViolator h (Nat.not_odd_iff_even.mp hvOdd)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
refine : (∀ (u : Set V), ¬G.IsTutteViolator u) → ∃ (M : G.Subgraph), M.IsPerfectMatching
refine₁ refine₂ : ∀ (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching), ∃ (u : Set V), G.IsTutteViolator u
⊢ (∃ (M : G.Subgraph), M.IsPerfectMatching) ↔ ∀ (u : Set V), ¬G.IsTutteViolator u
have pos : ∀ (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching) (hvOdd : Odd (Nat.card V)), ∃ (u : Set V), G.IsTutteViolator u
Tactic: classical
  refine ⟨by rintro ⟨M, hM⟩; apply not_isTutteViolator_of_isPerfectMatching hM, ?_⟩
  contrapose!
  intro h
  by_cases hvOdd : Odd (Nat.card V)
  · exact ⟨∅, .empty hvOdd⟩
  · exact exists_isTutteViolator h (Nat.not_odd_iff_even.mp hvOdd)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
refine : (∀ (u : Set V), ¬G.IsTutteViolator u) → ∃ (M : G.Subgraph), M.IsPerfectMatching
refine₁ refine₂ : ∀ (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching), ∃ (u : Set V), G.IsTutteViolator u
pos : ∀ (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching) (hvOdd : Odd (Nat.card V)), ∃ (u : Set V), G.IsTutteViolator u
⊢ (∃ (M : G.Subgraph), M.IsPerfectMatching) ↔ ∀ (u : Set V), ¬G.IsTutteViolator u
have neg : ∀ (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching) (hvOdd : ¬Odd (Nat.card V)), ∃ (u : Set V), G.IsTutteViolator u
Tactic: classical
  refine ⟨by rintro ⟨M, hM⟩; apply not_isTutteViolator_of_isPerfectMatching hM, ?_⟩
  contrapose!
  intro h
  by_cases hvOdd : Odd (Nat.card V)
  · exact ⟨∅, .empty hvOdd⟩
  · exact exists_isTutteViolator h (Nat.not_odd_iff_even.mp hvOdd)