awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
w : V
hvw : M.Adj v w
hw : ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
⊢ (fun (w : V) ↦ (M.induce (M.verts ∩ (G.connectedComponentMk v).supp)).Adj v w) w ∧
    ∀ (y : V), (fun (w : V) ↦ (M.induce (M.verts ∩ (G.connectedComponentMk v).supp)).Adj v w) y → y = w

Tactic:
simpa [hv, hvw, M.edge_vert hvw.symm, (M.adj_sub hvw).symm.reachable] using fun _ _ _ ↦ hw _

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Adj.symm, SimpleGraph.Subgraph.Adj.symm, SimpleGraph.Adj.reachable, SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsPerfectMatching
c : G.ConnectedComponent
⊢ (M.induce c.supp).IsMatching

Tactic:
simpa [h.2.verts_eq_univ] using h.1.induce_connectedComponent c

Premises used: SimpleGraph.Subgraph.IsMatching.induce_connectedComponent, And.right, And.left, SimpleGraph.Subgraph.IsSpanning.verts_eq_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.spanningCoe ≤ G'
⊢ (toSubgraph M.spanningCoe h).IsPerfectMatching ↔ M.IsPerfectMatching

Tactic:
simp only [isPerfectMatching_iff, toSubgraph_adj, spanningCoe_adj]

Premises used: SimpleGraph.Subgraph.isPerfectMatching_iff, SimpleGraph.toSubgraph_adj, SimpleGraph.Subgraph.spanningCoe_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hMr : M.IsMatching
hc : G.IsClique M.verts
hu : M.verts.Finite
⊢ Even M.verts.ncard

Tactic:
simpa [Set.ncard_eq_toFinset_card _ hu, Set.toFinite_toFinset,
      ← Set.toFinset_card] using @hMr.even_card _ _ _ hu.fintype

Premises used: Set.toFinite_toFinset, Set.toFinset_card, Set.ncard_eq_toFinset_card, SimpleGraph.Subgraph.IsMatching.even_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
u : Set V
hc : G.IsClique u
hu : u.Finite
refine : ∀ (h : Even u.ncard), ∃ (M : G.Subgraph), M.verts = u ∧ M.IsMatching
⊢ Even u.ncard ↔ ∃ (M : G.Subgraph), M.verts = u ∧ M.IsMatching

Tactic:
refine ⟨fun h ↦ ?_, by
    rintro ⟨M, rfl, hMr⟩
    simpa [Set.ncard_eq_toFinset_card _ hu, Set.toFinite_toFinset,
      ← Set.toFinset_card] using @hMr.even_card _ _ _ hu.fintype⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
u : Set V
hc : G.IsClique u
hu : u.Finite
h : Even u.ncard
obtain :
  ∀ (t u : Set V) (hc : G.IsClique (t ∪ u)) (hu : (t ∪ u).Finite) (h : Even (t ∪ u).ncard) (hd : Disjoint t u)
    (hcard : t.ncard = u.ncard), ∃ (M : G.Subgraph), M.verts = t ∪ u ∧ M.IsMatching
⊢ ∃ (M : G.Subgraph), M.verts = u ∧ M.IsMatching

Tactic:
obtain ⟨t, u, rfl, hd, hcard⟩ := Set.exists_union_disjoint_ncard_eq_of_even h

Premises used: Set.exists_union_disjoint_ncard_eq_of_even, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
rw : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑t.ncard : Cardinal.{u_1}) (↑u.ncard : Cardinal.{u_1})
⊢ Nonempty.{max 1 (u_1 + 1)} ((↑t : Type u_1) ≃ (↑u : Type u_1))

Tactic:
rw [← Cardinal.eq, ← t.cast_ncard (Set.finite_union.mp hu).1,
      ← u.cast_ncard (Set.finite_union.mp hu).2]

Premises used: Set.finite_union, And.right, And.left, Cardinal.eq, Set.cast_ncard, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑t.ncard : Cardinal.{u_1}) (↑u.ncard : Cardinal.{u_1})

Tactic:
congrArg Nat.cast hcard

Premises used: congrArg, Nat.cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑t.ncard : Cardinal.{u_1}) (↑u.ncard : Cardinal.{u_1})

Tactic:
exact congrArg Nat.cast hcard

Premises used: congrArg, Nat.cast
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
obtain : ∀ (f : (↑t : Type u_1) ≃ (↑u : Type u_1)), ∃ (M : G.Subgraph), M.verts = t ∪ u ∧ M.IsMatching
⊢ ∃ (M : G.Subgraph), M.verts = t ∪ u ∧ M.IsMatching

Tactic:
obtain ⟨f⟩ : Nonempty (t ≃ u) := by
    rw [← Cardinal.eq, ← t.cast_ncard (Set.finite_union.mp hu).1,
      ← u.cast_ncard (Set.finite_union.mp hu).2]
    exact congrArg Nat.cast hcard

Premises used: Set.Elem, Equiv, Nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
f : (↑t : Type u_1) ≃ (↑u : Type u_1)
v : (↑t : Type u_1)
⊢ (↑v : V) ∈ t ∪ u

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
f : (↑t : Type u_1) ≃ (↑u : Type u_1)
v : (↑t : Type u_1)
⊢ (↑((f : (a : (↑t : Type u_1)) → (↑u : Type u_1)) v) : V) ∈ t ∪ u

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
f : (↑t : Type u_1) ≃ (↑u : Type u_1)
v : (↑t : Type u_1)
⊢ (↑v : V) ∈ t

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
f : (↑t : Type u_1) ≃ (↑u : Type u_1)
v : (↑t : Type u_1)
⊢ (↑((f : (a : (↑t : Type u_1)) → (↑u : Type u_1)) v) : V) ∈ u

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
f : (↑t : Type u_1) ≃ (↑u : Type u_1)
⊢ ∃ (M : G.Subgraph), M.verts = t ∪ u ∧ M.IsMatching

