Theorem: Digraph.set_walk_self_length_zero_eq (GraphProjects/DigraphConnectivity.lean)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
⊢ {p | Walk.length p = 0} = {Walk.nil}
Tactic:
ext p
State after:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
p : Walk G u u
⊢ p ∈ {p | Walk.length p = 0} ↔ p ∈ {Walk.nil}

State before:
case h
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u : V
p : Walk G u u
⊢ p ∈ {p | Walk.length p = 0} ↔ p ∈ {Walk.nil}
Tactic:
simp
State after:
no goals