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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ list_direct_succ_set g (x :: xs) = ↑(direct_succ_list g x).toFinset ∪ list_direct_succ_set g xs
Tactic:
simp only [list_direct_succ_set]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | ∃ x_1 ∈ x :: xs, ∃ ys, y ∈ ys ∧ (x_1, ys) ∈ g} =
    ↑(direct_succ_list g x).toFinset ∪ {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | ∃ x_1 ∈ x :: xs, ∃ ys, y ∈ ys ∧ (x_1, ys) ∈ g} =
    ↑(direct_succ_list g x).toFinset ∪ {y | ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}
Tactic:
simp only [← mem_direct_succ_list_iff]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | ∃ x_1 ∈ x :: xs, y ∈ direct_succ_list g x_1} =
    ↑(direct_succ_list g x).toFinset ∪ {y | ∃ x ∈ xs, y ∈ direct_succ_list g x}

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | ∃ x_1 ∈ x :: xs, y ∈ direct_succ_list g x_1} =
    ↑(direct_succ_list g x).toFinset ∪ {y | ∃ x ∈ xs, y ∈ direct_succ_list g x}
Tactic:
simp
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | y ∈ direct_succ_list g x ∨ ∃ a ∈ xs, y ∈ direct_succ_list g a} =
    {a | a ∈ direct_succ_list g x} ∪ {y | ∃ x ∈ xs, y ∈ direct_succ_list g x}

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
xs : List Node
⊢ {y | y ∈ direct_succ_list g x ∨ ∃ a ∈ xs, y ∈ direct_succ_list g a} =
    {a | a ∈ direct_succ_list g x} ∪ {y | ∃ x ∈ xs, y ∈ direct_succ_list g x}
Tactic:
rfl
State after:
no goals