awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc :
  ¬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
⊢ False
have 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)))
Tactic: simp_rw [Fintype.card_eq_nat_card, Nat.card_coe_set_eq] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
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)))
⊢ False
have 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
Tactic: push Not at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
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
⊢ False
have pos : ∀ (M : Gmax.Subgraph) (hM : M.IsPerfectMatching), False
Tactic: obtain ⟨M, hM⟩ := Subgraph.IsPerfectMatching.exists_of_isClique_supp hvEven
      (by simpa [IsTutteViolator] using hc) h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc :
  ¬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
⊢ False
have neg : ∀ (K : Gmax.deleteUniversalVerts.coe.ConnectedComponent) (hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp), False
Tactic: obtain ⟨K, hK⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc :
  ¬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
⊢ False
have 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
Tactic: obtain ⟨x, y, hxy⟩ := (not_isClique_iff _).mp hK
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc :
  ¬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))
⊢ False
have neg : ∀ (p : K.toSimpleGraph.Walk x y) (hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x y), False
Tactic: obtain ⟨p, hp⟩ := Reachable.exists_path_of_dist (K.connected_toSimpleGraph x y)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc :
  ¬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
⊢ False
have 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
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)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc :
  ¬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
⊢ False
have 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)
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
Cleared hypotheses: hxa, hxb, hnadjxb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc :
  ¬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)
⊢ False
have 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)
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
Cleared hypotheses: hxa, hxb, hnadjxb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc :
  ¬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)
⊢ False
have 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)
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
Cleared hypotheses: hxa, hxb, hnadjxb
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc :
  ¬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)
⊢ False
have 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
Tactic: obtain ⟨c, hc⟩ : ∃ (c : V), (a : V) ≠ c ∧ ¬ Gmax.Adj c a := by
      simpa [universalVerts] using a.1.2.2
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc_1 :
  ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
      Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x_1 y : (↑K.supp : Type u_1)
hxy :
  x_1 ≠ y ∧
    ¬Gmax.deleteUniversalVerts.coe.Adj (↑x_1 : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
        (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
p : K.toSimpleGraph.Walk x_1 y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x_1 y
x a b : ↥K
hnxb : x ≠ b
hxa :
  Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hxb :
  Gmax.Adj (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hnadjxb :
  ¬Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
      (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
c : V
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c ∧
    ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
⊢ False
have hbnec : (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c
Tactic: have hbnec : b.val.val ≠ c := by rintro rfl; exact hc.2 hxb.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc_1 :
  ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
      Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x_1 y : (↑K.supp : Type u_1)
hxy :
  x_1 ≠ y ∧
    ¬Gmax.deleteUniversalVerts.coe.Adj (↑x_1 : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
        (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
p : K.toSimpleGraph.Walk x_1 y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x_1 y
x a b : ↥K
hnxb : x ≠ b
hxa :
  Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hxb :
  Gmax.Adj (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hnadjxb :
  ¬Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
      (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
c : V
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c ∧
    ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
hbnec : (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c
⊢ ¬edge (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≤
      Gmax
have 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))
Tactic: rw [edge_le_iff (v := x.1.1) (w := b.1.1)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc_1 :
  ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
      Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x_1 y : (↑K.supp : Type u_1)
hxy :
  x_1 ≠ y ∧
    ¬Gmax.deleteUniversalVerts.coe.Adj (↑x_1 : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
        (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
p : K.toSimpleGraph.Walk x_1 y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x_1 y
x a b : ↥K
hnxb : x ≠ b
hxa :
  Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hxb :
  Gmax.Adj (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hnadjxb :
  ¬Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
      (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
c : V
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c ∧
    ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
hbnec : (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c
⊢ False
have 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
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])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvEven : Even (Nat.card V)
val : Fintype V
Gmax : SimpleGraph V
hSubgraph : G ≤ Gmax
hMatchingFree : Gmax.IsMatchingFree
hMaximal : ∀ G' > Gmax, ∃ (M : G'.Subgraph), M.IsPerfectMatching
hc_1 :
  ¬Fintype.card.{u_1} (↑Gmax.universalVerts : Type u_1) <
      Fintype.card.{u_1} (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ Gmax.universalVerts))) : Type u_1)
K : Gmax.deleteUniversalVerts.coe.ConnectedComponent
hK : ¬Gmax.deleteUniversalVerts.coe.IsClique K.supp
x_1 y : (↑K.supp : Type u_1)
hxy :
  x_1 ≠ y ∧
    ¬Gmax.deleteUniversalVerts.coe.Adj (↑x_1 : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
        (↑y : (↑Gmax.deleteUniversalVerts.verts : Type u_1))
p : K.toSimpleGraph.Walk x_1 y
hp : p.IsPath ∧ p.length = K.toSimpleGraph.dist x_1 y
x a b : ↥K
hnxb : x ≠ b
hxa :
  Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hxb :
  Gmax.Adj (↑(↑a : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
    (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
hnadjxb :
  ¬Gmax.Adj (↑(↑x : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
      (↑(↑b : (↑(Set.univ \ {v : V | ∀ ⦃w : V⦄, ¬v = w → Gmax.Adj w v}) : Type u_1)) : V)
c : V
hc :
  (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c ∧
    ¬Gmax.Adj c (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
hbnec : (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) ≠ c
w :
  (Gmax ⊔
      edge (↑(↑x : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)
        (↑(↑b : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V)).Subgraph
hG1 : w.IsPerfectMatching
⊢ ¬edge (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) c ≤ Gmax
have rwa : ¬((↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) = c ∨
    Gmax.Adj (↑(↑a : (↑Gmax.deleteUniversalVerts.verts : Type u_1)) : V) c)
Tactic: rwa [edge_le_iff (v := a.1.1) (w := c), adj_comm, not_or]