no goals
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
v w : V
h : IsMatching M
hv : v ∈ M.verts
hw : w ∈ M.verts
ha : Adj M v w
⊢ toEdge h { val := v, property := hv } = toEdge h { val := w, property := hw }
rw [h.toEdge_eq_of_adj hv ha, h.toEdge_eq_of_adj hw (M.symm ha), Subtype.mk_eq_mk, Sym2.eq_swap]