-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma ncard_neighborSet_toSubgraph_internal_eq_two {u} {i : ℕ} {p : G.Walk u v} (hp : p.IsPath)
    (h : i ≠ 0) (h' : i < p.length) :
    (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2

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
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ 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
⊢ (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2

Tactic:
rw [hp.neighborSet_toSubgraph_internal h h']

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
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2

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
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ 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
this : p.getVert (i - 1) ≠ p.getVert (i + 1)
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2

Tactic:
simp_all

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
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2

Tactic:
have : p.getVert (i - 1) ≠ p.getVert (i + 1) := by
  intro h
  have := hp.getVert_injOn (by rw [Set.mem_setOf_eq]; omega) (by rw [Set.mem_setOf_eq]; omega) h
  omega

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
this : p.getVert (i - 1) ≠ p.getVert (i + 1)
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2

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
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ 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
h✝ : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ 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
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ 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
h✝ : i ≠ 0
h' : i < p.length
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ 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
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ False

Tactic:
have := hp.getVert_injOn (by rw [Set.mem_setOf_eq]; omega) (by rw [Set.mem_setOf_eq]; omega) h

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
h : p.getVert (i - 1) = p.getVert (i + 1)
this : i - 1 = i + 1
⊢ False

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
h : p.getVert (i - 1) = p.getVert (i + 1)
this : i - 1 = i + 1
⊢ False

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
⊢ p.getVert (i - 1) ≠ p.getVert (i + 1)

Tactic:
intro h

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
h : p.getVert (i - 1) = p.getVert (i + 1)
⊢ False