[GOAL]
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 }
[PROOFSTEP]
simp only [IsMatching.toEdge, Subtype.mk_eq_mk]
[GOAL]
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)
[PROOFSTEP]
congr
[GOAL]
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
[PROOFSTEP]
exact ((h (M.edge_vert hvw)).choose_spec.2 w hvw).symm
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
⊢ Function.Surjective (toEdge h)
[PROOFSTEP]
rintro ⟨e, he⟩
[GOAL]
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 }
[PROOFSTEP]
refine Sym2.ind (fun x y he => ?_) e he
[GOAL]
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 }
[PROOFSTEP]
exact ⟨⟨x, M.edge_vert he⟩, h.toEdge_eq_of_adj _ he⟩
[GOAL]
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 }
[PROOFSTEP]
rw [h.toEdge_eq_of_adj hv ha, h.toEdge_eq_of_adj hw (M.symm ha), Subtype.mk_eq_mk, Sym2.eq_swap]
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
⊢ support M = M.verts
[PROOFSTEP]
refine M.support_subset_verts.antisymm fun v hv => ?_
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
h : IsMatching M
v : V
hv : v ∈ M.verts
⊢ v ∈ support M
[PROOFSTEP]
obtain ⟨w, hvw, -⟩ := h hv
[GOAL]
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
[PROOFSTEP]
exact ⟨_, hvw⟩
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : (v : V) → Fintype ↑(neighborSet M v)
⊢ IsMatching M ↔ ∀ (v : V), v ∈ M.verts → degree M v = 1
[PROOFSTEP]
simp only [degree_eq_one_iff_unique_adj, IsMatching]
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h : IsMatching M
⊢ Even (Finset.card (Set.toFinset M.verts))
[PROOFSTEP]
classical
rw [isMatching_iff_forall_degree] at h 
use M.coe.edgeFinset.card
rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]
  -- Porting note: `SimpleGraph.Subgraph.coe_degree` does not trigger because it uses
    -- instance arguments instead of implicit arguments for the first `Fintype` argument.
    -- Using a `convert_to` to swap out the `Fintype` instance to the "right" one.
convert_to _ = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v using 3
simp [h, Finset.card_univ]
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h : IsMatching M
⊢ Even (Finset.card (Set.toFinset M.verts))
[PROOFSTEP]
rw [isMatching_iff_forall_degree] at h 
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h✝ : IsMatching M
h : ∀ (v : V), v ∈ M.verts → degree M v = 1
⊢ Even (Finset.card (Set.toFinset M.verts))
[PROOFSTEP]
use M.coe.edgeFinset.card
[GOAL]
case h
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h✝ : IsMatching M
h : ∀ (v : V), v ∈ M.verts → degree M v = 1
⊢ Finset.card (Set.toFinset M.verts) =
    Finset.card (edgeFinset (Subgraph.coe M)) + Finset.card (edgeFinset (Subgraph.coe M))
[PROOFSTEP]
rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]
  -- Porting note: `SimpleGraph.Subgraph.coe_degree` does not trigger because it uses
    -- instance arguments instead of implicit arguments for the first `Fintype` argument.
    -- Using a `convert_to` to swap out the `Fintype` instance to the "right" one.
[GOAL]
case h
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h✝ : IsMatching M
h : ∀ (v : V), v ∈ M.verts → degree M v = 1
⊢ Finset.card (Set.toFinset M.verts) = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v
[PROOFSTEP]
convert_to _ = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v using 3
[GOAL]
case h.convert_2
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h✝ : IsMatching M
h : ∀ (v : V), v ∈ M.verts → degree M v = 1
⊢ Finset.card (Set.toFinset M.verts) = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v
[PROOFSTEP]
simp [h, Finset.card_univ]
[GOAL]
V : Type u
G : SimpleGraph V
M : Subgraph G
⊢ IsPerfectMatching M ↔ ∀ (v : V), ∃! w, Adj M v w
[PROOFSTEP]
refine' ⟨_, fun hm => ⟨fun v _ => hm v, fun v => _⟩⟩
[GOAL]
case refine'_1
V : Type u
G : SimpleGraph V
M : Subgraph G
⊢ IsPerfectMatching M → ∀ (v : V), ∃! w, Adj M v w
[PROOFSTEP]
rintro ⟨hm, hs⟩ v
[GOAL]
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
[PROOFSTEP]
exact hm (hs v)
[GOAL]
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
[PROOFSTEP]
obtain ⟨w, hw, -⟩ := hm v
[GOAL]
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
[PROOFSTEP]
exact M.edge_vert hw
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : (v : V) → Fintype ↑(neighborSet M v)
⊢ IsPerfectMatching M ↔ ∀ (v : V), degree M v = 1
[PROOFSTEP]
simp [degree_eq_one_iff_unique_adj, isPerfectMatching_iff]
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype V
h : IsPerfectMatching M
⊢ Even (Fintype.card V)
[PROOFSTEP]
classical simpa only [h.2.card_verts] using IsMatching.even_card h.1
[GOAL]
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype V
h : IsPerfectMatching M
⊢ Even (Fintype.card V)
[PROOFSTEP]
simpa only [h.2.card_verts] using IsMatching.even_card h.1
