case zero
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ u v : V
⊢ ↑(finsetWalkLength G Nat.zero u v) = {p | Walk.length p = Nat.zero}

case succ
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
⊢ ↑(finsetWalkLength G (Nat.succ n) u v) = {p | Walk.length p = Nat.succ n}
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
n : ℕ
u v : V
⊢ ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
induction' n with n ih generalizing u v
no goals
case zero
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ u v : V
⊢ ↑(finsetWalkLength G Nat.zero u v) = {p | Walk.length p = Nat.zero}
obtain rfl | huv := eq_or_ne u v <;> simp [finsetWalkLength, set_walk_length_zero_eq_of_ne, *]
case succ
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
⊢ (⋃ (x : ↑(neighborSet G u)),
      ↑(Finset.map
          { toFun := fun p => Walk.cons (_ : ↑x ∈ neighborSet G u) p,
            inj' :=
              (_ :
                ∀ (x_1 x_2 : Walk G (↑x) v),
                  Walk.cons (_ : ↑x ∈ neighborSet G u) x_1 = Walk.cons (_ : ↑x ∈ neighborSet G u) x_2 → x_1 = x_2) }
          (finsetWalkLength G n (↑x) v))) =
    ⋃ (w : V) (h : Adj G u w), Walk.cons h '' {p' | Walk.length p' = n}
case succ
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
⊢ ↑(finsetWalkLength G (Nat.succ n) u v) = {p | Walk.length p = Nat.succ n}
simp only [finsetWalkLength, set_walk_length_succ_eq, Finset.coe_biUnion, Finset.mem_coe,
  Finset.mem_univ, Set.iUnion_true]
case succ.h
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
⊢ (p ∈
      ⋃ (x : ↑(neighborSet G u)),
        ↑(Finset.map
            { toFun := fun p => Walk.cons (_ : ↑x ∈ neighborSet G u) p,
              inj' :=
                (_ :
                  ∀ (x_1 x_2 : Walk G (↑x) v),
                    Walk.cons (_ : ↑x ∈ neighborSet G u) x_1 = Walk.cons (_ : ↑x ∈ neighborSet G u) x_2 → x_1 = x_2) }
            (finsetWalkLength G n (↑x) v))) ↔
    p ∈ ⋃ (w : V) (h : Adj G u w), Walk.cons h '' {p' | Walk.length p' = n}
case succ
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
⊢ (⋃ (x : ↑(neighborSet G u)),
      ↑(Finset.map
          { toFun := fun p => Walk.cons (_ : ↑x ∈ neighborSet G u) p,
            inj' :=
              (_ :
                ∀ (x_1 x_2 : Walk G (↑x) v),
                  Walk.cons (_ : ↑x ∈ neighborSet G u) x_1 = Walk.cons (_ : ↑x ∈ neighborSet G u) x_2 → x_1 = x_2) }
          (finsetWalkLength G n (↑x) v))) =
    ⋃ (w : V) (h : Adj G u w), Walk.cons h '' {p' | Walk.length p' = n}
ext p
case succ.h
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
⊢ (∃ i h x,
      x ∈ finsetWalkLength G n i v ∧
        Walk.cons (_ : ↑{ val := i, property := (_ : i ∈ neighborSet G u) } ∈ neighborSet G u) x = p) ↔
    ∃ i h x, Walk.length x = n ∧ Walk.cons (_ : Adj G u i) x = p
case succ.h
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
⊢ (p ∈
      ⋃ (x : ↑(neighborSet G u)),
        ↑(Finset.map
            { toFun := fun p => Walk.cons (_ : ↑x ∈ neighborSet G u) p,
              inj' :=
                (_ :
                  ∀ (x_1 x_2 : Walk G (↑x) v),
                    Walk.cons (_ : ↑x ∈ neighborSet G u) x_1 = Walk.cons (_ : ↑x ∈ neighborSet G u) x_2 → x_1 = x_2) }
            (finsetWalkLength G n (↑x) v))) ↔
    p ∈ ⋃ (w : V) (h : Adj G u w), Walk.cons h '' {p' | Walk.length p' = n}
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]
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
x✝² : V
x✝¹ : Adj G u x✝²
x✝ : Walk G x✝² v
⊢ x✝ ∈ finsetWalkLength G n x✝² v ↔ Walk.length x✝ = n
case succ.h
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
⊢ (∃ i h x,
      x ∈ finsetWalkLength G n i v ∧
        Walk.cons (_ : ↑{ val := i, property := (_ : i ∈ neighborSet G u) } ∈ neighborSet G u) x = p) ↔
    ∃ i h x, Walk.length x = n ∧ Walk.cons (_ : Adj G u i) x = p
congr!
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
w : V
x✝ : Adj G u w
q : Walk G w v
⊢ q ∈ finsetWalkLength G n w v ↔ Walk.length q = n
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
x✝² : V
x✝¹ : Adj G u x✝²
x✝ : Walk G x✝² v
⊢ x✝ ∈ finsetWalkLength G n x✝² v ↔ Walk.length x✝ = n
rename_i w _ q
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
w : V
x✝ : Adj G u w
q : Walk G w v
this : q ∈ ↑(finsetWalkLength G n w v) ↔ q ∈ {p | Walk.length p = n}
⊢ q ∈ finsetWalkLength G n w v ↔ Walk.length q = n
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
w : V
x✝ : Adj G u w
q : Walk G w v
⊢ q ∈ finsetWalkLength G n w v ↔ Walk.length q = n
have := Set.ext_iff.mp (ih w v) q
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
w : V
x✝ : Adj G u w
q : Walk G w v
this : q ∈ finsetWalkLength G n w v ↔ Walk.length q = n
⊢ q ∈ finsetWalkLength G n w v ↔ Walk.length q = n
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
w : V
x✝ : Adj G u w
q : Walk G w v
this : q ∈ ↑(finsetWalkLength G n w v) ↔ q ∈ {p | Walk.length p = n}
⊢ q ∈ finsetWalkLength G n w v ↔ Walk.length q = n
simp only [Finset.mem_coe, Set.mem_setOf_eq] at this
no goals
case succ.h.a.h.e'_2.h.h.e'_2.h.h.e'_2.h.h.e'_1.a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
inst✝¹ : DecidableEq V
inst✝ : LocallyFinite G
u✝ v✝ : V
n : ℕ
ih : ∀ (u v : V), ↑(finsetWalkLength G n u v) = {p | Walk.length p = n}
u v : V
p : Walk G u v
w : V
x✝ : Adj G u w
q : Walk G w v
this : q ∈ finsetWalkLength G n w v ↔ Walk.length q = n
⊢ q ∈ finsetWalkLength G n w v ↔ Walk.length q = n
rw [← this]