-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma neighborSet_toSubgraph_internal {u} {i : ℕ} {p : G.Walk u u} (hpc : p.IsCycle)
    (h : i ≠ 0) (h' : i < p.length) :
    p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
⊢ i < p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
hadj2 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i + 1))
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Tactic:
ext v

Result:
case h
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
hadj2 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i + 1))
v : V
⊢ v ∈ p.toSubgraph.neighborSet (p.getVert i) ↔ v ∈ {p.getVert (i - 1), p.getVert (i + 1)}

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Tactic:
have hadj2 := p.toSubgraph_adj_getVert (by omega : i < p.length)

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
hadj2 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i + 1))
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
⊢ i - 1 < p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
hadj2 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i + 1) ∨
        p.getVert i_1 = p.getVert (i + 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ 1 ≤ i ∧ i ≤ p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
hadj2 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i + 1) ∨
        p.getVert i_1 = p.getVert (i + 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 ∈ {i | 1 ≤ i ∧ i ≤ p.length}

Tactic:
rw [Set.mem_setOf_eq]

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
hadj2 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i + 1) ∨
        p.getVert i_1 = p.getVert (i + 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : p.getVert (i' + 1) = p.getVert i
⊢ 1 ≤ i' + 1 ∧ i' + 1 ≤ p.length

Proof state:
case h.intro.intro.inr.intro
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
hadj2 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i + 1) ∨
        p.getVert i_1 = p.getVert (i + 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : i' + 1 = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Tactic:
have hadj1 := ((show i - 1 + 1 = i from by omega) ▸
  p.toSubgraph_adj_getVert (by omega : (i - 1) < p.length)).symm

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
hadj1 : p.toSubgraph.Adj (p.getVert i) (p.getVert (i - 1))
⊢ p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
h : i ≠ 0
h' : i < p.length
⊢ i - 1 + 1 = i

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
hadj2 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i + 1) ∨
        p.getVert i_1 = p.getVert (i + 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i ≤ p.length - 1

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
hadj2 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i + 1) ∨
        p.getVert i_1 = p.getVert (i + 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i' ∈ {i | i ≤ p.length - 1}

Tactic:
rw [Set.mem_setOf_eq]

Result:
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
hadj2 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i + 1) ∨
        p.getVert i_1 = p.getVert (i + 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hl1 : p.getVert i' = p.getVert i
hl2 : p.getVert (i' + 1) = v
⊢ i' ≤ p.length - 1