V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
c : Walk G v v
hc : Walk.IsCycle c
⊢ False
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
⊢ IsAcyclic G
intro v c hc
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
c : Walk G v v
hc : Walk.IsTrail c ∧ ¬c = Walk.nil ∧ List.Nodup (List.tail (Walk.support c))
⊢ False
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
c : Walk G v v
hc : Walk.IsCycle c
⊢ False
simp only [Walk.isCycle_def, Ne.def] at hc
no goals
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
c : Walk G v v
hc : Walk.IsTrail c ∧ ¬c = Walk.nil ∧ List.Nodup (List.tail (Walk.support c))
⊢ False
cases c with
| nil => cases hc.2.1 rfl
| cons ha c' =>
  simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons, true_and_iff] at hc
  specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
  rw [Path.singleton, Subtype.mk.injEq] at h
  simp [h] at hc
no goals
case nil
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v : V
hc : Walk.IsTrail Walk.nil ∧ ¬Walk.nil = Walk.nil ∧ List.Nodup (List.tail (Walk.support Walk.nil))
⊢ False
cases hc.2.1 rfl
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (Walk.IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Walk.edges c') ∧ List.Nodup (Walk.support c')
⊢ False
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc :
  Walk.IsTrail (Walk.cons ha c') ∧ ¬Walk.cons ha c' = Walk.nil ∧ List.Nodup (List.tail (Walk.support (Walk.cons ha c')))
⊢ False
simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons, true_and_iff] at hc
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (Walk.IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Walk.edges c') ∧ List.Nodup (Walk.support c')
h : { val := c', property := (_ : Walk.IsPath c') } = Path.singleton (_ : Adj G v✝ v)
⊢ False
case cons
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (Walk.IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Walk.edges c') ∧ List.Nodup (Walk.support c')
⊢ False
specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (Walk.IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Walk.edges c') ∧ List.Nodup (Walk.support c')
h : c' = Walk.cons (_ : Adj G v✝ v) Walk.nil
⊢ False
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (Walk.IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Walk.edges c') ∧ List.Nodup (Walk.support c')
h : { val := c', property := (_ : Walk.IsPath c') } = Path.singleton (_ : Adj G v✝ v)
⊢ False
rw [Path.singleton, Subtype.mk.injEq] at h
no goals
case cons
V : Type u
G : SimpleGraph V
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (Walk.IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Walk.edges c') ∧ List.Nodup (Walk.support c')
h : c' = Walk.cons (_ : Adj G v✝ v) Walk.nil
⊢ False
simp [h] at hc
no goals
V : Type u
G : SimpleGraph V
h : ∀ (v w : V) (p q : Path G v w), p = q
v v✝ : V
ha : Adj G v v✝
c' : Walk G v✝ v
hc : (Walk.IsTrail c' ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (v, v✝) ∈ Walk.edges c') ∧ List.Nodup (Walk.support c')
⊢ Walk.IsPath c'
simp only [Walk.isPath_def, hc.2]