case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
⊢ IsEulerian p → IsTrail p ∧ ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p

case mpr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
⊢ (IsTrail p ∧ ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p) → IsEulerian p
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
⊢ IsEulerian p ↔ IsTrail p ∧ ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p
constructor
case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
⊢ IsTrail p ∧ ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p
case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
⊢ IsEulerian p → IsTrail p ∧ ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p
intro h
no goals
case mp
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsEulerian p
⊢ IsTrail p ∧ ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p
exact ⟨h.isTrail, fun _ => h.mem_edges_iff.mpr⟩
case mpr.intro
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsTrail p
hl : ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p
⊢ IsEulerian p
case mpr
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
⊢ (IsTrail p ∧ ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p) → IsEulerian p
rintro ⟨h, hl⟩
no goals
case mpr.intro
V : Type u_1
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
p : Walk G u v
h : IsTrail p
hl : ∀ (e : Sym2 V), e ∈ edgeSet G → e ∈ edges p
⊢ IsEulerian p
exact h.isEulerian_of_forall_mem hl