case a
V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑(edgeSet G)
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
⊢ e ∈ IsTrail.edgesFinset (_ : IsTrail p) ↔ e ∈ edgeFinset G
V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑(edgeSet G)
u v : V
p : Walk G u v
h : IsEulerian p
⊢ IsTrail.edgesFinset (_ : IsTrail p) = edgeFinset G
ext e
no goals
case a
V : Type u_1
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑(edgeSet G)
u v : V
p : Walk G u v
h : IsEulerian p
e : Sym2 V
⊢ e ∈ IsTrail.edgesFinset (_ : IsTrail p) ↔ e ∈ edgeFinset G
simp [h.mem_edges_iff]