awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ ¬M.spanningCoe.Adj x a

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ (p.toSubgraph.spanningCoe ⊔ edge x a).Adj a c

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
refine_1 : ∀ (u' : V) (hu'x : u' ≠ x) (hadj : p.toSubgraph.spanningCoe.Adj a u'), M.spanningCoe.Adj a u'
refine_2 : (p.toSubgraph.spanningCoe ⊔ edge x a).IsCycles
refine_3 : ¬(p.toSubgraph.spanningCoe ⊔ edge x a).Adj x b
refine_4 : ∀ (v w : V) (hvw : (edge x a).Adj v w), (G ⊔ edge a c).Adj v w
⊢ ∃ (G' : SimpleGraph V), G'.IsAlternating M.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
refine ⟨p.toSubgraph.spanningCoe ⊔ edge x a, (hcalt.spanningCoe p.toSubgraph).sup_edge (by simpa)
    (fun u' hu'x hadj ↦ ?_) aux, ?_, ?_, by aesop, sup_le_iff.mpr ⟨hle, fun v w hvw ↦ ?_⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
u' : V
hu'x : u' ≠ x
hadj : p.toSubgraph.spanningCoe.Adj a u'
⊢ M.spanningCoe.Adj a u'

Tactic:
simpa [← hp.snd_of_toSubgraph_adj hadj, hp.snd_of_toSubgraph_adj hpac]

Premises used: SimpleGraph.Walk.IsPath.snd_of_toSubgraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ (p.toSubgraph.spanningCoe ⊔ edge x a).IsCycles

Tactic:
hp.isCycles_spanningCoe_toSubgraph_sup_edge hgadj.ne.symm fun hadj ↦ ?_

Premises used: SimpleGraph.Adj.ne, Ne.symm, SimpleGraph.Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
refine_2 : ∀ (hadj : s(x, a) ∈ p.edges), False
⊢ (p.toSubgraph.spanningCoe ⊔ edge x a).IsCycles

Tactic:
refine hp.isCycles_spanningCoe_toSubgraph_sup_edge hgadj.ne.symm fun hadj ↦ ?_

Premises used: SimpleGraph.Adj.ne, Ne.symm, SimpleGraph.Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
hadj : s(x, a) ∈ p.edges
⊢ p.toSubgraph.Adj x a

Tactic:
rw [← Walk.mem_edges_toSubgraph, Subgraph.mem_edgeSet] at hadj

Premises used: SimpleGraph.Subgraph.mem_edgeSet, SimpleGraph.Walk.mem_edges_toSubgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
hadj : p.toSubgraph.Adj x a
⊢ False

Tactic:
simp [← hp.snd_of_toSubgraph_adj hadj.symm, hp.snd_of_toSubgraph_adj hpac] at hnxc

Premises used: SimpleGraph.Subgraph.Adj.symm, SimpleGraph.Walk.IsPath.snd_of_toSubgraph_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
⊢ ¬(p.toSubgraph.spanningCoe ⊔ edge x a).Adj x b

Tactic:
simp +contextual [hnpxb, edge_adj, hnab.symm]

Premises used: Ne.symm, SimpleGraph.edge_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
x b a c : V
M : (G ⊔ edge a c).Subgraph
p : G'.Walk a x
hp : p.IsPath
hcalt : G'.IsAlternating M.spanningCoe
hM2nadj : ¬M.Adj x a
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
hM2ac : M.Adj a c
hgadj : G.Adj x a
hnxc : x ≠ c
hnab : a ≠ b
hle : p.toSubgraph.spanningCoe ≤ G ⊔ edge a c
aux : ∀ (c' : V), c' ≠ a → p.toSubgraph.Adj c' x → M.Adj c' x
v w : V
hvw : (edge x a).Adj v w
⊢ (G ⊔ edge a c).Adj v w

Tactic:
simpa [edge_adj, adj_congr_of_sym2 _ ((adj_edge _ _).mp hvw).1.symm] using .inl hgadj

Premises used: SimpleGraph.adj_edge, SimpleGraph.edge_adj, And.left, SimpleGraph.adj_congr_of_sym2, Iff.mp, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
inst : Finite V
u : Set V
h : G ≤ G'
ht :
  u.ncard <
    Set.ncard (α :=
      ConnectedComponent (V := (↑(Set.univ \ u) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u) :
          SimpleGraph (↑(Subgraph.verts (G := G') (Subgraph.deleteVerts ⊤ u)) : Type u_1)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
⊢ Set.ncard (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) ≤
    Set.ncard (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
      (oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))

Tactic:
have := ncard_oddComponents_mono _ (Subgraph.deleteVerts_mono' (G := G) (G' := G') u h)
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
inst : Finite V
u : Set V
h : G ≤ G'
ht :
  u.ncard <
    Set.ncard.{u_1} (α :=
      ConnectedComponent (V := (↑(Set.univ \ u) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u) :
          SimpleGraph (↑(Subgraph.verts (G := G') (Subgraph.deleteVerts ⊤ u)) : Type u_1)))
      {c :
        ConnectedComponent (V := (↑(Set.univ \ u) : Type u_1))
          (Subgraph.coe (Subgraph.deleteVerts ⊤ u) :
            SimpleGraph (↑(Subgraph.verts (G := G') (Subgraph.deleteVerts ⊤ u)) : Type u_1)) |
        Odd c.supp.ncard}
this :
  Set.ncard.{u_1} (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
      {c :
        ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
          (Subgraph.coe (Subgraph.deleteVerts ⊤ u)) |
        Odd c.supp.ncard} ≤
    Set.ncard.{u_1} (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
      {c :
        ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
          (Subgraph.coe (Subgraph.deleteVerts ⊤ u)) |
        Odd c.supp.ncard}
⊢ u.ncard <
    Set.ncard.{u_1} (α :=
      ConnectedComponent (V := (↑(Set.univ \ u) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u) :
          SimpleGraph (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)))
      {c :
        ConnectedComponent (V := (↑(Set.univ \ u) : Type u_1))
          (Subgraph.coe (Subgraph.deleteVerts ⊤ u) :
            SimpleGraph (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) |
        Odd c.supp.ncard}

Tactic:
lt_of_lt_of_le ht this

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G G' : SimpleGraph V
inst : Finite V
u : Set V
h : G ≤ G'
ht :
  u.ncard <
    Set.ncard.{u_1} (α :=
      ConnectedComponent (V := (↑(Set.univ \ u) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u) :
          SimpleGraph (↑(Subgraph.verts (G := G') (Subgraph.deleteVerts ⊤ u)) : Type u_1)))
      {c :
        ConnectedComponent (V := (↑(Set.univ \ u) : Type u_1))
          (Subgraph.coe (Subgraph.deleteVerts ⊤ u) :
            SimpleGraph (↑(Subgraph.verts (G := G') (Subgraph.deleteVerts ⊤ u)) : Type u_1)) |
        Odd c.supp.ncard}
this :
  Set.ncard.{u_1} (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
      {c :
        ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
          (Subgraph.coe (Subgraph.deleteVerts ⊤ u)) |
        Odd c.supp.ncard} ≤
    Set.ncard.{u_1} (α :=
      ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u)))
      {c :
        ConnectedComponent (V := (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
          (Subgraph.coe (Subgraph.deleteVerts ⊤ u)) |
        Odd c.supp.ncard}
⊢ u.ncard <
    Set.ncard.{u_1} (α :=
      ConnectedComponent (V := (↑(Set.univ \ u) : Type u_1))
        (Subgraph.coe (Subgraph.deleteVerts ⊤ u) :
          SimpleGraph (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)))
      {c :
        ConnectedComponent (V := (↑(Set.univ \ u) : Type u_1))
          (Subgraph.coe (Subgraph.deleteVerts ⊤ u) :
            SimpleGraph (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) |
        Odd c.supp.ncard}

Tactic:
exact lt_of_lt_of_le ht this

Premises used: lt_of_lt_of_le
-- 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
⊢ ConnectedComponent.Represents
    (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents

Tactic:
have hrep := ConnectedComponent.Represents.image_out G.deleteUniversalVerts.coe.oddComponents
-- 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
⊢ Set.ncard (α :=
      ConnectedComponent (V := (↑(verts (G := G) (deleteVerts ⊤ G.universalVerts)) : Type u_1))
        (Subgraph.coe (deleteVerts ⊤ G.universalVerts)))
      (oddComponents (Subgraph.coe (deleteVerts ⊤ G.universalVerts))) ≤
    G.universalVerts.ncard

Tactic:
simp only [IsTutteViolator, not_lt] at h

Premises used: SimpleGraph.IsTutteViolator, not_lt
-- 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
h :
  Set.ncard (α :=
      ConnectedComponent (V := (↑(verts (G := G) (deleteVerts ⊤ G.universalVerts)) : Type u_1))
        (Subgraph.coe (deleteVerts ⊤ G.universalVerts)))
      (oddComponents (Subgraph.coe (deleteVerts ⊤ G.universalVerts))) ≤
    G.universalVerts.ncard
rwa :
  (Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents).ncard ≤
    G.universalVerts.ncard
rwa₁ : Type u_1
rwa₂ : Set { x : V // x ∈ G.deleteUniversalVerts.verts }
rwa₃ rwa₄ rwa₅ rwa₆ : G.deleteUniversalVerts.coe.oddComponents.ncard ≤ G.universalVerts.ncard
⊢ (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
        Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents).ncard ≤
    G.universalVerts.ncard

Tactic:
rwa [Set.ncard_image_of_injective _ Subtype.val_injective, hrep.ncard_eq]

Premises used: Subtype.val_injective, SimpleGraph.ConnectedComponent.Represents.ncard_eq, Set.ncard_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
obtain :
  ∀ (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),
    ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
⊢ ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts

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

Premises used: SimpleGraph.Subgraph.IsMatching.exists_of_universalVerts, Disjoint.symm, SimpleGraph.disjoint_image_val_universalVerts
-- 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
K : G.deleteUniversalVerts.coe.ConnectedComponent
⊢ G.IsClique (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts)

Tactic:
have : G.IsClique (Subtype.val '' K.supp \ M1.verts) :=
      ((h' K).of_induce).subset Set.diff_subset
-- 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
K : G.deleteUniversalVerts.coe.ConnectedComponent
this : G.IsClique (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts)
rw :
  Even
    (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \
        (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
            Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents ∪
          t)).ncard
⊢ ∃ (M : G.Subgraph),
    M.verts = Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts ∧ M.IsMatching

Tactic:
rw [← this.even_iff_exists_isMatching (Set.toFinite _), hM1.1]

Premises used: SimpleGraph.IsClique.even_iff_exists_isMatching, Set.toFinite, And.left
-- 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
K : G.deleteUniversalVerts.coe.ConnectedComponent
this : G.IsClique (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts)
⊢ Even
    (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \
        (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
            Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents ∪
          t)).ncard

Tactic:
even_ncard_image_val_supp_sdiff_image_val_rep_union _ ht hrep

Premises used: SimpleGraph.even_ncard_image_val_supp_sdiff_image_val_rep_union
-- 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
K : G.deleteUniversalVerts.coe.ConnectedComponent
this : G.IsClique (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts)
⊢ Even
    (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \
        (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) ''
            Quot.out (r := G.deleteUniversalVerts.coe.Reachable) '' G.deleteUniversalVerts.coe.oddComponents ∪
          t)).ncard

Tactic:
exact even_ncard_image_val_supp_sdiff_image_val_rep_union _ ht hrep

Premises used: SimpleGraph.even_ncard_image_val_supp_sdiff_image_val_rep_union
-- 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
⊢ ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
    ∃ (M : G.Subgraph),
      M.verts = Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts ∧ M.IsMatching

Tactic:
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
-- 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
exists_complMatch :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent),
    ∃ (M : G.Subgraph),
      M.verts = Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \ M1.verts ∧ M.IsMatching
choose :
  ∀ (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),
    ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts
⊢ ∃ (M : G.Subgraph), M.IsMatching ∧ M.vertsᶜ ⊆ G.universalVerts

Tactic:
choose complMatch hcomplMatch_compl hcomplMatch_match using exists_complMatch