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

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

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

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

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

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

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

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

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

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

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