awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h_1 : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents
    (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 :
  M1.verts =
      Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
          Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents ∪
        t ∧
    M1.IsMatching
complMatch : (K : G.deleteUniversalVerts.coe.ConnectedComponent) → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
    (complMatch K).verts = Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ (K : G.deleteUniversalVerts.coe.ConnectedComponent), complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
hv : v ∈ Set.univ \ G.universalVerts
h : v ∉ M1.verts
⊢ ∃ (i : G.deleteUniversalVerts.coe.ConnectedComponent),
    v ∈ (fun (a : { x : V // x ∈ Set.univ \ G.universalVerts }) ↦ (↑a : V)) '' i.supp \ M1.verts
have h₁ : v ∈
  (fun (a : { x : V // x ∈ Set.univ \ G.universalVerts }) ↦ (↑a : V)) ''
      (G.deleteUniversalVerts.coe.connectedComponentMk
          (Subtype.mk (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) v hv)).supp \
    M1.verts
Tactic: use G.deleteUniversalVerts.coe.connectedComponentMk ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents
    (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 :
  M1.verts =
      Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
          Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents ∪
        t ∧
    M1.IsMatching
complMatch : (K : G.deleteUniversalVerts.coe.ConnectedComponent) → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
    (complMatch K).verts = Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ (K : G.deleteUniversalVerts.coe.ConnectedComponent), complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
⊢ ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
have this : (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts
Tactic: have : (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts := by
    rw [Set.compl_subset_comm, Set.compl_eq_univ_diff]
    intro v hv
    by_cases h : v ∈ M1.verts
    · exact M1.verts.mem_union_left _ h
    right
    simp only [deleteUniversalVerts_verts, Subgraph.verts_iSup, Set.mem_iUnion, M2,
      hcomplMatch_compl]
    use G.deleteUniversalVerts.coe.connectedComponentMk ⟨v, hv⟩
    aesop
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
⊢ ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
have have : ∀
  (hrep :
    ConnectedComponent.Represents
      (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
      G.deleteUniversalVerts.coe.oddComponents),
  ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
Tactic: classical
  have hrep := ConnectedComponent.Represents.image_out G.deleteUniversalVerts.coe.oddComponents
  -- First we match one node from each odd component to a universal vertex
  obtain ⟨t, ht, M1, hM1⟩ := Subgraph.IsMatching.exists_of_universalVerts
      (disjoint_image_val_universalVerts _).symm (by
        simp only [IsTutteViolator, not_lt] at h
        rwa [Set.ncard_image_of_injective _ Subtype.val_injective, hrep.ncard_eq])
  -- Then we match all other nodes in components internally
  have exists_complMatch (K : G.deleteUniversalVerts.coe.ConnectedComponent) :
      ∃ M : Subgraph G, M.verts = Subtype.val '' K.supp \ M1.verts ∧ M.IsMatching := by
    have : G.IsClique (Subtype.val '' K.supp \ M1.verts) :=
      ((h' K).of_induce).subset Set.diff_subset
    rw [← this.even_iff_exists_isMatching (Set.toFinite _), hM1.1]
    exact even_ncard_image_val_supp_sdiff_image_val_rep_union _ ht hrep
  choose complMatch hcomplMatch_compl hcomplMatch_match using exists_complMatch
  let M2 : Subgraph G := ⨆ K, complMatch K
  have hM2 : M2.IsMatching := by
    refine .iSup hcomplMatch_match fun i j hij ↦ (?_ : Disjoint _ _)
    rw [(hcomplMatch_match i).support_eq_verts, hcomplMatch_compl i,
        (hcomplMatch_match j).support_eq_verts, hcomplMatch_compl j]
    exact Set.disjoint_of_subset Set.diff_subset Set.diff_subset <|
      Set.disjoint_image_of_injective Subtype.val_injective <|
        SimpleGraph.pairwise_disjoint_supp_connectedComponent _ hij
  have disjointM12 : Disjoint M1.support M2.support := by
    rw [hM1.2.support_eq_verts, hM2.support_eq_verts, Subgraph.verts_iSup,
      Set.disjoint_iUnion_right]
    exact fun K ↦ hcomplMatch_compl K ▸ Set.disjoint_sdiff_right
  -- The only vertices left are indeed contained in universalVerts
  have : (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts := by
    rw [Set.compl_subset_comm, Set.compl_eq_univ_diff]
    intro v hv
    by_cases h : v ∈ M1.verts
    · exact M1.verts.mem_union_left _ h
    right
    simp only [deleteUniversalVerts_verts, Subgraph.verts_iSup, Set.mem_iUnion, M2,
      hcomplMatch_compl]
    use G.deleteUniversalVerts.coe.connectedComponentMk ⟨v, hv⟩
    aesop
  exact ⟨M1 ⊔ M2, hM1.2.sup hM2 disjointM12, this⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have intro : ∀ (val : Fintype V), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: cases nonempty_fintype V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have intro : ∀ (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have intro : ∀ (M' : G.Subgraph) (hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
    (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have intro : Disjoint M.support M'.support
Tactic: refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
intro : Disjoint M.support M'.support
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have intro₁ : (M ⊔ M').IsSpanning
Tactic: refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
M' : G.Subgraph
hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching
⊢ (M ⊔ M').IsSpanning
have intro : M.verts ∪ M.vertsᶜ = Set.univ
Tactic: rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have intro : ∀ (val : Fintype V), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: classical
  cases nonempty_fintype V
  obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
  obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
    (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card)
  refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
  · simp [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, disjoint_compl_right]
  · rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
    exact M.verts.union_compl_self
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
intro : ∀ (val : Fintype V), ∃ (M : G.Subgraph), M.IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have intro₁ : ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts),
  ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: classical
  cases nonempty_fintype V
  obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
  obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
    (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card)
  refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
  · simp [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, disjoint_compl_right]
  · rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
    exact M.verts.union_compl_self
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
intro : ∀ (val : Fintype V), ∃ (M : G.Subgraph), M.IsPerfectMatching
intro₁ :
  ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts),
    ∃ (M : G.Subgraph), M.IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have intro₂ : ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts) (M' : G.Subgraph)
  (hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: classical
  cases nonempty_fintype V
  obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
  obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
    (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card)
  refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
  · simp [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, disjoint_compl_right]
  · rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
    exact M.verts.union_compl_self
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
intro : ∀ (val : Fintype V), ∃ (M : G.Subgraph), M.IsPerfectMatching
intro₁ :
  ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts),
    ∃ (M : G.Subgraph), M.IsPerfectMatching
intro₂ :
  ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts) (M' : G.Subgraph)
    (hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching), ∃ (M : G.Subgraph), M.IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have intro₃ : ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts) (M' : G.Subgraph)
  (hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching), Disjoint M.support M'.support
Tactic: classical
  cases nonempty_fintype V
  obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
  obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
    (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card)
  refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
  · simp [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, disjoint_compl_right]
  · rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
    exact M.verts.union_compl_self
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
intro : ∀ (val : Fintype V), ∃ (M : G.Subgraph), M.IsPerfectMatching
intro₁ :
  ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts),
    ∃ (M : G.Subgraph), M.IsPerfectMatching
intro₂ :
  ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts) (M' : G.Subgraph)
    (hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching), ∃ (M : G.Subgraph), M.IsPerfectMatching
intro₃ :
  ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts) (M' : G.Subgraph)
    (hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching), Disjoint M.support M'.support
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have intro₄ : ∀ (val : Fintype V) (M : G.Subgraph) (hM : M.IsMatching) (hsub : M.vertsᶜ ⊆ G.universalVerts) (M' : G.Subgraph)
  (hM' : M'.verts = M.vertsᶜ ∧ M'.IsMatching), (M ⊔ M').IsSpanning
Tactic: classical
  cases nonempty_fintype V
  obtain ⟨M, hM, hsub⟩ := IsMatching.exists_verts_compl_subset_universalVerts h h'
  obtain ⟨M', hM'⟩ := ((G.isClique_universalVerts.subset hsub).even_iff_exists_isMatching
    (Set.toFinite _)).mp (by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card)
  refine ⟨M ⊔ M', hM.sup hM'.2 ?_, ?_⟩
  · simp [hM.support_eq_verts, hM'.2.support_eq_verts, hM'.1, disjoint_compl_right]
  · rw [Subgraph.isSpanning_iff, Subgraph.verts_sup, hM'.1]
    exact M.verts.union_compl_self
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
hodd : Odd (Nat.card V)
⊢ G.IsTutteViolator ∅
have rw : 0 <
  Set.ncard.{u_1} (α :=
    ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ ∅)) : Type u_1))
      (Subgraph.coe (Subgraph.deleteVerts ⊤ ∅)))
    (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ ∅)))
Tactic: rw [IsTutteViolator, Set.ncard_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
⊢ ¬G.IsTutteViolator u
have choose : ∀ (f : (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) → V)
  (hf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), f c ∈ u)
  (g :
    (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) →
      (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
  (hgf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), M.Adj (↑(g c) : V) (f c))
  (hg :
    ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)),
      g c ∈ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp),
  ¬G.IsTutteViolator u
Tactic: choose f hf g hgf hg using ConnectedComponent.odd_matches_node_outside hM (u := u)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) → V
hf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), f c ∈ u
g :
  (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) →
    (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)
hgf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), M.Adj (↑(g c) : V) (f c)
hg :
  ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)),
    g c ∈ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
c d : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
hcd : f c = f d
⊢ c = d
have hcd₁ : g c = g d
Tactic: replace hcd : g c = g d := Subtype.val_injective <| hM.1.eq_of_adj_right (hgf c) (hcd ▸ hgf d)
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
M : G.Subgraph
hM : M.IsPerfectMatching
u : Set V
f : (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) → V
hf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), f c ∈ u
g :
  (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)) →
    (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)
hgf : ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)), M.Adj (↑(g c) : V) (f c)
hg :
  ∀ (c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)),
    g c ∈ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
⊢ ¬G.IsTutteViolator u
have hfinj : Function.Injective f
Tactic: have hfinj : f.Injective := fun c d hcd ↦ by
    replace hcd : g c = g d := Subtype.val_injective <| hM.1.eq_of_adj_right (hgf c) (hcd ▸ hgf d)
    exact Subtype.val_injective <| ConnectedComponent.eq_of_common_vertex (hg c) (hcd ▸ hg d)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have pos : ∀ (hM1xb : ¬M1.Adj x b), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: by_cases hM1xb : ¬M1.Adj x b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
pos : ∀ (hM1xb : ¬M1.Adj x b), ∃ (M : G.Subgraph), M.IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have neg : ∀ (hM1xb : ¬¬M1.Adj x b), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: by_cases hM1xb : ¬M1.Adj x b
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : ¬M1.Adj x b
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have h : (toSubgraph M1.spanningCoe sorry).IsPerfectMatching
Tactic: use G.toSubgraph M1.spanningCoe (M1.spanningCoe_sup_edge_le _ hM1xb)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : ¬¬M1.Adj x b
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have pos : ∀ (hM2ac : ¬M2.Adj a c), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: by_cases hM2ac : ¬M2.Adj a c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : ¬¬M1.Adj x b
pos : ∀ (hM2ac : ¬M2.Adj a c), ∃ (M : G.Subgraph), M.IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have neg : ∀ (hM2ac : ¬¬M2.Adj a c), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: by_cases hM2ac : ¬M2.Adj a c
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : ¬¬M1.Adj x b
hM2ac : ¬M2.Adj a c
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have h : (toSubgraph M2.spanningCoe sorry).IsPerfectMatching
Tactic: use G.toSubgraph M2.spanningCoe (M2.spanningCoe_sup_edge_le _ hM2ac)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Tutte (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : ¬¬M1.Adj x b
hM2ac : ¬¬M2.Adj a c
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have hM1xb₁ : M1.Adj x b
Tactic: simp only [not_not] at hM1xb hM2ac
Cleared hypotheses: hM1xb, hM2ac