internlm/Lean-Github huggingface dataset:
Theorem: reachable_from_list_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
a1 : x ∈ reachable_from_list g (direct_succ_list g hd) ∪ reachable_from_list g (list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl
Tactic:
simp at a1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
a1 : x ∈ reachable_from_list g (direct_succ_list g hd) ∨ x ∈ reachable_from_list g (list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl
Theorem: reachable_from_list_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
a1 : x ∈ reachable_from_list g (direct_succ_list g hd) ∨ x ∈ reachable_from_list g (list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl
Tactic:
cases a1
Proof state after:
case inl
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
h✝ : x ∈ reachable_from_list g (direct_succ_list g hd)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl

case inr
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
h✝ : x ∈ reachable_from_list g (list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl
Theorem: reachable_from_list_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
left : x ∈ reachable_from_list g (direct_succ_list g hd)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl
Tactic:
case _ left =>
  left
  obtain s1 := reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list g hd
  exact Set.mem_of_subset_of_mem s1 left
Proof state after:
no goals
Theorem: reachable_from_list_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
right : x ∈ reachable_from_list g (list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl
Tactic:
case _ right =>
  right
  exact ih right
Proof state after:
no goals
Theorem: reachable_from_list_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
left : x ∈ reachable_from_list g (direct_succ_list g hd)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl
Tactic:
left
Proof state after:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
left : x ∈ reachable_from_list g (direct_succ_list g hd)
⊢ x ∈ reachable_from_list g [hd]
Theorem: reachable_from_list_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
left : x ∈ reachable_from_list g (direct_succ_list g hd)
⊢ x ∈ reachable_from_list g [hd]
Tactic:
obtain s1 := reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list g hd
Proof state after:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
left : x ∈ reachable_from_list g (direct_succ_list g hd)
s1 : reachable_from_list g (direct_succ_list g hd) ⊆ reachable_from_list g [hd]
⊢ x ∈ reachable_from_list g [hd]
Theorem: reachable_from_list_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
left : x ∈ reachable_from_list g (direct_succ_list g hd)
s1 : reachable_from_list g (direct_succ_list g hd) ⊆ reachable_from_list g [hd]
⊢ x ∈ reachable_from_list g [hd]
Tactic:
exact Set.mem_of_subset_of_mem s1 left
Proof state after:
no goals
Theorem: reachable_from_list_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
right : x ∈ reachable_from_list g (list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl
Tactic:
right
Proof state after:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
right : x ∈ reachable_from_list g (list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g tl
Theorem: reachable_from_list_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x hd : Node
tl : List Node
ih : x ∈ reachable_from_list g (list_direct_succ_list g tl) → x ∈ reachable_from_list g tl
right : x ∈ reachable_from_list g (list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g tl
Tactic:
exact ih right
Proof state after:
no goals
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack visited : List Node
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
induction stack, visited using dft_aux.induct g
Proof state after:
case case1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
⊢ ↑(dft_aux g [] visited✝).toFinset ⊆ reachable_from_list g [] ∪ ↑visited✝.toFinset

case case2
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∈ visited✝
ih1✝ : ↑(dft_aux g xs✝ visited✝).toFinset ⊆ reachable_from_list g xs✝ ∪ ↑visited✝.toFinset
⊢ ↑(dft_aux g (x✝ :: xs✝) visited✝).toFinset ⊆ reachable_from_list g (x✝ :: xs✝) ∪ ↑visited✝.toFinset

case case3
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited✝ : List Node
x✝ : Node
xs✝ : List Node
h✝ : x✝ ∉ visited✝
ih1✝ :
  ↑(dft_aux g (direct_succ_list g x✝ ++ xs✝) (x✝ :: visited✝)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x✝ ++ xs✝) ∪ ↑(x✝ :: visited✝).toFinset
⊢ ↑(dft_aux g (x✝ :: xs✝) visited✝).toFinset ⊆ reachable_from_list g (x✝ :: xs✝) ∪ ↑visited✝.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ ↑(dft_aux g [] visited).toFinset ⊆ reachable_from_list g [] ∪ ↑visited.toFinset
Tactic:
case _ visited =>
  simp only [dft_aux]
  simp
Proof state after:
no goals
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g (x :: stack) visited).toFinset ⊆ reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
case _ visited x stack c1 ih =>
  simp only [reachable_from_list_of_cons g x stack]
  simp only [dft_aux]
  simp only [if_pos c1]
  simp only [Set.union_assoc ]
  exact Set.subset_union_of_subset_right ih (reachable_from_list g [x])
Proof state after:
no goals
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ ↑(dft_aux g [] visited).toFinset ⊆ reachable_from_list g [] ∪ ↑visited.toFinset
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ ↑visited.toFinset ⊆ reachable_from_list g [] ∪ ↑visited.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
⊢ ↑visited.toFinset ⊆ reachable_from_list g [] ∪ ↑visited.toFinset
Tactic:
simp
Proof state after:
no goals
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g (x :: stack) visited).toFinset ⊆ reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
simp only [reachable_from_list_of_cons g x stack]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g (x :: stack) visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g (x :: stack) visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
simp only [if_pos c1]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
simp only [Set.union_assoc ]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g [x] ∪ (reachable_from_list g stack ∪ ↑visited.toFinset)
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih : ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g stack ∪ ↑visited.toFinset
⊢ ↑(dft_aux g stack visited).toFinset ⊆ reachable_from_list g [x] ∪ (reachable_from_list g stack ∪ ↑visited.toFinset)
Tactic:
exact Set.subset_union_of_subset_right ih (reachable_from_list g [x])
Proof state after:
no goals
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x ++ stack) ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (x :: stack) visited).toFinset ⊆ reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
simp only [dft_aux]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x ++ stack) ∪ ↑(x :: visited).toFinset
⊢ ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x ++ stack) ∪ ↑(x :: visited).toFinset
⊢ ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
simp only [if_neg c1]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x ++ stack) ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x ++ stack) ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
simp only [reachable_from_list_of_append g (direct_succ_list g x) stack] at ih
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (x :: stack) ∪ ↑visited.toFinset
Tactic:
simp only [reachable_from_list_of_cons g x stack]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
trans (reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ (x :: visited).toFinset.toSet)
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset

Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
Tactic:
exact ih
Proof state after:
no goals
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
⊢ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
have s1 : reachable_from_list g (direct_succ_list g x) ⊆ reachable_from_list g [x] := reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list g x
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
s1 : reachable_from_list g (direct_succ_list g x) ⊆ reachable_from_list g [x]
⊢ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset ⊆
    reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
