-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
theorem set_walk_length_succ_eq (u v : V) (n : ℕ) :
    {p : G.Walk u v | p.length = n.succ} =
      ⋃ (w : V) (h : G.Adj u w), Walk.cons h '' {p' : G.Walk w v | p'.length = n}

Proof state:
case h.nil
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ Walk.nil ∈ {p | p.length = n.succ} ↔ Walk.nil ∈ ⋃ w, ⋃ (h : G.Adj u w), Walk.cons h '' {p' | p'.length = n}

Tactic:
simp [eq_comm]

Result:
no goals

Proof state:
case h.cons.mpr.intro.intro.intro.intro.refl
V : Type u
G : SimpleGraph V
u v v✝ : V
huw✝ : G.Adj u v✝
pwv : G.Walk v✝ v
huw : G.Adj u v✝
⊢ pwv.length = pwv.length

Tactic:
rfl

Result:
no goals

Proof state:
case h.cons.mp
V : Type u
G : SimpleGraph V
u v v✝ : V
huw : G.Adj u v✝
pwv : G.Walk v✝ v
⊢ ∃ i, ∃ (h : G.Adj u i), ∃ x, x.length = pwv.length ∧ Walk.cons ⋯ x = Walk.cons huw pwv

Tactic:
exact ⟨_, huw, pwv, rfl, rfl⟩

Result:
no goals

Proof state:
case h.cons.mpr
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
huw : G.Adj u v✝
pwv : G.Walk v✝ v
⊢ (∃ i, ∃ (h : G.Adj u i), ∃ x, x.length = n ∧ Walk.cons ⋯ x = Walk.cons huw pwv) → pwv.length = n

Tactic:
rintro ⟨w, huw, pwv, rfl, rfl, rfl⟩

Result:
case h.cons.mpr.intro.intro.intro.intro.refl
V : Type u
G : SimpleGraph V
u v v✝ : V
huw✝ : G.Adj u v✝
pwv : G.Walk v✝ v
huw : G.Adj u v✝
⊢ pwv.length = pwv.length

Proof state:
case h.cons
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
huw : G.Adj u v✝
pwv : G.Walk v✝ v
⊢ pwv.length = n ↔ ∃ i, ∃ (h : G.Adj u i), ∃ x, x.length = n ∧ Walk.cons ⋯ x = Walk.cons huw pwv

Tactic:
constructor

Result:
case h.cons.mp
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
huw : G.Adj u v✝
pwv : G.Walk v✝ v
⊢ pwv.length = n → ∃ i, ∃ (h : G.Adj u i), ∃ x, x.length = n ∧ Walk.cons ⋯ x = Walk.cons huw pwv

case h.cons.mpr
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
huw : G.Adj u v✝
pwv : G.Walk v✝ v
⊢ (∃ i, ∃ (h : G.Adj u i), ∃ x, x.length = n ∧ Walk.cons ⋯ x = Walk.cons huw pwv) → pwv.length = n

Proof state:
case h.cons
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
huw : G.Adj u v✝
pwv : G.Walk v✝ v
⊢ Walk.cons huw pwv ∈ {p | p.length = n.succ} ↔
    Walk.cons huw pwv ∈ ⋃ w, ⋃ (h : G.Adj u w), Walk.cons h '' {p' | p'.length = n}

Tactic:
simp only [Nat.succ_eq_add_one, Set.mem_setOf_eq, Walk.length_cons, add_left_inj,
  Set.mem_iUnion, Set.mem_image, exists_prop]

Result:
case h.cons
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
huw : G.Adj u v✝
pwv : G.Walk v✝ v
⊢ pwv.length = n ↔ ∃ i, ∃ (h : G.Adj u i), ∃ x, x.length = n ∧ Walk.cons ⋯ x = Walk.cons huw pwv

Proof state:
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
⊢ {p | p.length = n.succ} = ⋃ w, ⋃ (h : G.Adj u w), Walk.cons h '' {p' | p'.length = n}

Tactic:
ext p

Result:
case h
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ {p | p.length = n.succ} ↔ p ∈ ⋃ w, ⋃ (h : G.Adj u w), Walk.cons h '' {p' | p'.length = n}

Proof state:
case h.cons.mp
V : Type u
G : SimpleGraph V
u v : V
n : ℕ
v✝ : V
huw : G.Adj u v✝
pwv : G.Walk v✝ v
⊢ pwv.length = n → ∃ i, ∃ (h : G.Adj u i), ∃ x, x.length = n ∧ Walk.cons ⋯ x = Walk.cons huw pwv

Tactic:
rintro rfl

Result:
case h.cons.mp
V : Type u
G : SimpleGraph V
u v v✝ : V
huw : G.Adj u v✝
pwv : G.Walk v✝ v
⊢ ∃ i, ∃ (h : G.Adj u i), ∃ x, x.length = pwv.length ∧ Walk.cons ⋯ x = Walk.cons huw pwv