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 (Finset.filter (fun v => Odd (degree G v)) Finset.univ) = 0 ∨
    Finset.card (Finset.filter (fun v => Odd (degree G v)) Finset.univ) = 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
s : Finset V
h : s = Finset.filter (fun v => Odd (degree G v)) Finset.univ
⊢ Finset.card s = 0 ∨ Finset.card s = 2
subst s
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.filter (fun v => ¬Even (degree G v)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v => ¬Even (degree G v)) Finset.univ) = 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
⊢ Finset.card (Finset.filter (fun v => Odd (degree G v)) Finset.univ) = 0 ∨
    Finset.card (Finset.filter (fun v => Odd (degree G v)) Finset.univ) = 2
simp only [Nat.odd_iff_not_even, Finset.card_eq_zero]
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.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = 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
⊢ Finset.filter (fun v => ¬Even (degree G v)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v => ¬Even (degree G v)) Finset.univ) = 2
simp only [ht.even_degree_iff, Ne.def, not_forall, not_and, Classical.not_not, exists_prop]
case inl
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u : V
p : Walk G u u
ht : IsEulerian p
⊢ Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ) = 2

case inr
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
hn : u ≠ v
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = 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
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = 2
obtain rfl | hn := eq_or_ne u v
case inl.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u : V
p : Walk G u u
ht : IsEulerian p
⊢ Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ = ∅
case inl
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u : V
p : Walk G u u
ht : IsEulerian p
⊢ Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ) = 2
left
no goals
case inl.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u : V
p : Walk G u u
ht : IsEulerian p
⊢ Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ = ∅
simp
case inr.h
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
hn : u ≠ v
⊢ Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = 2
case inr
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
hn : u ≠ v
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨
    Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = 2
right
case h.e'_3
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
hn : u ≠ v
⊢ 2 = Finset.card {u, v}

case inr.h
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
hn : u ≠ v
⊢ Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = Finset.card {u, v}
case inr.h
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
hn : u ≠ v
⊢ Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = 2
convert_to _ = ({u, v} : Finset V).card
no goals
case h.e'_3
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
hn : u ≠ v
⊢ 2 = Finset.card {u, v}
simp [hn]
case inr.h.e_s
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
hn : u ≠ v
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = {u, v}
case inr.h
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
hn : u ≠ v
⊢ Finset.card (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ) = Finset.card {u, v}
congr
case inr.h.e_s.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
hn : u ≠ v
x : V
⊢ x ∈ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ ↔ x ∈ {u, v}
case inr.h.e_s
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
hn : u ≠ v
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = {u, v}
ext x
no goals
case inr.h.e_s.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
hn : u ≠ v
x : V
⊢ x ∈ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ ↔ x ∈ {u, v}
simp [hn, imp_iff_not_or]