-- 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.intro.intro.inr.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
hr : p.getVert i = v ∧ p.getVert (i + 1) = u
h1 : i + 1 = 0
⊢ v = p.snd ∨ v = p.penultimate

Tactic:
contradiction

Result:
no goals

Proof state:
case h
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
hadj1 : p.toSubgraph.Adj u p.snd
hadj2 : p.toSubgraph.Adj u p.penultimate
v : V
⊢ v ∈ p.toSubgraph.neighborSet u ↔ v ∈ {p.snd, p.penultimate}

Tactic:
simp_all only [Subgraph.mem_neighborSet, Set.mem_insert_iff, Set.mem_singleton_iff,
  SimpleGraph.Walk.toSubgraph_adj_iff, Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk]

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
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
⊢ v = p.snd ∨ v = p.penultimate →
    ∃ i, (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length

Tactic:
aesop

Result:
no goals

Proof state:
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}

Tactic:
have hadj2 := (p.toSubgraph_adj_penultimate hpc.not_nil).symm

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

Proof state:
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
⊢ i ≤ p.length

Tactic:
omega

Result:
no goals

Proof state:
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

Tactic:
rcases (hpc.getVert_endpoint_iff (by omega)).mp hr.2 with h1 | h2

Result:
case h.intro.intro.inr.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
hr : p.getVert i = v ∧ p.getVert (i + 1) = u
h1 : i + 1 = 0
⊢ v = p.snd ∨ v = p.penultimate

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

Proof state:
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
⊢ i + 1 ≤ p.length

Tactic:
omega

Result:
no goals

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 : (i = 0 ∨ i = p.length) ∧ p.getVert (i + 1) = v
⊢ v = p.snd ∨ v = p.penultimate

Tactic:
cases hl.1 <;> aesop

Result:
no goals

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

Tactic:
ext v

Result:
case h
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
hadj1 : p.toSubgraph.Adj u p.snd
hadj2 : p.toSubgraph.Adj u p.penultimate
v : V
⊢ v ∈ p.toSubgraph.neighborSet u ↔ v ∈ {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.getVert i

Tactic:
aesop

Result:
no goals