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 :
  ¬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
neg :
  ∀ (x y : (↑K.supp : Type u_1))
    (hxy :
      x ≠ y ∧
        ¬Gmax.deleteUniversalVerts.coe.Adj (↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
            (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))),
    False
⊢ False

Tactic:
obtain ⟨x, y, hxy⟩ := (not_isClique_iff _).mp hK

Premises used: Iff.mp, SimpleGraph.not_isClique_iff
-- 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)
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x y : (↑K.supp : Type u_1)
hxy :
  x ≠ y ∧
    ¬Gmax.deleteUniversalVerts.coe.Adj (↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
        (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
neg : ∀ (p : K.toSimpleGraph.Walk x y) (hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x y), False
⊢ False

Tactic:
obtain ⟨p, hp⟩ := Reachable.exists_path_of_dist (K.connected_toSimpleGraph x y)

Premises used: SimpleGraph.Connected.preconnected, SimpleGraph.ConnectedComponent.connected_toSimpleGraph, SimpleGraph.Reachable.exists_path_of_dist
-- 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)
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x y : (↑K.supp : Type u_1)
hxy :
  x ≠ y ∧
    ¬Gmax.deleteUniversalVerts.coe.Adj (↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
        (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
p : K.toSimpleGraph.Walk x y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x y
neg :
  ∀ (x a b : ↥K) (hxa : K.toSimpleGraph.Adj x a) (hxb : K.toSimpleGraph.Adj a b) (hnadjxb : ¬K.toSimpleGraph.Adj x b)
    (hnxb : x ≠ b), False
⊢ False

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

Premises used: SimpleGraph.Walk.exists_adj_adj_not_adj_ne, SimpleGraph.Reachable.one_lt_dist_of_ne_of_not_adj, SimpleGraph.Walk.reachable, And.right, And.left
-- 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)
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
hxa : K.toSimpleGraph.Adj x a
hxb : K.toSimpleGraph.Adj a b
hnadjxb : ¬K.toSimpleGraph.Adj x b
hnxb : x ≠ b
⊢ 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)

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

Premises used: Subtype.coe_prop, SimpleGraph.Subgraph.induce_adj, SimpleGraph.Subgraph.verts_top, SimpleGraph.Subgraph.coe_adj, Function.Embedding.coe_subtype, SimpleGraph.ConnectedComponent.toSimpleGraph, ne_eq, SimpleGraph.comap_adj, SimpleGraph.Subgraph.induce_verts, SimpleGraph.Subgraph.top_adj, SimpleGraph.universalVerts, SimpleGraph.deleteUniversalVerts, true_and
-- 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)
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
hxa : K.toSimpleGraph.Adj x a
hxb : K.toSimpleGraph.Adj a b
hnadjxb : ¬K.toSimpleGraph.Adj x b
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)
⊢ 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)

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

Premises used: Subtype.coe_prop, SimpleGraph.Subgraph.induce_adj, SimpleGraph.Subgraph.verts_top, SimpleGraph.Subgraph.coe_adj, Function.Embedding.coe_subtype, SimpleGraph.ConnectedComponent.toSimpleGraph, ne_eq, SimpleGraph.comap_adj, SimpleGraph.Subgraph.induce_verts, SimpleGraph.Subgraph.top_adj, SimpleGraph.universalVerts, SimpleGraph.deleteUniversalVerts, true_and
-- 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)
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
hxa : K.toSimpleGraph.Adj x a
hxb : K.toSimpleGraph.Adj a b
hnadjxb : ¬K.toSimpleGraph.Adj x b
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)
⊢ ¬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)

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

Premises used: Subtype.coe_prop, SimpleGraph.Subgraph.induce_adj, SimpleGraph.Subgraph.verts_top, SimpleGraph.Subgraph.coe_adj, Function.Embedding.coe_subtype, SimpleGraph.ConnectedComponent.toSimpleGraph, ne_eq, SimpleGraph.comap_adj, SimpleGraph.Subgraph.induce_verts, SimpleGraph.Subgraph.top_adj, SimpleGraph.universalVerts, SimpleGraph.deleteUniversalVerts, true_and
-- 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)
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),
    (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c ∧
      ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)

Tactic:
simpa [universalVerts] using a.1.2.2

Premises used: And.right, SimpleGraph.universalVerts, Subtype.val, Subtype.property
-- 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)
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)
neg :
  ∀ (c : V)
    (hc :
      (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c ∧
        ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)),
    False
⊢ False

Tactic:
obtain ⟨c, hc⟩ : ∃ (c : V), (a : V) ≠ c ∧ ¬ Gmax.Adj c a := by
      simpa [universalVerts] using a.1.2.2

Premises used: Subtype.val
-- 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)
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠
      (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ∧
    ¬Gmax.Adj (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
⊢ False

Tactic:
hc.2 hxb.symm

Premises used: SimpleGraph.Adj.symm, 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)
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠
      (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ∧
    ¬Gmax.Adj (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
⊢ False

Tactic:
exact hc.2 hxb.symm

Premises used: SimpleGraph.Adj.symm, 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)
⊢ (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c

Tactic:
have hbnec : b.val.val ≠ c := by rintro rfl; exact hc.2 hxb.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)
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
rw :
  ¬((↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) =
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ∨
      Gmax.Adj (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V))
⊢ ¬edge (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≤
      Gmax

Tactic:
rw [edge_le_iff (v := x.1.1) (w := b.1.1)]

Premises used: SimpleGraph.edge_le_iff
-- 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
⊢ ¬((↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) =
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ∨
      Gmax.Adj (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V))

Tactic:
simp [hnadjxb, Subtype.val_injective.ne <| Subtype.val_injective.ne hnxb]

Premises used: Subtype.val_injective, Function.Injective.ne