V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G v u
h : Adj G u v
⊢ (¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p ∧ List.Nodup (edges p)) ∧ cons h p ≠ nil ∧ List.Nodup (support p) ↔
    List.Nodup (support p) ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G v u
h : Adj G u v
⊢ IsCycle (cons h p) ↔ IsPath p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
simp only [Walk.isCycle_def, Walk.isPath_def, Walk.isTrail_def, edges_cons, List.nodup_cons,
  support_cons, List.tail_cons]
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G v u
h : Adj G u v
this : List.Nodup (support p) → List.Nodup (edges p)
⊢ (¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p ∧ List.Nodup (edges p)) ∧ cons h p ≠ nil ∧ List.Nodup (support p) ↔
    List.Nodup (support p) ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G v u
h : Adj G u v
⊢ (¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p ∧ List.Nodup (edges p)) ∧ cons h p ≠ nil ∧ List.Nodup (support p) ↔
    List.Nodup (support p) ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
have : p.support.Nodup → p.edges.Nodup := edges_nodup_of_support_nodup
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G v u
h : Adj G u v
this : List.Nodup (support p) → List.Nodup (edges p)
⊢ (¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p ∧ List.Nodup (edges p)) ∧ cons h p ≠ nil ∧ List.Nodup (support p) ↔
    List.Nodup (support p) ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ edges p
tauto