-- Mathlib/Combinatorics/SimpleGraph/Trails.lean
theorem IsEulerian.even_degree_iff {x u v : V} {p : G.Walk u v} (ht : p.IsEulerian) [Fintype V]
    [DecidableRel G.Adj] : Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v

Proof state:
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.degree x = List.countP (fun e => decide (x ∈ e)) p.edges

Tactic:
rw [← Multiset.coe_countP, Multiset.countP_eq_card_filter, ← card_incidenceFinset_eq_degree]

Result:
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (G.incidenceFinset x).card = (Multiset.filter (fun e => x ∈ e) ↑p.edges).card

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v

Tactic:
convert ht.isTrail.even_countP_edges_iff x

Result:
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.degree x = List.countP (fun e => decide (x ∈ e)) p.edges

Proof state:
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (G.incidenceFinset x).card = (Multiset.filter (fun e => x ∈ e) ↑p.edges).card

Tactic:
change Multiset.card _ = _

Result:
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (G.incidenceFinset x).val.card = (Multiset.filter (fun e => x ∈ e) ↑p.edges).card

Proof state:
case h.e'_1.h.e'_3.e_a.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (G.incidenceFinset x).val = (Finset.filter (fun x_1 => x ∈ x_1) ⋯.edgesFinset).val

Tactic:
have : Fintype G.edgeSet := fintypeEdgeSet ht

Result:
case h.e'_1.h.e'_3.e_a.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
this : Fintype ↑G.edgeSet
⊢ (G.incidenceFinset x).val = (Finset.filter (fun x_1 => x ∈ x_1) ⋯.edgesFinset).val

Proof state:
case h.e'_1.h.e'_3.e_a.convert_2
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
this : Fintype ↑G.edgeSet
⊢ (G.incidenceFinset x).val = (Finset.filter (fun x_1 => x ∈ x_1) ⋯.edgesFinset).val

Tactic:
rw [ht.edgesFinset_eq, G.incidenceFinset_eq_filter x]

Result:
no goals

Proof state:
case h.e'_1.h.e'_3
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (G.incidenceFinset x).val.card = (Multiset.filter (fun e => x ∈ e) ↑p.edges).card

Tactic:
congr 1

Result:
case h.e'_1.h.e'_3.e_a
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
x u v : V
p : G.Walk u v
ht : p.IsEulerian
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ (G.incidenceFinset x).val = Multiset.filter (fun e => x ∈ e) ↑p.edges