V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
⊢ False
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
⊢ False
have hv := c.fst_mem_support_of_mem_edges he
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
⊢ False
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
⊢ False
let puw := (c.takeUntil v hv).takeUntil w hw
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
⊢ False
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
⊢ False
let pwv := (c.takeUntil v hv).dropUntil w hw
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
⊢ False
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
⊢ False
let pvu := c.dropUntil v hv
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
this : c = Walk.append (Walk.append puw pwv) pvu
⊢ False
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
⊢ False
have : c = (puw.append pwv).append pvu := by simp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
this : c = Walk.append (Walk.append puw pwv) pvu
hbq : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.append pvu puw)
⊢ False
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
this : c = Walk.append (Walk.append puw pwv) pvu
⊢ False
have hbq := hb (pvu.append puw)
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
this : c = Walk.append (Walk.append puw pwv) pvu
hbq : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.append pvu puw)
hpq' : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.reverse pwv)
⊢ False
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
this : c = Walk.append (Walk.append puw pwv) pvu
hbq : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.append pvu puw)
⊢ False
have hpq' := hb pwv.reverse
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
this : c = Walk.append (Walk.append puw pwv) pvu
hbq : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.append pvu puw)
hpq' : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges pwv
⊢ False
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
this : c = Walk.append (Walk.append puw pwv) pvu
hbq : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.append pvu puw)
hpq' : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.reverse pwv)
⊢ False
rw [Walk.edges_reverse, List.mem_reverse'] at hpq'
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
hc : List.Nodup (Walk.edges (Walk.append pvu puw) ++ Walk.edges pwv)
this : c = Walk.append (Walk.append puw pwv) pvu
hbq : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.append pvu puw)
hpq' : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges pwv
⊢ False
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
this : c = Walk.append (Walk.append puw pwv) pvu
hbq : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.append pvu puw)
hpq' : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges pwv
⊢ False
rw [Walk.isTrail_def, this, Walk.edges_append, Walk.edges_append, List.nodup_append_comm,
  ← List.append_assoc, ← Walk.edges_append] at hc
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
hc : List.Nodup (Walk.edges (Walk.append pvu puw) ++ Walk.edges pwv)
this : c = Walk.append (Walk.append puw pwv) pvu
hbq : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.append pvu puw)
hpq' : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges pwv
⊢ False
exact List.disjoint_of_nodup_append hc hbq hpq'
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝ : DecidableEq V
u v w : V
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
c : Walk G u u
hc : Walk.IsTrail c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hw : w ∈ Walk.support (Walk.takeUntil c v (_ : v ∈ Walk.support c))
hv : v ∈ Walk.support c
puw : Walk G u w := Walk.takeUntil (Walk.takeUntil c v hv) w hw
pwv : Walk G w v := Walk.dropUntil (Walk.takeUntil c v hv) w hw
pvu : Walk G v u := Walk.dropUntil c v hv
⊢ c = Walk.append (Walk.append puw pwv) pvu
simp