awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux :
  ∀ {x'_1 : V} (hx' : Membership.mem (γ := Set V) {x, x'} x'_1) (c' : V) (hc : c' ≠ a)
    (hadj : p.toSubgraph.Adj c' x'_1), M2.Adj c' x'_1
h : ∀ (G' : SimpleGraph V), G'.Adj x' x
| ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x x' ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
enter [1, G', 2, 2, 1, 1]
      rw [adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux :
  ∀ {x'_1 : V} (hx' : Membership.mem (γ := Set V) {x, x'} x'_1) (c' : V) (hc : c' ≠ a)
    (hadj : p.toSubgraph.Adj c' x'_1), M2.Adj c' x'_1
neg :
  ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x' x ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x x' ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
conv =>
      enter [1, G', 2, 2, 1, 1]
      rw [adj_comm]

Premises used: SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux :
  ∀ {x'_1 : V} (hx' : Membership.mem (γ := Set V) {x, x'} x'_1) (c' : V) (hc : c' ≠ a)
    (hadj : p.toSubgraph.Adj c' x'_1), M2.Adj c' x'_1
⊢ ¬p.toSubgraph.Adj x' x

Tactic:
rw [Subgraph.adj_comm] at hnpxb

Premises used: SimpleGraph.Subgraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux :
  ∀ {x'_1 : V} (hx' : Membership.mem (γ := Set V) {x, x'} x'_1) (c' : V) (hc : c' ≠ a)
    (hadj : p.toSubgraph.Adj c' x'_1), M2.Adj c' x'_1
hnpxb₁ : ¬p.toSubgraph.Adj x' x
⊢ p.toSubgraph.spanningCoe ≤ G ⊔ edge a c

Tactic:
rw [Subgraph.adj_comm] at hnpxb

Premises used: SimpleGraph.Subgraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x x'
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux :
  ∀ {x'_1 : V} (hx' : Membership.mem (γ := Set V) {x, x'} x'_1) (c' : V) (hc : c' ≠ a)
    (hadj : p.toSubgraph.Adj c' x'_1), M2.Adj c' x'_1
hnpxb₁ : ¬p.toSubgraph.Adj x' x
hle₁ : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
⊢ ∀ {x'_1 : V} (hx' : Membership.mem (γ := Set V) {x, x'} x'_1) (c' : V) (hc : c' ≠ a)
    (hadj : p.toSubgraph.Adj c' x'_1), M2.Adj c' x'_1

Tactic:
rw [Subgraph.adj_comm] at hnpxb

Premises used: SimpleGraph.Subgraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x' x
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux :
  ∀ {x'_1 : V} (hx' : Membership.mem (γ := Set V) {x, x'} x'_1) (c' : V) (hc : c' ≠ a)
    (hadj : p.toSubgraph.Adj c' x'_1), M2.Adj c' x'_1
⊢ Membership.mem (γ := Set V) {x, x'} x'

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a c : V
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hnGac : ¬G.Adj a c
hnxc : x ≠ c
hnac : a ≠ c
hM2 : M2.IsPerfectMatching
hM2ac : M2.Adj a c
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V) (h : x' ≠ c), ¬M2.Adj x' a
x' : V
M1 : (G ⊔ edge x x').Subgraph
hab : G.Adj a x'
hnGxb : ¬G.Adj x x'
hnxb : x ≠ x'
hnbc : x' ≠ c
hM1 : M1.IsPerfectMatching
hM1xb : M1.Adj x x'
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x x' ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x x'
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x x'
induce_le :
  (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe (s := (↑(cycles.connectedComponentMk c) : Set V)) ≤
    G ⊔ edge a c ⊔ edge x x'
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x' x
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux :
  ∀ {x'_1 : V} (hx' : Membership.mem (γ := Set V) {x, x'} x'_1) (c' : V) (hc : c' ≠ a)
    (hadj : p.toSubgraph.Adj c' x'_1), M2.Adj c' x'_1
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x' x ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
exact tutte_exists_isAlternating_isCycles p hp hcalt (hnM2 _ hnbc) hpac hnpxb hM2ac
      hab.symm hnbc hxa.ne.symm hle (aux (by simp))

Premises used: SimpleGraph.Adj.symm, _private.0.SimpleGraph.tutte_exists_isAlternating_isCycles, SimpleGraph.Adj.ne, Ne.symm
-- 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
⊢ ∃ (u : Set V), G.IsTutteViolator u

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
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
intro :
  ∀ (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

Tactic:
obtain ⟨Gmax, hSubgraph, hMatchingFree, hMaximal⟩ := exists_maximal_isMatchingFree h

Premises used: SimpleGraph.exists_maximal_isMatchingFree
-- 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)
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:
⟨Gmax.universalVerts, .mono hSubgraph ?_⟩

Premises used: SimpleGraph.IsTutteViolator.mono, Exists.intro, SimpleGraph.universalVerts
-- 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)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
intro : Gmax.IsTutteViolator Gmax.universalVerts
⊢ ∃ (u : Set V), G.IsTutteViolator u

Tactic:
refine ⟨Gmax.universalVerts, .mono hSubgraph ?_⟩
-- 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)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
intro : ∀ (hc : ¬Gmax.IsTutteViolator Gmax.universalVerts), False
⊢ Gmax.IsTutteViolator Gmax.universalVerts

Tactic:
by_contra! hc
-- 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)
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
⊢ ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
      Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)

Tactic:
simp only [IsTutteViolator, Set.ncard_eq_toFinset_card', Set.toFinset_card] at hc

Premises used: SimpleGraph.IsTutteViolator, Set.toFinset_card, Set.ncard_eq_toFinset_card'
-- 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)
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)
pos :
  ∀ (h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp),
    False
neg :
  ∀ (h' : ∃ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp),
    False
⊢ False

Tactic:
by_cases! h' : ∀ (K : ConnectedComponent Gmax.deleteUniversalVerts.coe),
      Gmax.deleteUniversalVerts.coe.IsClique K.supp
-- 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)
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
⊢ ¬Nat.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
      Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)

Tactic:
rw [Fintype.card_eq_nat_card] at hc

Premises used: Fintype.card_eq_nat_card
-- 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)
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
hc₁ :
  ¬Nat.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), Gmax.deleteUniversalVerts.coe.IsClique K.supp

Tactic:
rw [Fintype.card_eq_nat_card] at hc

Premises used: Fintype.card_eq_nat_card
-- 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)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc :
  ¬Nat.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
⊢ ¬Gmax.universalVerts.ncard <
      Set.ncard (α :=
        ConnectedComponent (V :=
          (↑(Subgraph.verts (G := Gmax) (Subgraph.deleteVerts ⊤ Gmax.universalVerts)) : Type u_1))
          (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts)))
        (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts)))

Tactic:
simp_rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] at hc

Premises used: Nat.card_coe_set_eq, Fintype.card_eq_nat_card
-- 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)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
hc :
  ¬Gmax.universalVerts.ncard <
      Set.ncard (α :=
        ConnectedComponent (V :=
          (↑(Subgraph.verts (G := Gmax) (Subgraph.deleteVerts ⊤ Gmax.universalVerts)) : Type u_1))
          (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts)))
        (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts)))
