V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
⊢ Finset.card (Set.toFinset {v | Odd (degree G v)}) = 0 ∨ Finset.card (Set.toFinset {v | Odd (degree G v)}) = 2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
⊢ Fintype.card ↑{v | Odd (degree G v)} = 0 ∨ Fintype.card ↑{v | Odd (degree G v)} = 2
rw [← Set.toFinset_card]
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
⊢ Set.toFinset {v | Odd (degree G v)} = Finset.filter (fun v => Odd (degree G v)) Finset.univ
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
⊢ Finset.card (Set.toFinset {v | Odd (degree G v)}) = 0 ∨ Finset.card (Set.toFinset {v | Odd (degree G v)}) = 2
apply IsEulerian.card_filter_odd_degree ht
case a
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v✝ : V
p : Walk G u v✝
ht : IsEulerian p
v : V
⊢ v ∈ Set.toFinset {v | Odd (degree G v)} ↔ v ∈ Finset.filter (fun v => Odd (degree G v)) Finset.univ
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : Walk G u v
ht : IsEulerian p
⊢ Set.toFinset {v | Odd (degree G v)} = Finset.filter (fun v => Odd (degree G v)) Finset.univ
ext v
no goals
case a
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v✝ : V
p : Walk G u v✝
ht : IsEulerian p
v : V
⊢ v ∈ Set.toFinset {v | Odd (degree G v)} ↔ v ∈ Finset.filter (fun v => Odd (degree G v)) Finset.univ
simp