-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma neighborSet_toSubgraph_endpoint {u} {p : G.Walk u u} (hpc : p.IsCycle) :
    p.toSubgraph.neighborSet u = {p.snd, p.penultimate}

Proof state:
case h
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 : ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
hadj2 :
  ∃ i,
    (p.getVert i = u ∧ p.getVert (i + 1) = p.penultimate ∨ p.getVert i = p.penultimate ∧ p.getVert (i + 1) = u) ∧
      i < p.length
⊢ (∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length) →
    v = p.snd ∨ v = p.penultimate

Tactic:
rintro ⟨i, hl | hr⟩

Result:
case h.intro.intro.inl
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 : ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
hadj2 :
  ∃ i,
    (p.getVert i = u ∧ p.getVert (i + 1) = p.penultimate ∨ p.getVert i = p.penultimate ∧ p.getVert (i + 1) = u) ∧
      i < p.length
i : ℕ
right✝ : i < p.length
hl : p.getVert i = u ∧ p.getVert (i + 1) = v
⊢ v = p.snd ∨ v = p.penultimate

case h.intro.intro.inr
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 : ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
hadj2 :
  ∃ i,
    (p.getVert i = u ∧ p.getVert (i + 1) = p.penultimate ∨ p.getVert i = p.penultimate ∧ p.getVert (i + 1) = u) ∧
      i < p.length
i : ℕ
right✝ : i < p.length
hr : p.getVert i = v ∧ p.getVert (i + 1) = u
⊢ v = p.snd ∨ v = p.penultimate

Proof state:
case h.intro.intro.inl
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 : ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
hadj2 :
  ∃ i,
    (p.getVert i = u ∧ p.getVert (i + 1) = p.penultimate ∨ p.getVert i = p.penultimate ∧ p.getVert (i + 1) = u) ∧
      i < p.length
i : ℕ
right✝ : i < p.length
hl : p.getVert i = u ∧ p.getVert (i + 1) = v
⊢ v = p.snd ∨ v = p.penultimate

Tactic:
rw [hpc.getVert_endpoint_iff (by omega)] at hl

Result:
case h.intro.intro.inl
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 : ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
hadj2 :
  ∃ i,
    (p.getVert i = u ∧ p.getVert (i + 1) = p.penultimate ∨ p.getVert i = p.penultimate ∧ p.getVert (i + 1) = u) ∧
      i < p.length
i : ℕ
right✝ : i < p.length
hl : (i = 0 ∨ i = p.length) ∧ p.getVert (i + 1) = v
⊢ v = p.snd ∨ v = p.penultimate

Proof state:
case h
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 : ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
hadj2 :
  ∃ i,
    (p.getVert i = u ∧ p.getVert (i + 1) = p.penultimate ∨ p.getVert i = p.penultimate ∧ p.getVert (i + 1) = u) ∧
      i < p.length
⊢ (∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length) ↔
    v = p.snd ∨ v = p.penultimate

Tactic:
refine ⟨?_, by aesop⟩

Result:
case h
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 : ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
hadj2 :
  ∃ i,
    (p.getVert i = u ∧ p.getVert (i + 1) = p.penultimate ∨ p.getVert i = p.penultimate ∧ p.getVert (i + 1) = u) ∧
      i < p.length
⊢ (∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length) →
    v = p.snd ∨ v = p.penultimate

Proof state:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ p.toSubgraph.neighborSet u = {p.snd, p.penultimate}

Tactic:
have hadj1 := p.toSubgraph_adj_snd hpc.not_nil

Result:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
hadj1 : p.toSubgraph.Adj u p.snd
⊢ p.toSubgraph.neighborSet u = {p.snd, p.penultimate}

Proof state:
case h.intro.intro.inr.inr
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 : ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
hadj2 :
  ∃ i,
    (p.getVert i = u ∧ p.getVert (i + 1) = p.penultimate ∨ p.getVert i = p.penultimate ∧ p.getVert (i + 1) = u) ∧
      i < p.length
i : ℕ
right✝ : i < p.length
hr : p.getVert i = v ∧ p.getVert (i + 1) = u
h2 : i + 1 = p.length
⊢ v = p.snd ∨ v = p.penultimate

Tactic:
simp only [penultimate, ← h2, add_tsub_cancel_right]

Result:
case h.intro.intro.inr.inr
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
hadj1 : ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = p.snd ∨ p.getVert i = p.snd ∧ p.getVert (i + 1) = u) ∧ i < p.length
hadj2 :
  ∃ i,
    (p.getVert i = u ∧ p.getVert (i + 1) = p.penultimate ∨ p.getVert i = p.penultimate ∧ p.getVert (i + 1) = u) ∧
      i < p.length
i : ℕ
right✝ : i < p.length
hr : p.getVert i = v ∧ p.getVert (i + 1) = u
h2 : i + 1 = p.length
⊢ v = p.snd ∨ v = p.getVert i