V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v : V
hv : v ∈ M.verts
⊢ v ∈ support M
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
⊢ support M = M.verts
refine M.support_subset_verts.antisymm fun v hv => ?_
case intro.intro
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v : V
hv : v ∈ M.verts
w : V
hvw : Adj M v w
⊢ v ∈ support M
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v : V
hv : v ∈ M.verts
⊢ v ∈ support M
obtain ⟨w, hvw, -⟩ := h hv
no goals
case intro.intro
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v : V
hv : v ∈ M.verts
w : V
hvw : Adj M v w
⊢ v ∈ support M
exact ⟨_, hvw⟩