no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w : V
p : Walk G u v
⊢ Set.Finite (Subgraph.neighborSet (Walk.toSubgraph p) w)
induction p with
| nil =>
  rw [Walk.toSubgraph, neighborSet_singletonSubgraph]
  apply Set.toFinite
| cons ha _ ih =>
  rw [Walk.toSubgraph, Subgraph.neighborSet_sup]
  refine Set.Finite.union ?_ ih
  refine Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)
  apply Set.toFinite
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ : V
⊢ Set.Finite ∅
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ : V
⊢ Set.Finite (Subgraph.neighborSet (Walk.toSubgraph nil) w)
rw [Walk.toSubgraph, neighborSet_singletonSubgraph]
no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ : V
⊢ Set.Finite ∅
apply Set.toFinite
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
ha : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : Set.Finite (Subgraph.neighborSet (Walk.toSubgraph p✝) w)
⊢ Set.Finite (Subgraph.neighborSet (subgraphOfAdj G ha) w ∪ Subgraph.neighborSet (Walk.toSubgraph p✝) w)
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
ha : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : Set.Finite (Subgraph.neighborSet (Walk.toSubgraph p✝) w)
⊢ Set.Finite (Subgraph.neighborSet (Walk.toSubgraph (cons ha p✝)) w)
rw [Walk.toSubgraph, Subgraph.neighborSet_sup]
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
ha : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : Set.Finite (Subgraph.neighborSet (Walk.toSubgraph p✝) w)
⊢ Set.Finite (Subgraph.neighborSet (subgraphOfAdj G ha) w)
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
ha : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : Set.Finite (Subgraph.neighborSet (Walk.toSubgraph p✝) w)
⊢ Set.Finite (Subgraph.neighborSet (subgraphOfAdj G ha) w ∪ Subgraph.neighborSet (Walk.toSubgraph p✝) w)
refine Set.Finite.union ?_ ih
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
ha : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : Set.Finite (Subgraph.neighborSet (Walk.toSubgraph p✝) w)
⊢ Set.Finite {u✝, v✝}
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
ha : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : Set.Finite (Subgraph.neighborSet (Walk.toSubgraph p✝) w)
⊢ Set.Finite (Subgraph.neighborSet (subgraphOfAdj G ha) w)
refine Set.Finite.subset ?_ (neighborSet_subgraphOfAdj_subset ha)
no goals
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
ha : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih : Set.Finite (Subgraph.neighborSet (Walk.toSubgraph p✝) w)
⊢ Set.Finite {u✝, v✝}
apply Set.toFinite