V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ (Adj G v w ∧ ∃ p, ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p) ↔
    ∃ u p, Walk.IsCycle p ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ Adj G v w ∧ Reachable (G \ fromEdgeSet {Quotient.mk (Sym2.Rel.setoid V) (v, w)}) v w ↔
    ∃ u p, Walk.IsCycle p ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
rw [reachable_delete_edges_iff_exists_walk]
case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ (Adj G v w ∧ ∃ p, ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p) →
    ∃ u p, Walk.IsCycle p ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p

case mpr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ (∃ u p, Walk.IsCycle p ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p) →
    Adj G v w ∧ ∃ p, ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ (Adj G v w ∧ ∃ p, ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p) ↔
    ∃ u p, Walk.IsCycle p ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
constructor
case mp.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ ∃ u p, Walk.IsCycle p ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
case mp
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ (Adj G v w ∧ ∃ p, ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p) →
    ∃ u p, Walk.IsCycle p ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
rintro ⟨h, p, hp⟩
case mp.intro.intro.refine_1
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ Walk.IsCycle (Walk.cons (_ : Adj G w v) ↑(Walk.toPath p))

case mp.intro.intro.refine_2
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.cons (_ : Adj G w v) ↑(Walk.toPath p))
case mp.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ ∃ u p, Walk.IsCycle p ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
refine ⟨w, Walk.cons h.symm p.toPath, ?_, ?_⟩
case mp.intro.intro.refine_1.he
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ ¬Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges ↑(Walk.toPath p)
case mp.intro.intro.refine_1
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ Walk.IsCycle (Walk.cons (_ : Adj G w v) ↑(Walk.toPath p))
apply Path.cons_isCycle
case mp.intro.intro.refine_1.he
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges ↑(Walk.toPath p)
case mp.intro.intro.refine_1.he
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ ¬Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges ↑(Walk.toPath p)
rw [Sym2.eq_swap]
case mp.intro.intro.refine_1.he
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h✝ : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges ↑(Walk.toPath p)
⊢ False
case mp.intro.intro.refine_1.he
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges ↑(Walk.toPath p)
intro h
no goals
case mp.intro.intro.refine_1.he
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h✝ : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
h : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges ↑(Walk.toPath p)
⊢ False
cases hp (Walk.edges_toPath_subset p h)
no goals
case mp.intro.intro.refine_2
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
h : Adj G v w
p : Walk G v w
hp : ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges (Walk.cons (_ : Adj G w v) ↑(Walk.toPath p))
simp only [Sym2.eq_swap, Walk.edges_cons, List.mem_cons, eq_self_iff_true, true_or_iff]
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
⊢ Adj G v w ∧ ∃ p, ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
case mpr
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w : V
⊢ (∃ u p, Walk.IsCycle p ∧ Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p) →
    Adj G v w ∧ ∃ p, ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
rintro ⟨u, c, hc, he⟩
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
⊢ ∃ p, ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
⊢ Adj G v w ∧ ∃ p, ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
refine ⟨c.adj_of_mem_edges he, ?_⟩
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ False
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
⊢ ∃ p, ¬Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
by_contra' hb
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
hb' : ∀ (p : Walk G w v), Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges p
⊢ False
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ False
have hb' : ∀ p : G.Walk w v, ⟦(w, v)⟧ ∈ p.edges := by
  intro p
  simpa [Sym2.eq_swap] using hb p.reverse
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
hb' : ∀ (p : Walk G w v), Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges p
hvc : v ∈ Walk.support c
⊢ False
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
hb' : ∀ (p : Walk G w v), Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges p
⊢ False
have hvc : v ∈ c.support := Walk.fst_mem_support_of_mem_edges c he
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
hb' : ∀ (p : Walk G w v), Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges p
hvc : v ∈ Walk.support c
⊢ Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges (Walk.rotate c hvc)
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
hb' : ∀ (p : Walk G w v), Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges p
hvc : v ∈ Walk.support c
⊢ False
refine reachable_deleteEdges_iff_exists_cycle.aux hb' (c.rotate hvc) (hc.isTrail.rotate hvc)
  ?_ (Walk.start_mem_support _)
no goals
case mpr.intro.intro.intro
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
hb' : ∀ (p : Walk G w v), Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges p
hvc : v ∈ Walk.support c
⊢ Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges (Walk.rotate c hvc)
rwa [(Walk.rotate_edges c hvc).mem_iff, Sym2.eq_swap]
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
p : Walk G w v
⊢ Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges p
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
⊢ ∀ (p : Walk G w v), Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges p
intro p
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u : V
c : Walk G u u
hc : Walk.IsCycle c
he : Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges c
hb : ∀ (p : Walk G v w), Quotient.mk (Sym2.Rel.setoid V) (v, w) ∈ Walk.edges p
p : Walk G w v
⊢ Quotient.mk (Sym2.Rel.setoid V) (w, v) ∈ Walk.edges p
simpa [Sym2.eq_swap] using hb p.reverse