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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
⊢ ∀ (xs : List Node) (y : Node), y ∈ list_direct_succ_list g xs ↔ ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g
Tactic:
simp only [list_direct_succ_list]
State after:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
⊢ ∀ (xs : List Node) (y : Node),
    y ∈ (List.map (fun x => direct_succ_list g x) xs).join ↔ ∃ x ∈ xs, ∃ ys, y ∈ ys ∧ (x, ys) ∈ g

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
⊢ ∀ (xs : List Node) (y : Node),
    y ∈ (List.map (fun x => direct_succ_list g x) xs).join ↔ ∃ 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
⊢ ∀ (xs : List Node) (y : Node),
    y ∈ (List.map (fun x => direct_succ_list g x) xs).join ↔ ∃ x ∈ xs, y ∈ direct_succ_list g x

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
⊢ ∀ (xs : List Node) (y : Node),
    y ∈ (List.map (fun x => direct_succ_list g x) xs).join ↔ ∃ x ∈ xs, y ∈ direct_succ_list g x
Tactic:
simp
State after:
no goals