-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
theorem coe_finsetWalkLength_eq (n : ℕ) (u v : V) :
    (G.finsetWalkLength n u v : Set (G.Walk u v)) = {p : G.Walk u v | p.length = n}

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
u v : V
⊢ ↑(G.finsetWalkLength n u v) = {p | p.length = n}

Tactic:
induction n generalizing u v with
| zero =>
  obtain rfl | huv := eq_or_ne u v <;> simp [finsetWalkLength, set_walk_length_zero_eq_of_ne, *]
| succ n ih =>
  simp only [finsetWalkLength, set_walk_length_succ_eq, Finset.coe_biUnion, Finset.mem_coe,
    Finset.mem_univ, Set.iUnion_true]
  ext p
  simp only [mem_neighborSet, Finset.coe_map, Embedding.coeFn_mk, Set.iUnion_coe_set,
    Set.mem_iUnion, Set.mem_image, Finset.mem_coe, Set.mem_setOf_eq]
  congr!
  rename_i w _ q
  have := Set.ext_iff.mp (ih w v) q
  simp only [Finset.mem_coe, Set.mem_setOf_eq] at this
  rw [← this]

Result:
no goals

Proof state:
case succ
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
⊢ ↑(G.finsetWalkLength (n + 1) u v) = {p | p.length = n + 1}

Tactic:
simp only [finsetWalkLength, set_walk_length_succ_eq, Finset.coe_biUnion, Finset.mem_coe,
  Finset.mem_univ, Set.iUnion_true]

Result:
case succ
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
⊢ ⋃ x, ↑(map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑x) v)) =
    ⋃ w, ⋃ (h : G.Adj u w), Walk.cons h '' {p' | p'.length = n}

Proof state:
case zero
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
⊢ ↑(G.finsetWalkLength 0 u v) = {p | p.length = 0}

Tactic:
obtain rfl | huv := eq_or_ne u v <;> simp [finsetWalkLength, set_walk_length_zero_eq_of_ne, *]

Result:
no goals

Proof state:
case succ
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
⊢ ⋃ x, ↑(map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑x) v)) =
    ⋃ w, ⋃ (h : G.Adj u w), Walk.cons h '' {p' | p'.length = n}

Tactic:
ext p

Result:
case succ.h
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
⊢ p ∈ ⋃ x, ↑(map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑x) v)) ↔
    p ∈ ⋃ w, ⋃ (h : G.Adj u w), Walk.cons h '' {p' | p'.length = n}

Proof state:
case succ.h
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
⊢ (∃ i, ∃ (h : G.Adj u i), ∃ x ∈ G.finsetWalkLength n i v, Walk.cons ⋯ x = p) ↔
    ∃ i, ∃ (h : G.Adj u i), ∃ x, x.length = n ∧ Walk.cons ⋯ x = p

Tactic:
congr!

Result:
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
x✝² : V
x✝¹ : G.Adj u x✝²
x✝ : G.Walk x✝² v
⊢ x✝ ∈ G.finsetWalkLength n x✝² v ↔ x✝.length = n

Proof state:
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
w : V
x✝ : G.Adj u w
q : G.Walk w v
this : q ∈ G.finsetWalkLength n w v ↔ q.length = n
⊢ q ∈ G.finsetWalkLength n w v ↔ q.length = n

Tactic:
rw [← this]

Result:
no goals

Proof state:
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
w : V
x✝ : G.Adj u w
q : G.Walk w v
this : q ∈ ↑(G.finsetWalkLength n w v) ↔ q ∈ {p | p.length = n}
⊢ q ∈ G.finsetWalkLength n w v ↔ q.length = n

Tactic:
simp only [Finset.mem_coe, Set.mem_setOf_eq] at this

Result:
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
w : V
x✝ : G.Adj u w
q : G.Walk w v
this : q ∈ G.finsetWalkLength n w v ↔ q.length = n
⊢ q ∈ G.finsetWalkLength n w v ↔ q.length = n

Proof state:
case succ.h
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
⊢ p ∈ ⋃ x, ↑(map { toFun := fun p => Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑x) v)) ↔
    p ∈ ⋃ w, ⋃ (h : G.Adj u w), Walk.cons h '' {p' | p'.length = n}

Tactic:
simp only [mem_neighborSet, Finset.coe_map, Embedding.coeFn_mk, Set.iUnion_coe_set,
  Set.mem_iUnion, Set.mem_image, Finset.mem_coe, Set.mem_setOf_eq]

Result:
case succ.h
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
⊢ (∃ i, ∃ (h : G.Adj u i), ∃ x ∈ G.finsetWalkLength n i v, Walk.cons ⋯ x = p) ↔
    ∃ i, ∃ (h : G.Adj u i), ∃ x, x.length = n ∧ Walk.cons ⋯ x = p

Proof state:
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
x✝² : V
x✝¹ : G.Adj u x✝²
x✝ : G.Walk x✝² v
⊢ x✝ ∈ G.finsetWalkLength n x✝² v ↔ x✝.length = n

Tactic:
rename_i w _ q

Result:
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
w : V
x✝ : G.Adj u w
q : G.Walk w v
⊢ q ∈ G.finsetWalkLength n w v ↔ q.length = n

Proof state:
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
w : V
x✝ : G.Adj u w
q : G.Walk w v
⊢ q ∈ G.finsetWalkLength n w v ↔ q.length = n

Tactic:
have := Set.ext_iff.mp (ih w v) q

Result:
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
ih : ∀ (u v : V), ↑(G.finsetWalkLength n u v) = {p | p.length = n}
u v : V
p : G.Walk u v
w : V
x✝ : G.Adj u w
q : G.Walk w v
this : q ∈ ↑(G.finsetWalkLength n w v) ↔ q ∈ {p | p.length = n}
⊢ q ∈ G.finsetWalkLength n w v ↔ q.length = n