awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h_1 : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents
    (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 :
  M1.verts =
      Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
          Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents ∪
        t ∧
    M1.IsMatching
complMatch : (K : G.deleteUniversalVerts.coe.ConnectedComponent) → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
    (complMatch K).verts = Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ (K : G.deleteUniversalVerts.coe.ConnectedComponent), complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
h : v ∉ M1.verts
h₁ :
  v ∈
    (fun (a : { x : V // x ∈ Set.univ \ G.universalVerts }) ↦ (↑a : V)) ''
        (G.deleteUniversalVerts.coe.connectedComponentMk
            (Subtype.mk (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) v hv)).supp \
      M1.verts
⊢ ∃ (i : G.deleteUniversalVerts.coe.ConnectedComponent),
    v ∈ (fun (a : { x : V // x ∈ Set.univ \ G.universalVerts }) ↦ (↑a : V)) '' i.supp \ M1.verts

Tactic:
use G.deleteUniversalVerts.coe.connectedComponentMk ⟨v, hv⟩

Premises used: SimpleGraph.connectedComponentMk, Subtype.mk, SimpleGraph.Subgraph.coe, SimpleGraph.deleteUniversalVerts
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h_1 : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents
    (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 :
  M1.verts =
      Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
          Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents ∪
        t ∧
    M1.IsMatching
complMatch : (K : G.deleteUniversalVerts.coe.ConnectedComponent) → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
    (complMatch K).verts = Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ (K : G.deleteUniversalVerts.coe.ConnectedComponent), complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
h : v ∉ M1.verts
⊢ v ∈
    (fun (a : { x : V // x ∈ Set.univ \ G.universalVerts }) ↦ (↑a : V)) ''
        (G.deleteUniversalVerts.coe.connectedComponentMk
            (Subtype.mk (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) v hv)).supp \
      M1.verts

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents
    (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 :
  M1.verts =
      Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
          Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents ∪
        t ∧
    M1.IsMatching
complMatch : (K : G.deleteUniversalVerts.coe.ConnectedComponent) → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
    (complMatch K).verts = Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ (K : G.deleteUniversalVerts.coe.ConnectedComponent), complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
⊢ (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts

Tactic:
have : (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts := by
    rw [Set.compl_subset_comm, Set.compl_eq_univ_diff]
    intro v hv
    by_cases h : v ∈ M1.verts
    · exact M1.verts.mem_union_left _ h
    right
    simp only [deleteUniversalVerts_verts, Subgraph.verts_iSup, Set.mem_iUnion, M2,
      hcomplMatch_compl]
    use G.deleteUniversalVerts.coe.connectedComponentMk ⟨v, hv⟩
    aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents
    (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 :
  M1.verts =
      Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
          Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents ∪
        t ∧
    M1.IsMatching
complMatch : (K : G.deleteUniversalVerts.coe.ConnectedComponent) → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
    (complMatch K).verts = Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ (K : G.deleteUniversalVerts.coe.ConnectedComponent), complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
this : (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts
⊢ ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts

Tactic:
⟨M1 ⊔ M2, hM1.2.sup hM2 disjointM12, this⟩

Premises used: SimpleGraph.Subgraph.IsMatching.sup, And.right, Max.max, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents
    (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 :
  M1.verts =
      Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
          Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents ∪
        t ∧
    M1.IsMatching
complMatch : (K : G.deleteUniversalVerts.coe.ConnectedComponent) → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
    (complMatch K).verts = Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ (K : G.deleteUniversalVerts.coe.ConnectedComponent), complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
this : (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts
⊢ ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts

Tactic:
exact ⟨M1 ⊔ M2, hM1.2.sup hM2 disjointM12, this⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
intro : ∀ (val : Fintype V), ∃ (M : G.Subgraph), M.IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching

Tactic:
cases nonempty_fintype V

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
intro :
  ∀ (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts), ∃ (M : G.Subgraph), M.IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching

Tactic:
obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'

Premises used: _private.0.SimpleGraph.Subgraph.IsMatching.exists_verts_compl_subset_universalVerts
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
⊢ Even M.vertsᶜ.ncard

Tactic:
simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card

Premises used: Set.even_ncard_compl_iff, Set.toFinset_card, Set.ncard_eq_toFinset_card', SimpleGraph.Subgraph.IsMatching.even_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
intro : ∀ (M' : G.Subgraph) (hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching), ∃ (M : G.Subgraph), M.IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching

Tactic:
obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
    (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card)

Premises used: SimpleGraph.IsClique.even_iff_exists_isMatching, Set.toFinite, Iff.mp, SimpleGraph.isClique_universalVerts, SimpleGraph.IsClique.subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching

Tactic:
⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩

Premises used: SimpleGraph.Subgraph.IsMatching.sup, And.right, Max.max, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
intro : Disjoint M.support M'.support
intro₁ : (M ⊔ M').IsSpanning
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching

Tactic:
refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
⊢ Disjoint M.support M'.support

Tactic:
simp [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, disjoint_compl_right]

Premises used: And.right, And.left, disjoint_compl_right, SimpleGraph.Subgraph.IsMatching.support_eq_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
intro : M.verts ∪ M.vertsᶜ = Set.univ
⊢ (M ⊔ M').IsSpanning

Tactic:
rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]

Premises used: SimpleGraph.Subgraph.verts_sup, And.left, SimpleGraph.Subgraph.isSpanning_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
⊢ M.verts ∪ M.vertsᶜ = Set.univ

Tactic:
M.verts.union_compl_self

Premises used: Set.union_compl_self, SimpleGraph.Subgraph.verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
⊢ M.verts ∪ M.vertsᶜ = Set.univ

Tactic:
exact M.verts.union_compl_self

Premises used: Set.union_compl_self, SimpleGraph.Subgraph.verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
intro : ∀ (val : Fintype V), ∃ (M : G.Subgraph), M.IsPerfectMatching
intro₁ :
  ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts),
    ∃ (M : G.Subgraph), M.IsPerfectMatching
intro₂ :
  ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts) (M' : G.Subgraph)
    (hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching), ∃ (M : G.Subgraph), M.IsPerfectMatching
intro₃ :
  ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts) (M' : G.Subgraph)
    (hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching), Disjoint M.support M'.support
intro₄ intro₅ :
  ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts) (M' : G.Subgraph)
    (hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching), (M ⊔ M').IsSpanning
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching

Tactic:
classical
  cases nonempty_fintype V
  obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
  obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
    (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card)
  refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
  · simp [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, disjoint_compl_right]
  · rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
    exact M.verts.union_compl_self

Premises used: SimpleGraph.Subgraph.verts_sup, _private.0.SimpleGraph.Subgraph.IsMatching.exists_verts_compl_subset_universalVerts, nonempty_fintype, disjoint_compl_right, SimpleGraph.Subgraph.isSpanning_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hodd : Odd (Nat.card V)
rw :
  0 <
    Set.ncard.{u_1} (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ ∅)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ ∅)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ ∅)))
⊢ G.IsTutteViolator ∅

Tactic:
rw [IsTutteViolator, Set.ncard_empty]

Premises used: Set.ncard_empty, SimpleGraph.IsTutteViolator
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hodd : Odd (Nat.card V)
⊢ Odd (Nat.card.{u_1} (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ ∅)) : Type u_1))

Tactic:
simpa using hodd
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hodd : Odd (Nat.card V)
⊢ 0 <
    Set.ncard.{u_1} (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ ∅)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ ∅)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ ∅)))

Tactic:
exact ((odd_ncard_oddComponents _).mpr <| by simpa using hodd).pos

Premises used: Iff.mpr, Odd.pos, SimpleGraph.odd_ncard_oddComponents
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
choose :
  ∀ (f : (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) → V)
    (hf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), f c ∈ u)
    (g :
      (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) →
        (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
    (hgf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), M.Adj (↑(g c) : V) (f c))
    (hg :
      ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)),
        g c ∈ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp),
    ¬G.IsTutteViolator u
⊢ ¬G.IsTutteViolator u

Tactic:
choose f hf g hgf hg using ConnectedComponent.odd_matches_node_outside hM (u := u)

Premises used: SimpleGraph.ConnectedComponent.odd_matches_node_outside
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) → V
hf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), f c ∈ u
g :
  (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) →
    (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)
hgf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), M.Adj (↑(g c) : V) (f c)
hg :
  ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)),
    g c ∈ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
c d : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
hcd : f c = f d
⊢ g c = g d

Tactic:
replace hcd : g c = g d := Subtype.val_injective <| hM.1.eq_of_adj_right (hgf c) (hcd ▸ hgf d)
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) → V
hf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), f c ∈ u
g :
  (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) →
    (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)
hgf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), M.Adj (↑(g c) : V) (f c)
hg :
  ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)),
    g c ∈ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
c d : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
hcd : g c = g d
⊢ c = d

Tactic:
Subtype.val_injective <| ConnectedComponent.eq_of_common_vertex (hg c) (hcd ▸ hg d)

Premises used: Subtype.val_injective, Eq.rec, SimpleGraph.ConnectedComponent.eq_of_common_vertex, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) → V
hf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), f c ∈ u
g :
  (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) →
    (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)
hgf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), M.Adj (↑(g c) : V) (f c)
hg :
  ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)),
    g c ∈ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
c d : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
hcd : g c = g d
⊢ c = d

Tactic:
exact Subtype.val_injective <| ConnectedComponent.eq_of_common_vertex (hg c) (hcd ▸ hg d)

Premises used: Subtype.val_injective, SimpleGraph.ConnectedComponent.eq_of_common_vertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) → V
hf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), f c ∈ u
g :
  (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) →
    (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)
hgf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), M.Adj (↑(g c) : V) (f c)
hg :
  ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)),
    g c ∈ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
⊢ Function.Injective f

Tactic:
have hfinj : f.Injective := fun c d hcd ↦ by
    replace hcd : g c = g d := Subtype.val_injective <| hM.1.eq_of_adj_right (hgf c) (hcd ▸ hgf d)
    exact Subtype.val_injective <| ConnectedComponent.eq_of_common_vertex (hg c) (hcd ▸ hg d)
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) → V
hf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), f c ∈ u
g :
  (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) →
    (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)
hgf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), M.Adj (↑(g c) : V) (f c)
hg :
  ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)),
    g c ∈ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hfinj : Function.Injective f
c d : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
⊢ Eq.{u_1 + 1} (α := (↑u : Type u_1))
      ((fun (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) ↦
          Subtype.mk (p := fun (x : V) ↦ x ∈ u) (f c) ⋯)
        c)
      ((fun (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) ↦
          Subtype.mk (p := fun (x : V) ↦ x ∈ u) (f c) ⋯)
        d) →
    c = d

Tactic:
simp [hfinj.eq_iff]

Premises used: Function.Injective.eq_iff