V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
⊢ ∀ (a : Sym2 V), List.count a (edges p) ≤ 1
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
⊢ IsTrail p
rw [isTrail_def, List.nodup_iff_count_le_one]
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
⊢ List.count e (edges p) ≤ 1
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
⊢ ∀ (a : Sym2 V), List.count a (edges p) ≤ 1
intro e
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
he : e ∈ edges p
⊢ List.count e (edges p) ≤ 1

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
he : ¬e ∈ edges p
⊢ List.count e (edges p) ≤ 1
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
⊢ List.count e (edges p) ≤ 1
by_cases he : e ∈ p.edges
no goals
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
he : e ∈ edges p
⊢ List.count e (edges p) ≤ 1
exact (h e (edges_subset_edgeSet _ he)).le
no goals
case neg
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
he : ¬e ∈ edges p
⊢ List.count e (edges p) ≤ 1
simp [he]