no goals
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h : IsMatching M
⊢ Even (Finset.card (Set.toFinset M.verts))
classical
rw [isMatching_iff_forall_degree] at h
use M.coe.edgeFinset.card
rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]
convert_to _ = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v using 3
simp [h, Finset.card_univ]
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))
V : Type u
G : SimpleGraph V
M✝ M : Subgraph G
inst✝ : Fintype ↑M.verts
h : IsMatching M
⊢ Even (Finset.card (Set.toFinset M.verts))
rw [isMatching_iff_forall_degree] at 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))
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))
use M.coe.edgeFinset.card
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
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))
rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]
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
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
convert_to _ = Finset.sum Finset.univ fun v => SimpleGraph.degree (Subgraph.coe M) v using 3
no goals
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
simp [h, Finset.card_univ]