-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma neighborSet_toSubgraph_startpoint {u v} {p : G.Walk u v}
    (hp : p.IsPath) (hnp : ¬ p.Nil) : p.toSubgraph.neighborSet u = {p.snd}

Proof state:
case h.intro.intro.inr
V : Type u
G : SimpleGraph V
u v✝ : V
p : G.Walk u v✝
hp : p.IsPath
hnp : ¬p.Nil
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
i : ℕ
right✝ : i < p.length
hr : p.getVert i = v ∧ p.getVert (i + 1) = u
⊢ v = p.snd

Tactic:
have : i + 1 = 0 := by
  apply hp.getVert_injOn (by rw [Set.mem_setOf]; omega) (by rw [Set.mem_setOf]; omega)
  aesop

Result:
case h.intro.intro.inr
V : Type u
G : SimpleGraph V
u v✝ : V
p : G.Walk u v✝
hp : p.IsPath
hnp : ¬p.Nil
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
i : ℕ
right✝ : i < p.length
hr : p.getVert i = v ∧ p.getVert (i + 1) = u
this : i + 1 = 0
⊢ v = p.snd

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

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v✝ : V
p : G.Walk u v✝
hp : p.IsPath
hnp : ¬p.Nil
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
i : ℕ
right✝ : i < p.length
hr : p.getVert i = v ∧ p.getVert (i + 1) = u
⊢ p.getVert (i + 1) = p.getVert 0

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v✝ : V
p : G.Walk u v✝
hp : p.IsPath
hnp : ¬p.Nil
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
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:
V : Type u
G : SimpleGraph V
u v✝ : V
p : G.Walk u v✝
hp : p.IsPath
hnp : ¬p.Nil
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
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:
V : Type u
G : SimpleGraph V
u v✝ : V
p : G.Walk u v✝
hp : p.IsPath
hnp : ¬p.Nil
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
i : ℕ
right✝ : i < p.length
hr : p.getVert i = v ∧ p.getVert (i + 1) = u
⊢ 0 ≤ p.length

Tactic:
omega

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
hadj1 : p.toSubgraph.Adj u p.snd
⊢ p.toSubgraph.neighborSet u = {p.snd}

Tactic:
ext v

Result:
case h
V : Type u
G : SimpleGraph V
u v✝ : V
p : G.Walk u v✝
hp : p.IsPath
hnp : ¬p.Nil
hadj1 : p.toSubgraph.Adj u p.snd
v : V
⊢ v ∈ p.toSubgraph.neighborSet u ↔ v ∈ {p.snd}

Proof state:
case h.intro.intro.inl
V : Type u
G : SimpleGraph V
u v✝ : V
p : G.Walk u v✝
hp : p.IsPath
hnp : ¬p.Nil
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
i : ℕ
right✝ : i < p.length
hl : p.getVert i = u ∧ p.getVert (i + 1) = v
this : i = 0
⊢ v = p.snd

Tactic:
aesop

Result:
no goals

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

Tactic:
omega

Result:
no goals

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

Tactic:
rw [Set.mem_setOf]

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