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

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

Result:
case intro.intro.mk.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
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
⊢ ∃! w, (M.induce (Subtype.val '' c.supp)).Adj (↑⟨v', hv'⟩) w

Proof state:
case intro.intro.mk.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
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
⊢ ∃! w, (M.induce (Subtype.val '' c.supp)).Adj (↑⟨v', hv'⟩) w

Tactic:
use w

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
⊢ (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

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
⊢ (M.induce (Subtype.val '' c.supp)).IsMatching

Tactic:
intro v hv

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
v : V
hv : v ∈ (M.induce (Subtype.val '' c.supp)).verts
⊢ ∃! w, (M.induce (Subtype.val '' c.supp)).Adj v w

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
⊢ ∃ w ∈ u, ∃ v, M.Adj (↑v) w ∧ v ∈ c.supp

Tactic:
by_contra! h

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
⊢ False

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
hv' : v' ∉ u
⊢ v' ∉ u

Tactic:
trivial

Result:
no goals

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
this : Fintype ↑(M.induce (Subtype.val '' c.supp)).verts
⊢ Even c.supp.ncard

Tactic:
classical
haveI : Fintype (c.supp) := Fintype.ofFinite _
simpa [Subgraph.induce_verts, Subgraph.verts_top, Set.toFinset_image, Nat.card_eq_fintype_card,
  Set.toFinset_image,Finset.card_image_of_injective _ (Subtype.val_injective), Set.toFinset_card,
  ← Set.Nat.card_coe_set_eq] using hMmatch.even_card

Result:
no goals

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
⊢ False

Tactic:
apply Nat.not_even_iff_odd.2 codd

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
⊢ 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
hMmatch : (M.induce (Subtype.val '' c.supp)).IsMatching
this : Fintype ↑(M.induce (Subtype.val '' c.supp)).verts
⊢ Even c.supp.ncard

Tactic:
haveI : Fintype (c.supp) := 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
this : Fintype ↑c.supp
⊢ 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
hMmatch : (M.induce (Subtype.val '' c.supp)).IsMatching
this✝ : Fintype ↑(M.induce (Subtype.val '' c.supp)).verts
this : Fintype ↑c.supp
⊢ Even c.supp.ncard

Tactic:
simpa [Subgraph.induce_verts, Subgraph.verts_top, Set.toFinset_image, Nat.card_eq_fintype_card,
  Set.toFinset_image,Finset.card_image_of_injective _ (Subtype.val_injective), Set.toFinset_card,
  ← Set.Nat.card_coe_set_eq] using hMmatch.even_card

Result:
no goals