s1 : reachable_from_list g (direct_succ_list g x) ⊆ reachable_from_list g [x]
⊢ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset ⊆
    reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
simp only [Set.subset_def] at *
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ∀ x_1 ∈ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset,
    x_1 ∈ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
s1 : ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
⊢ ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset,
    x_1 ∈ reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  ∀ x_1 ∈ ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset,
    x_1 ∈ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset
s1 : ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
⊢ ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x) ∪ reachable_from_list g stack ∪ ↑(x :: visited).toFinset,
    x_1 ∈ reachable_from_list g [x] ∪ reachable_from_list g stack ∪ ↑visited.toFinset
Tactic:
simp at *
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
s1 : ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
ih :
  ∀ x_1 ∈ dft_aux g (direct_succ_list g x ++ stack) (x :: visited),
    x_1 = x ∨ (x_1 ∈ reachable_from_list g (direct_succ_list g x) ∨ x_1 ∈ reachable_from_list g stack) ∨ x_1 ∈ visited
⊢ ((x ∈ reachable_from_list g [x] ∨ x ∈ reachable_from_list g stack) ∨ x ∈ visited) ∧
    ∀ (a : Node),
      (a ∈ reachable_from_list g (direct_succ_list g x) ∨ a ∈ reachable_from_list g stack) ∨ a ∈ visited →
        (a ∈ reachable_from_list g [x] ∨ a ∈ reachable_from_list g stack) ∨ a ∈ visited
Theorem: dft_aux_is_subset_of_reachable_from_list_and_visited
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
s1 : ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
ih :
  ∀ x_1 ∈ dft_aux g (direct_succ_list g x ++ stack) (x :: visited),
    x_1 = x ∨ (x_1 ∈ reachable_from_list g (direct_succ_list g x) ∨ x_1 ∈ reachable_from_list g stack) ∨ x_1 ∈ visited
⊢ ((x ∈ reachable_from_list g [x] ∨ x ∈ reachable_from_list g stack) ∨ x ∈ visited) ∧
    ∀ (a : Node),
      (a ∈ reachable_from_list g (direct_succ_list g x) ∨ a ∈ reachable_from_list g stack) ∨ a ∈ visited →
        (a ∈ reachable_from_list g [x] ∨ a ∈ reachable_from_list g stack) ∨ a ∈ visited
Tactic:
tauto
Proof state after:
no goals
Theorem: extracted_5
Proof state before:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : list_direct_succ_set g xs ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset
Tactic:
simp only [list_direct_succ_set] at h1
Proof state after:
α : Type
inst : DecidableEq α
g : Graph α
xs : List α
h1 : {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g} ⊆ ↑xs.toFinset
⊢ reachable_from_list g xs ⊆ ↑xs.toFinset