awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
neg :
  ∀
    (w :
      (Gmax ⊔
          edge (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
            (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)).Subgraph)
    (hG1 : w.IsPerfectMatching), False
⊢ False

Tactic:
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])

Premises used: Iff.mpr, left_lt_sup
-- 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_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))
rwa₂ rwa₃ rwa₄ 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

Tactic:
rwa [edge_le_iff (v := a.1.1) (w := c), adj_comm, not_or]

Premises used: not_or, SimpleGraph.edge_le_iff, SimpleGraph.adj_comm
-- 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_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
neg :
  ∀ (w : (Gmax ⊔ edge (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) c).Subgraph)
    (hG2 : w.IsPerfectMatching), False
⊢ False

Tactic:
obtain ⟨_, hG2⟩ := hMaximal _ <| left_lt_sup.mpr (by
      rwa [edge_le_iff (v := a.1.1) (w := c), adj_comm, not_or])

Premises used: Iff.mpr, left_lt_sup
-- 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_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)
w :
  (Gmax ⊔
      edge (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)).Subgraph
hG1 : w.IsPerfectMatching
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠
      (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ∧
    ¬Gmax.Adj (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
hbnec :
  (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠
    (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
w_1 :
  (Gmax ⊔
      edge (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)).Subgraph
hG2 : w_1.IsPerfectMatching
⊢ False

Tactic:
hc.2 hxa

Premises used: And.right
-- 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_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)
w :
  (Gmax ⊔
      edge (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)).Subgraph
hG1 : w.IsPerfectMatching
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠
      (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ∧
    ¬Gmax.Adj (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
hbnec :
  (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠
    (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
w_1 :
  (Gmax ⊔
      edge (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)).Subgraph
hG2 : w_1.IsPerfectMatching
⊢ False

Tactic:
exact hc.2 hxa

Premises used: And.right
-- 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_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
⊢ c ≠ (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)

Tactic:
have hcnex : c ≠ x.val.val := by rintro rfl; exact hc.2 hxa
-- 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_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)
⊢ (↑(↑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)

Tactic:
lia
-- 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_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)
neg : ∀ (Mcon : Gmax.Subgraph) (hMcon : Mcon.IsPerfectMatching), False
⊢ 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

Premises used: SimpleGraph.Adj.symm, Ne.symm, And.right, And.left, _private.0.SimpleGraph.tutte_exists_isPerfectMatching_of_near_matchings
-- 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_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)
Mcon : Gmax.Subgraph
hMcon : Mcon.IsPerfectMatching
⊢ False

Tactic:
hMatchingFree Mcon hMcon
-- 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_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)
Mcon : Gmax.Subgraph
hMcon : Mcon.IsPerfectMatching
⊢ False

Tactic:
exact hMatchingFree Mcon hMcon
-- 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), ¬G.IsTutteViolator u

Tactic:
apply not_isTutteViolator_of_isPerfectMatching hM

Premises used: SimpleGraph.not_isTutteViolator_of_isPerfectMatching
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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

Tactic:
refine ⟨by rintro ⟨M, hM⟩; apply not_isTutteViolator_of_isPerfectMatching hM, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
contrapose! : (∀ (M : G.Subgraph), ¬M.IsPerfectMatching) → ∃ (u : Set V), G.IsTutteViolator u
⊢ (∀ (u : Set V), ¬G.IsTutteViolator u) → ∃ (M : G.Subgraph), M.IsPerfectMatching

Tactic:
contrapose!