awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
⊢ M2.IsMatching

Tactic:
.iSup hcomplMatch_match fun i j hij ↦ (?_ : Disjoint _ _)

Premises used: SimpleGraph.Subgraph.IsMatching.iSup
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
refine :
  ∀ (i j : G.deleteUniversalVerts.coe.ConnectedComponent) (hij : i ≠ j),
    Disjoint (complMatch i).support (complMatch j).support
⊢ M2.IsMatching

Tactic:
refine .iSup hcomplMatch_match fun i j hij ↦ (?_ : Disjoint _ _)
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
i j : G.deleteUniversalVerts.coe.ConnectedComponent
hij : i ≠ j
rw :
  Disjoint (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' i.supp \ M1.verts)
    (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' j.supp \ M1.verts)
⊢ Disjoint (complMatch i).support (complMatch j).support

Tactic:
rw [(hcomplMatch_match i).support_eq_verts, hcomplMatch_compl i,
        (hcomplMatch_match j).support_eq_verts, hcomplMatch_compl j]

Premises used: SimpleGraph.Subgraph.IsMatching.support_eq_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
i j : G.deleteUniversalVerts.coe.ConnectedComponent
hij : i ≠ j
⊢ Disjoint (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' i.supp \ M1.verts)
    (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' j.supp \ M1.verts)

Tactic:
Set.disjoint_of_subset Set.diff_subset Set.diff_subset <|
      Set.disjoint_image_of_injective Subtype.val_injective <|
        SimpleGraph.pairwise_disjoint_supp_connectedComponent _ hij

Premises used: Set.diff_subset, Subtype.val_injective, Set.disjoint_of_subset, SimpleGraph.pairwise_disjoint_supp_connectedComponent, Set.disjoint_image_of_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
i j : G.deleteUniversalVerts.coe.ConnectedComponent
hij : i ≠ j
⊢ Disjoint (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' i.supp \ M1.verts)
    (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' j.supp \ M1.verts)

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

Premises used: Set.diff_subset, Subtype.val_injective, Set.disjoint_of_subset, SimpleGraph.pairwise_disjoint_supp_connectedComponent, Set.disjoint_image_of_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
⊢ M2.IsMatching

Tactic:
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
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
rw : ∀ (i : G.deleteUniversalVerts.coe.ConnectedComponent), Disjoint M1.verts (complMatch i).verts
⊢ Disjoint M1.support M2.support

Tactic:
rw [hM1.2.support_eq_verts, hM2.support_eq_verts, Subgraph.verts_iSup,
      Set.disjoint_iUnion_right]

Premises used: Set.disjoint_iUnion_right, And.right, SimpleGraph.Subgraph.verts_iSup, SimpleGraph.Subgraph.IsMatching.support_eq_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
⊢ ∀ (i : G.deleteUniversalVerts.coe.ConnectedComponent), Disjoint M1.verts (complMatch i).verts

Tactic:
fun K ↦ hcomplMatch_compl K ▸ Set.disjoint_sdiff_right

Premises used: Eq.rec, Set.disjoint_sdiff_right, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
⊢ ∀ (i : G.deleteUniversalVerts.coe.ConnectedComponent), Disjoint M1.verts (complMatch i).verts

Tactic:
exact fun K ↦ hcomplMatch_compl K ▸ Set.disjoint_sdiff_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
⊢ Disjoint M1.support M2.support

Tactic:
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
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
rw : Set.univ \ G.universalVerts ⊆ M1.verts ∪ M2.verts
⊢ (M1.verts ∪ M2.verts)ᶜ ⊆ G.universalVerts

Tactic:
rw [Set.compl_subset_comm, Set.compl_eq_univ_diff]

Premises used: Set.compl_subset_comm, Set.compl_eq_univ_diff
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
v : V
hv : v ∈ Set.univ \ G.universalVerts
pos : ∀ (h : v ∈ M1.verts), v ∈ M1.verts ∪ M2.verts
neg : ∀ (h : v ∉ M1.verts), v ∈ M1.verts ∪ M2.verts
⊢ v ∈ M1.verts ∪ M2.verts

Tactic:
by_cases h : v ∈ M1.verts

Premises used: SimpleGraph.Subgraph.verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
⊢ v ∈ M1.verts ∪ M2.verts

Tactic:
M1.verts.mem_union_left _ h

Premises used: Set.mem_union_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
⊢ v ∈ M1.verts ∪ M2.verts

Tactic:
exact M1.verts.mem_union_left _ h

Premises used: Set.mem_union_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
neg : v ∈ M2.verts
⊢ v ∈ M1.verts ∪ M2.verts

Tactic:
right
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
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
neg :
  ∃ (i : G.deleteUniversalVerts.coe.ConnectedComponent),
    v ∈ (fun (a : { x : V // x ∈ Set.univ \ G.universalVerts }) ↦ (↑a : V)) '' i.supp \ M1.verts
⊢ v ∈ M2.verts

Tactic:
simp only [deleteUniversalVerts_verts, Subgraph.verts_iSup, Set.mem_iUnion, M2,
      hcomplMatch_compl]

Premises used: SimpleGraph.deleteUniversalVerts_verts, Set.mem_iUnion, SimpleGraph.Subgraph.verts_iSup