Theorem: reachable_from_list_list_direct_succ_list_is_subset_of_reachable_from_list (FOL/Parsing/DFT.lean)

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]
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

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
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

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
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✝)

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
State after:
no goals

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
State after:
no goals

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
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 []

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
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
a1 : x ∈ reachable_from_list g []
⊢ x ∈ reachable_from_list g []

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
State after:
no goals

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
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)

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]
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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
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]

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
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]

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
State after:
no goals

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
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

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
State after:
no goals