internlm/Lean-Github huggingface dataset:
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih :
  list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset →
    list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g
      (if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
    ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: 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 :
  list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset →
    list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih :
  list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset →
    list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
Tactic:
apply ih
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih :
  list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset →
    list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih :
  list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset →
    list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset
Tactic:
trans (x :: stack).toFinset.toSet ∪ 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 :
  list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset →
    list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset

Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih :
  list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset →
    list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ ↑(x :: stack).toFinset ∪ ↑visited.toFinset ⊆ ↑stack.toFinset ∪ ↑visited.toFinset
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih :
  list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset →
    list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
Tactic:
exact h1
Proof state after:
no goals
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∈ visited
ih :
  list_direct_succ_set g visited ⊆ ↑stack.toFinset ∪ ↑visited.toFinset →
    list_direct_succ_set g (dft_aux g stack visited) ⊆ ↑(dft_aux g stack visited).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ ↑(x :: stack).toFinset ∪ ↑visited.toFinset ⊆ ↑stack.toFinset ∪ ↑visited.toFinset
Tactic:
exact extracted_3 visited stack x c1
Proof state after:
no goals
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g (x :: stack) visited) ⊆ ↑(dft_aux 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 :
  list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g
      (if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
    ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g
      (if x ∈ visited then dft_aux g stack visited else dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
    ↑(if x ∈ visited then dft_aux g stack visited
        else dft_aux g (direct_succ_list g x ++ stack) (x :: 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 :
  list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
    ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
    ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
Tactic:
apply ih
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset
Tactic:
simp only [list_direct_succ_set_cons]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ ↑(direct_succ_list g x).toFinset ∪ list_direct_succ_set g visited ⊆
    ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset
Theorem: list_direct_succ_set_closed_dft_aux_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
visited : List Node
x : Node
stack : List Node
c1 : x ∉ visited
ih :
  list_direct_succ_set g (x :: visited) ⊆ ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset →
    list_direct_succ_set g (dft_aux g (direct_succ_list g x ++ stack) (x :: visited)) ⊆
      ↑(dft_aux g (direct_succ_list g x ++ stack) (x :: visited)).toFinset
h1 : list_direct_succ_set g visited ⊆ ↑(x :: stack).toFinset ∪ ↑visited.toFinset
⊢ ↑(direct_succ_list g x).toFinset ∪ list_direct_succ_set g visited ⊆
    ↑(direct_succ_list g x ++ stack).toFinset ∪ ↑(x :: visited).toFinset
Tactic:
exact extracted_4 (direct_succ_list g x) visited stack (list_direct_succ_set g visited) x h1
Proof state after:
no goals
Theorem: list_direct_succ_set_closed_dft_aux
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ list_direct_succ_set g (dft_aux g stack []) ⊆ ↑(dft_aux g stack []).toFinset
Tactic:
apply list_direct_succ_set_closed_dft_aux_aux
Proof state after:
case h1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ list_direct_succ_set g [] ⊆ ↑stack.toFinset ∪ ↑[].toFinset
Theorem: list_direct_succ_set_closed_dft_aux
Proof state before:
case h1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ list_direct_succ_set g [] ⊆ ↑stack.toFinset ∪ ↑[].toFinset
Tactic:
simp only [list_direct_succ_set]
Proof state after:
case h1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ {y | ∃ x ∈ [], ∃ ys, y ∈ ys ∧ (x, ys) ∈ g} ⊆ ↑stack.toFinset ∪ ↑[].toFinset
Theorem: list_direct_succ_set_closed_dft_aux
Proof state before:
case h1
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
stack : List Node
⊢ {y | ∃ x ∈ [], ∃ ys, y ∈ ys ∧ (x, ys) ∈ g} ⊆ ↑stack.toFinset ∪ ↑[].toFinset
Tactic:
simp
Proof state after:
no goals
Theorem: base_of_reachable_from_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ↑xs.toFinset ⊆ reachable_from_list g xs
Tactic:
simp only [Set.subset_def]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ∀ x ∈ ↑xs.toFinset, x ∈ reachable_from_list g xs
Theorem: base_of_reachable_from_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
⊢ ∀ x ∈ ↑xs.toFinset, x ∈ reachable_from_list g xs
Tactic:
intro x a1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
x : Node
a1 : x ∈ ↑xs.toFinset
⊢ x ∈ reachable_from_list g xs
Theorem: base_of_reachable_from_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
x : Node
a1 : x ∈ ↑xs.toFinset
⊢ x ∈ reachable_from_list g xs
Tactic:
simp at a1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
x : Node
a1 : x ∈ xs
⊢ x ∈ reachable_from_list g xs
Theorem: base_of_reachable_from_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs : List Node
x : Node
a1 : x ∈ xs
⊢ x ∈ reachable_from_list g xs
Tactic:
exact reachable_from_list.base x a1
Proof state after:
no goals
Theorem: reachable_from_list_mono
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
⊢ reachable_from_list g xs ⊆ reachable_from_list g ys
Tactic:
simp only [Set.subset_def]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
⊢ ∀ x ∈ reachable_from_list g xs, x ∈ reachable_from_list g ys
Theorem: reachable_from_list_mono
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
⊢ ∀ x ∈ reachable_from_list g xs, x ∈ reachable_from_list g ys
Tactic:
intro x a1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x : Node
a1 : x ∈ reachable_from_list g xs
⊢ x ∈ reachable_from_list g ys
Theorem: reachable_from_list_mono
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x : Node
a1 : x ∈ reachable_from_list g xs
⊢ x ∈ reachable_from_list g ys
Tactic:
induction a1
Proof state after:
case base
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x x✝ : Node
a✝ : x✝ ∈ xs
⊢ x✝ ∈ reachable_from_list g ys

case step
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x x✝ : Node
e✝ : Node × List Node
a✝² : e✝ ∈ g
a✝¹ : x✝ ∈ e✝.2
a✝ : reachable_from_list g xs e✝.1
a_ih✝ : e✝.1 ∈ reachable_from_list g ys
⊢ x✝ ∈ reachable_from_list g ys
Theorem: reachable_from_list_mono
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x a : Node
ih : a ∈ xs
⊢ a ∈ reachable_from_list g ys
Tactic:
case base a ih =>
  apply reachable_from_list.base
  apply Set.mem_of_subset_of_mem h1 ih
Proof state after:
no goals
Theorem: reachable_from_list_mono
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x✝ x : Node
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
a✝ : reachable_from_list g xs e.1
ih_4 : e.1 ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g ys
Tactic:
case step x e ih_1 ih_2 _ ih_4 =>
  exact reachable_from_list.step x e ih_1 ih_2 ih_4
Proof state after:
no goals
Theorem: reachable_from_list_mono
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x a : Node
ih : a ∈ xs
⊢ a ∈ reachable_from_list g ys
Tactic:
apply reachable_from_list.base
Proof state after:
case a
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x a : Node
ih : a ∈ xs
⊢ a ∈ ys
Theorem: reachable_from_list_mono
Proof state before:
case a
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x a : Node
ih : a ∈ xs
⊢ a ∈ ys
Tactic:
apply Set.mem_of_subset_of_mem h1 ih
Proof state after:
no goals
Theorem: reachable_from_list_mono
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
h1 : xs ⊆ ys
x✝ x : Node
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
a✝ : reachable_from_list g xs e.1
ih_4 : e.1 ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g ys
Tactic:
exact reachable_from_list.step x e ih_1 ih_2 ih_4
Proof state after:
no goals
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ reachable_from_list g (xs ++ ys) ⊆ reachable_from_list g xs ∪ reachable_from_list g ys
Tactic:
simp only [Set.subset_def]
Proof state after:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ ∀ x ∈ reachable_from_list g (xs ++ ys), x ∈ reachable_from_list g xs ∪ reachable_from_list g ys
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ ∀ x ∈ reachable_from_list g (xs ++ ys), x ∈ reachable_from_list g xs ∪ reachable_from_list g ys
Tactic:
intro x a1
Proof state after:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
a1 : x ∈ reachable_from_list g (xs ++ ys)
⊢ x ∈ reachable_from_list g xs ∪ reachable_from_list g ys
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
a1 : x ∈ reachable_from_list g (xs ++ ys)
⊢ x ∈ reachable_from_list g xs ∪ reachable_from_list g ys
Tactic:
simp
Proof state after:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
a1 : x ∈ reachable_from_list g (xs ++ ys)
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
a1 : x ∈ reachable_from_list g (xs ++ ys)
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
induction a1
Proof state after:
case base
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x x✝ : Node
a✝ : x✝ ∈ xs ++ ys
⊢ x✝ ∈ reachable_from_list g xs ∨ x✝ ∈ reachable_from_list g ys

case step
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x x✝ : Node
e✝ : Node × List Node
a✝² : e✝ ∈ g
a✝¹ : x✝ ∈ e✝.2
a✝ : reachable_from_list g (xs ++ ys) e✝.1
a_ih✝ : e✝.1 ∈ reachable_from_list g xs ∨ e✝.1 ∈ reachable_from_list g ys
⊢ x✝ ∈ reachable_from_list g xs ∨ x✝ ∈ reachable_from_list g ys
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
ih : x ∈ xs ++ ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
case _ x ih =>
  simp at ih
  cases ih
  case inl c1 =>
    left
    exact reachable_from_list.base x c1
  case inr c1 =>
    right
    exact reachable_from_list.base x c1
Proof state after:
no goals
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
ih_3 : reachable_from_list g (xs ++ ys) e.1
ih_4 : e.1 ∈ reachable_from_list g xs ∨ e.1 ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
case _ x e ih_1 ih_2 ih_3 ih_4 =>
  cases ih_4
  case _ left =>
    left
    exact reachable_from_list.step x e ih_1 ih_2 left
  case _ right =>
    right
    exact reachable_from_list.step x e ih_1 ih_2 right
Proof state after:
no goals
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
ih : x ∈ xs ++ ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
simp at ih
Proof state after:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
ih : x ∈ xs ∨ x ∈ ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
ih : x ∈ xs ∨ x ∈ ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
cases ih
Proof state after:
case inl
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
h✝ : x ∈ xs
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys

case inr
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
h✝ : x ∈ ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
c1 : x ∈ xs
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
case inl c1 =>
  left
  exact reachable_from_list.base x c1
Proof state after:
no goals
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
c1 : x ∈ ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
case inr c1 =>
  right
  exact reachable_from_list.base x c1
Proof state after:
no goals
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
c1 : x ∈ xs
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
left
Proof state after:
case h
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
c1 : x ∈ xs
⊢ x ∈ reachable_from_list g xs
Theorem: reachable_from_list_of_append_left
Proof state before:
case h
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
c1 : x ∈ xs
⊢ x ∈ reachable_from_list g xs
Tactic:
exact reachable_from_list.base x c1
Proof state after:
no goals
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
c1 : x ∈ ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
right
Proof state after:
case h
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
c1 : x ∈ ys
⊢ x ∈ reachable_from_list g ys
Theorem: reachable_from_list_of_append_left
Proof state before:
case h
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
c1 : x ∈ ys
⊢ x ∈ reachable_from_list g ys
Tactic:
exact reachable_from_list.base x c1
Proof state after:
no goals
Theorem: reachable_from_list_of_append_left
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
ih_3 : reachable_from_list g (xs ++ ys) e.1
ih_4 : e.1 ∈ reachable_from_list g xs ∨ e.1 ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
cases ih_4
Proof state after:
case inl
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
ih_3 : reachable_from_list g (xs ++ ys) e.1
h✝ : e.1 ∈ reachable_from_list g xs
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys

case inr
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x✝ x : Node
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
ih_3 : reachable_from_list g (xs ++ ys) e.1
h✝ : e.1 ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys