-- Mathlib/Combinatorics/SimpleGraph/Trails.lean
theorem IsEulerian.card_filter_odd_degree [Fintype V] [DecidableRel G.Adj] {u v : V}
    {p : G.Walk u v} (ht : p.IsEulerian) {s}
    (h : s = (Finset.univ : Finset V).filter fun v => Odd (G.degree v)) :
    s.card = 0 ∨ s.card = 2

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
s : Finset V
h : s = Finset.filter (fun v => Odd (G.degree v)) Finset.univ
⊢ s.card = 0 ∨ s.card = 2

Tactic:
subst s

Result:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ (Finset.filter (fun v => Odd (G.degree v)) Finset.univ).card = 0 ∨
    (Finset.filter (fun v => Odd (G.degree v)) Finset.univ).card = 2

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ (Finset.filter (fun v => Odd (G.degree v)) Finset.univ).card = 0 ∨
    (Finset.filter (fun v => Odd (G.degree v)) Finset.univ).card = 2

Tactic:
simp only [← Nat.not_even_iff_odd, Finset.card_eq_zero]

Result:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Finset.filter (fun v => ¬Even (G.degree v)) Finset.univ = ∅ ∨
    (Finset.filter (fun v => ¬Even (G.degree v)) Finset.univ).card = 2

Proof state:
case inr.h.convert_2.e_s
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = {u, v}

Tactic:
ext x

Result:
case inr.h.convert_2.e_s.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
x : V
⊢ x ∈ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ ↔ x ∈ {u, v}

Proof state:
case inl
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u : V
p : G.Walk u u
ht : p.IsEulerian
⊢ Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ = ∅ ∨
    (Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ).card = 2

Tactic:
left

Result:
case inl.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u : V
p : G.Walk u u
ht : p.IsEulerian
⊢ Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ = ∅

Proof state:
case inr.h.convert_2.e_s.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
x : V
⊢ x ∈ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ ↔ x ∈ {u, v}

Tactic:
simp [hn, imp_iff_not_or]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Finset.filter (fun v => ¬Even (G.degree v)) Finset.univ = ∅ ∨
    (Finset.filter (fun v => ¬Even (G.degree v)) Finset.univ).card = 2

Tactic:
simp only [ht.even_degree_iff, Ne, not_forall, not_and, Classical.not_not, exists_prop]

Result:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨
    (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ).card = 2

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨
    (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ).card = 2

Tactic:
obtain rfl | hn := eq_or_ne u v

Result:
case inl
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u : V
p : G.Walk u u
ht : p.IsEulerian
⊢ Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ = ∅ ∨
    (Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ).card = 2

case inr
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨
    (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ).card = 2

Proof state:
case inr
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = ∅ ∨
    (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ).card = 2

Tactic:
right

Result:
case inr.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ).card = 2

Proof state:
case inl.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u : V
p : G.Walk u u
ht : p.IsEulerian
⊢ Finset.filter (fun v => ¬u = u ∧ (¬v = u → v = u)) Finset.univ = ∅

Tactic:
simp

Result:
no goals

Proof state:
case inr.h.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ).card = {u, v}.card

Tactic:
congr

Result:
case inr.h.convert_2.e_s
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ = {u, v}

Proof state:
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 : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ 2 = {u, v}.card

Tactic:
simp [hn]

Result:
no goals

Proof state:
case inr.h
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ).card = 2

Tactic:
convert_to _ = ({u, v} : Finset V).card

Result:
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 : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ 2 = {u, v}.card

case inr.h.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ (Finset.filter (fun v_1 => ¬u = v ∧ (¬v_1 = u → v_1 = v)) Finset.univ).card = {u, v}.card