case refine'_1
V : Type u
G : SimpleGraph V
M : Subgraph G
⊢ IsPerfectMatching M → ∀ (v : V), ∃! w, Adj M v w

case refine'_2
V : Type u
G : SimpleGraph V
M : Subgraph G
hm : ∀ (v : V), ∃! w, Adj M v w
v : V
⊢ v ∈ M.verts
V : Type u
G : SimpleGraph V
M : Subgraph G
⊢ IsPerfectMatching M ↔ ∀ (v : V), ∃! w, Adj M v w
refine' ⟨_, fun hm => ⟨fun v _ => hm v, fun v => _⟩⟩
case refine'_1.intro
V : Type u
G : SimpleGraph V
M : Subgraph G
hm : IsMatching M
hs : IsSpanning M
v : V
⊢ ∃! w, Adj M v w
case refine'_1
V : Type u
G : SimpleGraph V
M : Subgraph G
⊢ IsPerfectMatching M → ∀ (v : V), ∃! w, Adj M v w
rintro ⟨hm, hs⟩ v
no goals
case refine'_1.intro
V : Type u
G : SimpleGraph V
M : Subgraph G
hm : IsMatching M
hs : IsSpanning M
v : V
⊢ ∃! w, Adj M v w
exact hm (hs v)
case refine'_2.intro.intro
V : Type u
G : SimpleGraph V
M : Subgraph G
hm : ∀ (v : V), ∃! w, Adj M v w
v w : V
hw : Adj M v w
⊢ v ∈ M.verts
case refine'_2
V : Type u
G : SimpleGraph V
M : Subgraph G
hm : ∀ (v : V), ∃! w, Adj M v w
v : V
⊢ v ∈ M.verts
obtain ⟨w, hw, -⟩ := hm v
no goals
case refine'_2.intro.intro
V : Type u
G : SimpleGraph V
M : Subgraph G
hm : ∀ (v : V), ∃! w, Adj M v w
v w : V
hw : Adj M v w
⊢ v ∈ M.verts
exact M.edge_vert hw