-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem adj_and_reachable_delete_edges_iff_exists_cycle {v w : V} :
    G.Adj v w ∧ (G \ fromEdgeSet {s(v, w)}).Reachable v w ↔
      ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges

Proof state:
case mp
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges) → ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
rintro ⟨h, p, hp⟩

Result:
case mp.intro.intro
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges) ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges) → ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

case mpr
V : Type u
G : SimpleGraph V
v w : V
⊢ (∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges) → G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges

Proof state:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
⊢ ∃ p, s(v, w) ∉ p.edges

Tactic:
by_contra! hb

Result:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
⊢ False

Proof state:
case mp.intro.intro.refine_1.he
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(w, v) ∉ (↑p.toPath).edges

Tactic:
rw [Sym2.eq_swap]

Result:
case mp.intro.intro.refine_1.he
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∉ (↑p.toPath).edges

Proof state:
case mp.intro.intro
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
refine ⟨w, Walk.cons h.symm p.toPath, ?_, ?_⟩

Result:
case mp.intro.intro.refine_1
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ (Walk.cons ⋯ ↑p.toPath).IsCycle

case mp.intro.intro.refine_2
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∈ (Walk.cons ⋯ ↑p.toPath).edges

Proof state:
case mp.intro.intro.refine_1.he
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∉ (↑p.toPath).edges

Tactic:
intro h

Result:
case mp.intro.intro.refine_1.he
V : Type u
G : SimpleGraph V
v w : V
h✝ : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
h : s(v, w) ∈ (↑p.toPath).edges
⊢ False

Proof state:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
⊢ False

Tactic:
have hvc : v ∈ c.support := Walk.fst_mem_support_of_mem_edges c he

Result:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
hvc : v ∈ c.support
⊢ False

Proof state:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
hvc : v ∈ c.support
⊢ s(w, v) ∈ (c.rotate hvc).edges

Tactic:
rwa [(Walk.rotate_edges c hvc).mem_iff, Sym2.eq_swap]

Result:
no goals

Proof state:
case mp.intro.intro.refine_2
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(v, w) ∈ (Walk.cons ⋯ ↑p.toPath).edges

Tactic:
simp only [Sym2.eq_swap, Walk.edges_cons, List.mem_cons, eq_self_iff_true, true_or]

Result:
no goals

Proof state:
case mpr
V : Type u
G : SimpleGraph V
v w : V
⊢ (∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges) → G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges

Tactic:
rintro ⟨u, c, hc, he⟩

Result:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
⊢ G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges

Proof state:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
p : G.Walk w v
⊢ s(w, v) ∈ p.edges

Tactic:
simpa [Sym2.eq_swap] using hb p.reverse

Result:
no goals

Proof state:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
⊢ G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges

Tactic:
refine ⟨c.adj_of_mem_edges he, ?_⟩

Result:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
⊢ ∃ p, s(v, w) ∉ p.edges

Proof state:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
⊢ ∀ (p : G.Walk w v), s(w, v) ∈ p.edges

Tactic:
intro p

Result:
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
p : G.Walk w v
⊢ s(w, v) ∈ p.edges

Proof state:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
⊢ False

Tactic:
have hb' : ∀ p : G.Walk w v, s(w, v) ∈ p.edges := by
  intro p
  simpa [Sym2.eq_swap] using hb p.reverse

Result:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
⊢ False

Proof state:
case mp.intro.intro.refine_1.he
V : Type u
G : SimpleGraph V
v w : V
h✝ : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
h : s(v, w) ∈ (↑p.toPath).edges
⊢ False

Tactic:
cases hp (Walk.edges_toPath_subset p h)

Result:
no goals

Proof state:
case mp.intro.intro.refine_1
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ (Walk.cons ⋯ ↑p.toPath).IsCycle

Tactic:
apply Path.cons_isCycle

Result:
case mp.intro.intro.refine_1.he
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(w, v) ∉ (↑p.toPath).edges

Proof state:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
hvc : v ∈ c.support
⊢ False

Tactic:
refine reachable_deleteEdges_iff_exists_cycle.aux hb' (c.rotate hvc) (hc.isTrail.rotate hvc)
  ?_ (Walk.start_mem_support _)

Result:
case mpr.intro.intro.intro
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
hvc : v ∈ c.support
⊢ s(w, v) ∈ (c.rotate hvc).edges

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.Adj v w ∧ (G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
rw [reachable_delete_edges_iff_exists_walk]

Result:
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.Adj v w ∧ ∃ p, s(v, w) ∉ p.edges) ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges