case mk
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
e : Sym2 V
he : e ∈ edgeSet M
⊢ ∃ a, toEdge h a = { val := e, property := he }
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
⊢ Function.Surjective (toEdge h)
rintro ⟨e, he⟩
case mk
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
e : Sym2 V
he✝ : e ∈ edgeSet M
x y : V
he : Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet M
⊢ ∃ a, toEdge h a = { val := Quotient.mk (Sym2.Rel.setoid V) (x, y), property := he }
case mk
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
e : Sym2 V
he : e ∈ edgeSet M
⊢ ∃ a, toEdge h a = { val := e, property := he }
refine Sym2.ind (fun x y he => ?_) e he
no goals
case mk
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
e : Sym2 V
he✝ : e ∈ edgeSet M
x y : V
he : Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ edgeSet M
⊢ ∃ a, toEdge h a = { val := Quotient.mk (Sym2.Rel.setoid V) (x, y), property := he }
exact ⟨⟨x, M.edge_vert he⟩, h.toEdge_eq_of_adj _ he⟩