Tactic:
exact Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd f
    fun v ↦ hc (by simp) (by simp) <| hd.ne_of_mem (by simp) (by simp)

Premises used: SimpleGraph.Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv, Disjoint.ne_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this : DecidablePred fun (x : V) ↦ x ∈ (M.induce c.supp).verts := fun (a : V) ↦ G.instDecidableMemSupp c a
⊢ Even (M.induce c.supp).verts.toFinset.card

Tactic:
have := (hM.induce_connectedComponent_isMatching c).even_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this_1 : DecidablePred fun (x : V) ↦ x ∈ (M.induce c.supp).verts := fun (a : V) ↦ G.instDecidableMemSupp c a
this : Even (M.induce c.supp).verts.toFinset.card
⊢ Even (Fintype.card.{u_1} (↑c.supp : Type u_1))

Tactic:
simp only [Subgraph.induce_verts, Set.toFinset_card] at this

Premises used: Set.toFinset_card, SimpleGraph.Subgraph.induce_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this_1 : DecidablePred fun (x : V) ↦ x ∈ (M.induce c.supp).verts := fun (a : V) ↦ G.instDecidableMemSupp c a
this : Even (Fintype.card.{u_1} (↑c.supp : Type u_1))
⊢ Even (Fintype.card.{u_1} (↑c.supp : Type u_1))

Tactic:
this

Premises used: Set.Mem, setOf, SimpleGraph.ConnectedComponent.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this_1 : DecidablePred fun (x : V) ↦ x ∈ (M.induce c.supp).verts := fun (a : V) ↦ G.instDecidableMemSupp c a
this : Even (Fintype.card.{u_1} (↑c.supp : Type u_1))
⊢ Even (Fintype.card.{u_1} (↑c.supp : Type u_1))

Tactic:
exact this
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
by_contra! :
  ∀
    (h :
      ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
        (_ : M.Adj (↑v : V) w), v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp),
    False
⊢ ∃ w ∈ u,
    ∃ (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)),
      M.Adj (↑v : V) w ∧ v ∈ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp

Tactic:
by_contra! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
v : V
hv :
  v ∈
    (M.induce
        (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
          (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).verts
obtain :
  ∀ (w : V) (hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w),
    ∃! w : V,
      (M.induce
            (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
              (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
        v w
⊢ ∃! w : V,
    (M.induce
          (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
            (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
      v w

Tactic:
obtain ⟨w, hw⟩ := hM.1 (hM.2 v)

Premises used: And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
v : V
hv :
  v ∈
    (M.induce
        (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
          (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).verts
w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
obtain :
  ∀ (v' : V) (hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u))
    (hv :
      Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
        (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)
    (hw :
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          w ∧
        ∀ (y : V),
          (fun (w : V) ↦
                M.Adj
                  (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
                  w)
              y →
            y = w),
    ∃! w : V,
      (M.induce
            (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
              (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
        (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w
⊢ ∃! w : V,
    (M.induce
          (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
            (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
      v w

Tactic:
obtain ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ := hv

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
h₁ :
  (fun (w : V) ↦
        (M.induce
              (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
          (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            (M.induce
                  (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
              (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
          y →
        y = w
⊢ ∃! w : V,
    (M.induce
          (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
            (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
      (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w

Tactic:
use w
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
⊢ w ∉ u

Tactic:
have hwnu : w ∉ u := fun hw' ↦ h w hw' ⟨v', hv'⟩ (hw.1) hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
hwnu : w ∉ u
⊢ (fun (w : V) ↦
        (M.induce
              (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
          (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            (M.induce
                  (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
              (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
          y →
        y = w

Tactic:
⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩

Premises used: Subtype.mk, And.right, And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
hwnu : w ∉ u
h₁ :
  w ∈
    Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
      (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
⊢ (fun (w : V) ↦
        (M.induce
              (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
          (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            (M.induce
                  (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
              (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
          y →
        y = w

Tactic:
refine ⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
hwnu : w ∉ u
⊢ Membership.mem (γ := Set V) (Subgraph.verts (G := G) ⊤) w

Tactic:
trivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
hwnu : w ∉ u
h₁ :
  Subgraph.Adj (G := G) (Subgraph.deleteVerts ⊤ u)
    (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w
⊢ w ∈
    Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
      (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp

Tactic:
apply ConnectedComponent.mem_coe_supp_of_adj ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ ⟨by trivial, hwnu⟩

Premises used: Subtype.mk, SimpleGraph.ConnectedComponent.mem_coe_supp_of_adj, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
hwnu : w ∉ u
h₁ : ∀ (hv' : v' ∉ u), v' ∉ u
⊢ Subgraph.Adj (G := G) (Subgraph.deleteVerts ⊤ u)
    (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w

Tactic:
simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.mem_diff, Set.mem_univ, true_and,
      Subgraph.induce_adj, hwnu, not_false_eq_true, and_self, Subgraph.top_adj, M.adj_sub hw.1,
      and_true] at hv' ⊢

Premises used: SimpleGraph.Subgraph.induce_adj, and_true, and_self, SimpleGraph.Subgraph.verts_top, SimpleGraph.Subgraph.adj_sub, SimpleGraph.Subgraph.induce_verts, And.left, Set.mem_diff, Set.mem_univ, SimpleGraph.Subgraph.top_adj, not_false_eq_true, true_and