-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma ncard_neighborSet_toSubgraph_eq_two {u v} {p : G.Walk u u} (hpc : p.IsCycle)
    (h : v ∈ p.support) : (p.toSubgraph.neighborSet v).ncard = 2

Proof state:
case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2

Tactic:
exact Set.ncard_pair (hpc.getVert_sub_one_neq_getVert_add_one (by omega))

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ i < p.length

Tactic:
omega

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
rw [← hi.1, hpc.neighborSet_toSubgraph_internal he.1 (by omega)]

Result:
case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2

Proof state:
case intro
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
by_cases he : i = 0 ∨ i = p.length

Result:
case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2

case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : ¬(i = 0 ∨ i = p.length)
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Proof state:
case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
rw [← huv, hpc.neighborSet_toSubgraph_endpoint]

Result:
case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ {p.snd, p.penultimate}.ncard = 2

Proof state:
case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
have huv : u = v := by aesop

Result:
case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
⊢ u = v

Tactic:
aesop

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
h : v ∈ p.support
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
simp only [SimpleGraph.Walk.mem_support_iff_exists_getVert] at h ⊢

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
h : ∃ n, p.getVert n = v ∧ n ≤ p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Proof state:
case pos
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
huv : u = v
⊢ {p.snd, p.penultimate}.ncard = 2

Tactic:
exact Set.ncard_pair hpc.snd_ne_penultimate

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
h : ∃ n, p.getVert n = v ∧ n ≤ p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
obtain ⟨i, hi⟩ := h

Result:
case intro
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ i ≤ p.length

Tactic:
omega

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : ¬(i = 0 ∨ i = p.length)
⊢ (p.toSubgraph.neighborSet v).ncard = 2

Tactic:
push_neg at he

Result:
case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ (p.toSubgraph.neighborSet v).ncard = 2