-- 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:
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 = 0

Tactic:
apply hp.getVert_injOn (by rw [Set.mem_setOf]; omega) (by rw [Set.mem_setOf]; omega)

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
⊢ p.getVert i = p.getVert 0

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 ∈ {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
⊢ 0 ≤ p.length

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 ∈ {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
hr : p.getVert i = v ∧ p.getVert (i + 1) = u
⊢ i + 1 ≤ p.length

Proof state:
case h
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, (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length) → v = p.snd

Tactic:
rintro ⟨i, hl | hr⟩

Result:
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
⊢ v = p.snd

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

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
this : i + 1 = 0
⊢ v = p.snd

Tactic:
contradiction

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 ∈ {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
hr : p.getVert i = v ∧ p.getVert (i + 1) = u
⊢ 0 ≤ p.length

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
⊢ v = p.snd

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

Result:
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

Proof state:
case h
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, (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length) ↔ v = p.snd

Tactic:
refine ⟨?_, by aesop⟩

Result:
case h
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, (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length) → v = p.snd

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

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✝ : 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, (p.getVert i = u ∧ p.getVert (i + 1) = v ∨ p.getVert i = v ∧ p.getVert (i + 1) = u) ∧ i < p.length) ↔ 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
⊢ p.toSubgraph.neighborSet u = {p.snd}

Tactic:
have hadj1 := p.toSubgraph_adj_snd hnp

Result:
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}

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 = 0

Tactic:
apply hp.getVert_injOn (by rw [Set.mem_setOf]; omega) (by rw [Set.mem_setOf]; omega)

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

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
⊢ v = p.snd → ∃ 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