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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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