-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma odd_matches_node_outside [Finite V] {u : Set V}
    {c : ConnectedComponent (Subgraph.deleteVerts ⊤ u).coe}
    (hM : M.IsPerfectMatching) (codd : Odd c.supp.ncard) :
    ∃ᵉ (w ∈ u) (v : ((⊤ : G.Subgraph).deleteVerts u).verts), M.Adj v w ∧ v ∈ c.supp

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
⊢ False

Tactic:
have hMmatch : (M.induce c.supp).IsMatching := by
  intro v hv
  obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
  obtain ⟨⟨v', hv'⟩, ⟨hv , rfl⟩⟩ := hv
  use w
  have hwnu : w ∉ u := fun hw' ↦ h w hw' ⟨v', hv'⟩ (hw.1) hv
  refine ⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩
  apply ConnectedComponent.mem_coe_supp_of_adj ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ ⟨by trivial, hwnu⟩
  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' ⊢
  trivial

Result:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
hMmatch : (M.induce (Subtype.val '' c.supp)).IsMatching
⊢ False

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
hMmatch : (M.induce (Subtype.val '' c.supp)).IsMatching
⊢ Even c.supp.ncard

Tactic:
haveI : Fintype ↑(Subgraph.induce M (Subtype.val '' supp c)).verts := Fintype.ofFinite _

Result:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
hMmatch : (M.induce (Subtype.val '' c.supp)).IsMatching
this : Fintype ↑(M.induce (Subtype.val '' c.supp)).verts
⊢ Even c.supp.ncard

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
v : V
hv : v ∈ (M.induce (Subtype.val '' c.supp)).verts
⊢ ∃! w, (M.induce (Subtype.val '' c.supp)).Adj v w

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

Result:
case intro
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
v : V
hv : v ∈ (M.induce (Subtype.val '' c.supp)).verts
w : V
hw : (fun w => M.Adj v w) w ∧ ∀ (y : V), (fun w => M.Adj v w) y → y = w
⊢ ∃! w, (M.induce (Subtype.val '' c.supp)).Adj v w

Proof state:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
w v' : V
hv' : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'⟩ ∈ c.supp
hw : (fun w => M.Adj (↑⟨v', hv'⟩) w) w ∧ ∀ (y : V), (fun w => M.Adj (↑⟨v', hv'⟩) w) y → y = w
hwnu : w ∉ u
⊢ (fun w => (M.induce (Subtype.val '' c.supp)).Adj (↑⟨v', hv'⟩) w) w ∧
    ∀ (y : V), (fun w => (M.induce (Subtype.val '' c.supp)).Adj (↑⟨v', hv'⟩) w) y → y = w

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

Result:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
w v' : V
hv' : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'⟩ ∈ c.supp
hw : (fun w => M.Adj (↑⟨v', hv'⟩) w) w ∧ ∀ (y : V), (fun w => M.Adj (↑⟨v', hv'⟩) w) y → y = w
hwnu : w ∉ u
⊢ w ∈ Subtype.val '' c.supp

Proof state:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
w v' : V
hv' : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'⟩ ∈ c.supp
hw : (fun w => M.Adj (↑⟨v', hv'⟩) w) w ∧ ∀ (y : V), (fun w => M.Adj (↑⟨v', hv'⟩) w) y → y = w
hwnu : w ∉ u
⊢ (⊤.deleteVerts u).Adj (↑⟨v', hv'⟩) 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' ⊢

Result:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
w v' : V
hv'✝ : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'✝⟩ ∈ c.supp
hw : (fun w => M.Adj (↑⟨v', hv'✝⟩) w) w ∧ ∀ (y : V), (fun w => M.Adj (↑⟨v', hv'✝⟩) w) y → y = w
hwnu : w ∉ u
hv' : v' ∉ u
⊢ v' ∉ u

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
w v' : V
hv' : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'⟩ ∈ c.supp
hw : (fun w => M.Adj (↑⟨v', hv'⟩) w) w ∧ ∀ (y : V), (fun w => M.Adj (↑⟨v', hv'⟩) w) y → y = w
hwnu : w ∉ u
⊢ w ∈ ⊤.verts

Tactic:
trivial

Result:
no goals

Proof state:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
w v' : V
hv' : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'⟩ ∈ c.supp
hw : (fun w => M.Adj (↑⟨v', hv'⟩) w) w ∧ ∀ (y : V), (fun w => M.Adj (↑⟨v', hv'⟩) w) y → y = w
hwnu : w ∉ u
⊢ w ∈ Subtype.val '' c.supp

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

Result:
case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
c : (⊤.deleteVerts u).coe.ConnectedComponent
hM : M.IsPerfectMatching
codd : Odd c.supp.ncard
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ c.supp
w v' : V
hv' : v' ∈ (⊤.deleteVerts u).verts
hv : ⟨v', hv'⟩ ∈ c.supp
hw : (fun w => M.Adj (↑⟨v', hv'⟩) w) w ∧ ∀ (y : V), (fun w => M.Adj (↑⟨v', hv'⟩) w) y → y = w
hwnu : w ∉ u
⊢ (⊤.deleteVerts u).Adj (↑⟨v', hv'⟩) w