-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma exists_isCycle_snd_verts_eq {p : G.Walk v v} (h : p.IsCycle) (hadj : p.toSubgraph.Adj v w) :
    ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w ∈ p.toSubgraph.neighborSet v
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
rw [h.neighborSet_toSubgraph_endpoint] at this

Result:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w ∈ {p.snd, p.penultimate}
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Proof state:
case inl
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hl : w = p.snd
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
exact ⟨p, ⟨h, hl.symm, rfl⟩⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w = p.snd ∨ w = p.penultimate
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
obtain hl | hr := this

Result:
case inl
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hl : w = p.snd
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

case inr
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.penultimate
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
have : w ∈ p.toSubgraph.neighborSet v := hadj

Result:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w ∈ p.toSubgraph.neighborSet v
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.reverse.getVert 1
⊢ p.reverse.toSubgraph.verts = p.toSubgraph.verts

Tactic:
rw [toSubgraph_reverse _]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w ∈ {p.snd, p.penultimate}
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at this

Result:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
this : w = p.snd ∨ w = p.penultimate
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Proof state:
case inr
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.penultimate
⊢ ∃ p', p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

Tactic:
use p.reverse

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.penultimate
⊢ p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.reverse.getVert 1
⊢ p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts

Tactic:
exact ⟨h.reverse, hr.symm, by rw [toSubgraph_reverse _]⟩

Result:
no goals

Proof state:
case h
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.penultimate
⊢ p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts

Tactic:
rw [penultimate, ← getVert_reverse] at hr

Result:
case h
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v v
h : p.IsCycle
hadj : p.toSubgraph.Adj v w
hr : w = p.reverse.getVert 1
⊢ p.reverse.IsCycle ∧ p.reverse.snd = w ∧ p.reverse.toSubgraph.verts = p.toSubgraph.verts