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

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

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

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

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

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

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

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

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