internlm/Lean-Github huggingface dataset:
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
left : e.1 ∈ reachable_from_list g xs
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
case _ left =>
  left
  exact reachable_from_list.step x e ih_1 ih_2 left
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
right : e.1 ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
Tactic:
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
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
ih_3 : reachable_from_list g (xs ++ ys) e.1
left : e.1 ∈ reachable_from_list g 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
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
ih_3 : reachable_from_list g (xs ++ ys) e.1
left : e.1 ∈ reachable_from_list g 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
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
ih_3 : reachable_from_list g (xs ++ ys) e.1
left : e.1 ∈ reachable_from_list g xs
⊢ x ∈ reachable_from_list g xs
Tactic:
exact reachable_from_list.step x e ih_1 ih_2 left
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
right : e.1 ∈ reachable_from_list g 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
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
ih_3 : reachable_from_list g (xs ++ ys) e.1
right : e.1 ∈ reachable_from_list g 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
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
ih_3 : reachable_from_list g (xs ++ ys) e.1
right : 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 right
Proof state after:
no goals
Theorem: reachable_from_list_of_append_right
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ reachable_from_list g xs ∪ reachable_from_list g ys ⊆ reachable_from_list g (xs ++ 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 ∪ reachable_from_list g ys, x ∈ reachable_from_list g (xs ++ ys)
Theorem: reachable_from_list_of_append_right
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ ∀ x ∈ reachable_from_list g xs ∪ reachable_from_list g ys, x ∈ reachable_from_list g (xs ++ 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 ∪ reachable_from_list g ys
⊢ x ∈ reachable_from_list g (xs ++ ys)
Theorem: reachable_from_list_of_append_right
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
a1 : x ∈ reachable_from_list g xs ∪ reachable_from_list g ys
⊢ x ∈ reachable_from_list g (xs ++ ys)
Tactic:
simp at 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 ∨ x ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g (xs ++ ys)
Theorem: reachable_from_list_of_append_right
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
a1 : x ∈ reachable_from_list g xs ∨ x ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g (xs ++ ys)
Tactic:
cases a1
Proof state after:
case inl
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
h✝ : x ∈ reachable_from_list g xs
⊢ x ∈ reachable_from_list g (xs ++ ys)

case inr
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
h✝ : x ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g (xs ++ ys)
Theorem: reachable_from_list_of_append_right
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
left : x ∈ reachable_from_list g xs
⊢ x ∈ reachable_from_list g (xs ++ ys)
Tactic:
apply reachable_from_list_mono g xs (xs ++ ys)
Proof state after:
case h1
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
left : x ∈ reachable_from_list g xs
⊢ xs ⊆ xs ++ ys

case a
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
left : x ∈ reachable_from_list g xs
⊢ x ∈ reachable_from_list g xs
Theorem: reachable_from_list_of_append_right
Proof state before:
case h1
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
left : x ∈ reachable_from_list g xs
⊢ xs ⊆ xs ++ ys
Tactic:
simp
Proof state after:
no goals
Theorem: reachable_from_list_of_append_right
Proof state before:
case a
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
left : x ∈ reachable_from_list g xs
⊢ x ∈ reachable_from_list g xs
Tactic:
exact left
Proof state after:
no goals
Theorem: reachable_from_list_of_append_right
Proof state before:
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
right : x ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g (xs ++ ys)
Tactic:
apply reachable_from_list_mono g ys (xs ++ ys)
Proof state after:
case h1
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
right : x ∈ reachable_from_list g ys
⊢ ys ⊆ xs ++ ys

case a
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
right : x ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g ys
Theorem: reachable_from_list_of_append_right
Proof state before:
case h1
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
right : x ∈ reachable_from_list g ys
⊢ ys ⊆ xs ++ ys
Tactic:
simp
Proof state after:
no goals
Theorem: reachable_from_list_of_append_right
Proof state before:
case a
Node : Type
inst : DecidableEq Node
g : Graph Node
xs ys : List Node
x : Node
right : x ∈ reachable_from_list g ys
⊢ x ∈ reachable_from_list g ys
Tactic:
exact right
Proof state after:
no goals
Theorem: reachable_from_list_of_append
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:
apply Set.eq_of_subset_of_subset
Proof state after:
case a
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

case a
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ reachable_from_list g xs ∪ reachable_from_list g ys ⊆ reachable_from_list g (xs ++ ys)
Theorem: reachable_from_list_of_append
Proof state before:
case a
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:
apply reachable_from_list_of_append_left
Proof state after:
no goals
Theorem: reachable_from_list_of_append
Proof state before:
case a
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
xs ys : List Node
⊢ reachable_from_list g xs ∪ reachable_from_list g ys ⊆ reachable_from_list g (xs ++ ys)
Tactic:
apply reachable_from_list_of_append_right
Proof state after:
no goals
Theorem: reachable_from_list_of_cons
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
ys : List Node
⊢ reachable_from_list g (x :: ys) = reachable_from_list g [x] ∪ reachable_from_list g ys
Tactic:
simp only [← reachable_from_list_of_append]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
ys : List Node
⊢ reachable_from_list g (x :: ys) = reachable_from_list g ([x] ++ ys)
Theorem: reachable_from_list_of_cons
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
ys : List Node
⊢ reachable_from_list g (x :: ys) = reachable_from_list g ([x] ++ ys)
Tactic:
simp
Proof state after:
no goals
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
⊢ reachable_from_list g (direct_succ_list g x) ⊆ reachable_from_list g [x]
Tactic:
simp only [Set.subset_def]
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
⊢ ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
⊢ ∀ x_1 ∈ reachable_from_list g (direct_succ_list g x), x_1 ∈ reachable_from_list g [x]
Tactic:
intro a a1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
a1 : a ∈ reachable_from_list g (direct_succ_list g x)
⊢ a ∈ reachable_from_list g [x]
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
a1 : a ∈ reachable_from_list g (direct_succ_list g x)
⊢ a ∈ reachable_from_list g [x]
Tactic:
induction a1
Proof state after:
case base
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a x✝ : Node
a✝ : x✝ ∈ direct_succ_list g x
⊢ x✝ ∈ reachable_from_list g [x]

case step
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a x✝ : Node
e✝ : Node × List Node
a✝² : e✝ ∈ g
a✝¹ : x✝ ∈ e✝.2
a✝ : reachable_from_list g (direct_succ_list g x) e✝.1
a_ih✝ : e✝.1 ∈ reachable_from_list g [x]
⊢ x✝ ∈ reachable_from_list g [x]
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
ih : y ∈ direct_succ_list g x
⊢ y ∈ reachable_from_list g [x]
Tactic:
case _ x y ih =>
  obtain s1 := mem_direct_succ_list_iff g x y
  simp only [s1] at ih
  apply Exists.elim ih
  intro ys a2
  cases a2
  case _ a2_left a2_right =>
    apply reachable_from_list.step y (x, ys) a2_right a2_left
    apply reachable_from_list.base x
    simp
Proof state after:
no goals
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x✝ a x : Node
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
a✝ : reachable_from_list g (direct_succ_list g x✝) e.1
ih_4 : e.1 ∈ reachable_from_list g [x✝]
⊢ x ∈ reachable_from_list g [x✝]
Tactic:
case _ 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_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
ih : y ∈ direct_succ_list g x
⊢ y ∈ reachable_from_list g [x]
Tactic:
obtain s1 := mem_direct_succ_list_iff g x y
Proof state after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
ih : y ∈ direct_succ_list g x
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
ih : y ∈ direct_succ_list g x
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Tactic:
simp only [s1] at ih
Proof state after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Tactic:
apply Exists.elim ih
Proof state after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ ∀ (a : List Node), y ∈ a ∧ (x, a) ∈ g → y ∈ reachable_from_list g [x]
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
⊢ ∀ (a : List Node), y ∈ a ∧ (x, a) ∈ g → y ∈ reachable_from_list g [x]
Tactic:
intro ys a2
Proof state after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2 : y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2 : y ∈ ys ∧ (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Tactic:
cases a2
Proof state after:
case intro
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
left✝ : y ∈ ys
right✝ : (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Tactic:
case _ a2_left a2_right =>
  apply reachable_from_list.step y (x, ys) a2_right a2_left
  apply reachable_from_list.base x
  simp
Proof state after:
no goals
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ y ∈ reachable_from_list g [x]
Tactic:
apply reachable_from_list.step y (x, ys) a2_right a2_left
Proof state after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ reachable_from_list g [x] (x, ys).1
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ reachable_from_list g [x] (x, ys).1
Tactic:
apply reachable_from_list.base x
Proof state after:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ x ∈ [x]
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
x✝ : DecidableEq Node
g : Graph Node
x a y : Node
s1 : y ∈ direct_succ_list g x ↔ ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ih : ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
ys : List Node
a2_left : y ∈ ys
a2_right : (x, ys) ∈ g
⊢ x ∈ [x]
Tactic:
simp
Proof state after:
no goals
Theorem: reachable_from_list_direct_succ_list_is_subset_of_reachable_from_list
Proof state before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x✝ a x : Node
e : Node × List Node
ih_1 : e ∈ g
ih_2 : x ∈ e.2
a✝ : reachable_from_list g (direct_succ_list g x✝) e.1
ih_4 : e.1 ∈ reachable_from_list g [x✝]
⊢ x ∈ reachable_from_list g [x✝]
Tactic:
exact reachable_from_list.step x e ih_1 ih_2 ih_4
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
xs : List Node
⊢ reachable_from_list g (list_direct_succ_list g xs) ⊆ 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 ∈ reachable_from_list g (list_direct_succ_list g xs), x ∈ reachable_from_list g xs
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
xs : List Node
⊢ ∀ x ∈ reachable_from_list g (list_direct_succ_list g xs), 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 ∈ reachable_from_list g (list_direct_succ_list g xs)
⊢ x ∈ reachable_from_list g xs
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
xs : List Node
x : Node
a1 : x ∈ reachable_from_list g (list_direct_succ_list g xs)
⊢ x ∈ reachable_from_list g xs
Tactic:
induction xs
Proof state after:
case nil
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
a1 : x ∈ reachable_from_list g (list_direct_succ_list g [])
⊢ x ∈ reachable_from_list g []

case cons
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x head✝ : Node
tail✝ : List Node
tail_ih✝ : x ∈ reachable_from_list g (list_direct_succ_list g tail✝) → x ∈ reachable_from_list g tail✝
a1 : x ∈ reachable_from_list g (list_direct_succ_list g (head✝ :: tail✝))
⊢ x ∈ reachable_from_list g (head✝ :: tail✝)
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 : Node
a1 : x ∈ reachable_from_list g (list_direct_succ_list g [])
⊢ x ∈ reachable_from_list g []
Tactic:
case nil =>
  simp only [list_direct_succ_list] at a1
  simp at a1
  exact a1
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
a1 : x ∈ reachable_from_list g (list_direct_succ_list g (hd :: tl))
⊢ x ∈ reachable_from_list g (hd :: tl)
Tactic:
case cons hd tl ih =>
  simp only [list_direct_succ_list_cons] at a1
  simp only [reachable_from_list_of_cons g hd tl]
  simp
  simp only [reachable_from_list_of_append] at a1
  simp at a1
  cases a1
  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
  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 : Node
a1 : x ∈ reachable_from_list g (list_direct_succ_list g [])
⊢ x ∈ reachable_from_list g []
Tactic:
simp only [list_direct_succ_list] at a1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
a1 : x ∈ reachable_from_list g (List.map (fun x => direct_succ_list g x) []).join
⊢ x ∈ reachable_from_list g []
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 : Node
a1 : x ∈ reachable_from_list g (List.map (fun x => direct_succ_list g x) []).join
⊢ x ∈ reachable_from_list g []
Tactic:
simp at a1
Proof state after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
a1 : x ∈ reachable_from_list g []
⊢ x ∈ reachable_from_list g []
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 : Node
a1 : x ∈ reachable_from_list g []
⊢ x ∈ reachable_from_list g []
Tactic:
exact a1
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
a1 : x ∈ reachable_from_list g (list_direct_succ_list g (hd :: tl))
⊢ x ∈ reachable_from_list g (hd :: tl)
Tactic:
simp only [list_direct_succ_list_cons] 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 ++ list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g (hd :: 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 ++ list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g (hd :: tl)
Tactic:
simp only [reachable_from_list_of_cons g hd tl]
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 ++ list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g [hd] ∪ 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 ++ list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g [hd] ∪ reachable_from_list g tl
Tactic:
simp
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 ++ 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 ++ list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl
Tactic:
simp only [reachable_from_list_of_append] 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) ∪ reachable_from_list g (list_direct_succ_list g tl)
⊢ x ∈ reachable_from_list g [hd] ∨ x ∈ reachable_from_list g tl