⊢ Set.ncard (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := Gmax) (Subgraph.deleteVerts ⊤ Gmax.universalVerts)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) ≤
    Gmax.universalVerts.ncard

Tactic:
push Not at hc

Premises used: Not
-- 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)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
hc :
  Set.ncard (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := Gmax) (Subgraph.deleteVerts ⊤ Gmax.universalVerts)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) ≤
    Gmax.universalVerts.ncard
⊢ ¬Gmax.IsTutteViolator Gmax.universalVerts

Tactic:
simpa [IsTutteViolator] using hc

Premises used: SimpleGraph.IsTutteViolator
-- 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)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
hc :
  Set.ncard (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := Gmax) (Subgraph.deleteVerts ⊤ Gmax.universalVerts)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) ≤
    Gmax.universalVerts.ncard
pos : ∀ (M : Gmax.Subgraph) (hM : M.IsPerfectMatching), False
⊢ False

Tactic:
obtain ⟨M, hM⟩ := Subgraph.IsPerfectMatching.exists_of_isClique_supp hvEven
      (by simpa [IsTutteViolator] using hc) h'

Premises used: SimpleGraph.Subgraph.IsPerfectMatching.exists_of_isClique_supp
-- 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)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
hc :
  Set.ncard (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := Gmax) (Subgraph.deleteVerts ⊤ Gmax.universalVerts)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) ≤
    Gmax.universalVerts.ncard
M : Gmax.Subgraph
hM : M.IsPerfectMatching
⊢ False

Tactic:
hMatchingFree M hM
-- 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)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
h' : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent), Gmax.deleteUniversalVerts.coe.IsClique K.supp
hc :
  Set.ncard (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := Gmax) (Subgraph.deleteVerts ⊤ Gmax.universalVerts)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) ≤
    Gmax.universalVerts.ncard
M : Gmax.Subgraph
hM : M.IsPerfectMatching
⊢ False

Tactic:
exact hMatchingFree M hM
-- 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)
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
neg :
  ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent) (hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp), False
⊢ False

Tactic:
obtain ⟨K, hK⟩ := h'