V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v w : V
hv : v ∈ M.verts
hvw : Adj M v w
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, Exists.choose (_ : ∃! w, Adj M (↑{ val := v, property := hv }) w)) =
    Quotient.mk (Sym2.Rel.setoid V) (v, w)
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v w : V
hv : v ∈ M.verts
hvw : Adj M v w
⊢ toEdge h { val := v, property := hv } = { val := Quotient.mk (Sym2.Rel.setoid V) (v, w), property := hvw }
simp only [IsMatching.toEdge, Subtype.mk_eq_mk]
case e_a.e_snd
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v w : V
hv : v ∈ M.verts
hvw : Adj M v w
⊢ Exists.choose (_ : ∃! w, Adj M (↑{ val := v, property := hv }) w) = w
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v w : V
hv : v ∈ M.verts
hvw : Adj M v w
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, Exists.choose (_ : ∃! w, Adj M (↑{ val := v, property := hv }) w)) =
    Quotient.mk (Sym2.Rel.setoid V) (v, w)
congr
no goals
case e_a.e_snd
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v w : V
hv : v ∈ M.verts
hvw : Adj M v w
⊢ Exists.choose (_ : ∃! w, Adj M (↑{ val := v, property := hv }) w) = w
exact ((h (M.edge_vert hvw)).choose_spec.2 w hvw).symm