-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma neighborSet_toSubgraph_internal {u} {i : ℕ} {p : G.Walk u v} (hp : p.IsPath)
    (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
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
⊢ i - 1 < p.length

Tactic:
omega

Result:
no goals

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

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 ≤ p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
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:
ext v

Result:
case h
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
hadj1 : 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
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_setOf_eq]

Result:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i ≤ p.length

Proof state:
case h
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
h : i ≠ 0
h' : i < p.length
hadj1 : 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)}

Tactic:
simp_all only [ne_eq, 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
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
⊢ (∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) ↔
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Proof state:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1) →
    ∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 ∈ {i | i ≤ p.length}

Tactic:
rw [Set.mem_setOf_eq]

Result:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i' + 1 ≤ p.length

Proof state:
V : Type u
G : SimpleGraph V
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
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
v u : V
i : ℕ
p : G.Walk u v
hp : p.IsPath
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:
case h
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
⊢ (∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) ↔
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
refine ⟨?_, by aesop⟩

Result:
case h
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
⊢ (∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) →
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Proof state:
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : p.getVert (i' + 1) = p.getVert i
⊢ i ≤ p.length

Tactic:
omega

Result:
no goals

Proof state:
case h
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
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
⊢ (∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length) →
    v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
rintro ⟨i', ⟨hl, _⟩ | ⟨_, hl⟩⟩ <;>
  apply hp.getVert_injOn (by rw [Set.mem_setOf_eq]; omega)
    (by rw [Set.mem_setOf_eq]; omega) at hl <;> aesop

Result:
no goals