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

State before:
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x : Node
⊢ ↑(direct_succ_list g x).toFinset = direct_succ_set g x
Tactic:
ext a
State after:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ ↑(direct_succ_list g x).toFinset ↔ a ∈ direct_succ_set g x

State before:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ ↑(direct_succ_list g x).toFinset ↔ a ∈ direct_succ_set g x
Tactic:
simp only [direct_succ_set]
State after:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ ↑(direct_succ_list g x).toFinset ↔ a ∈ {y | ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}

State before:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ ↑(direct_succ_list g x).toFinset ↔ a ∈ {y | ∃ ys, y ∈ ys ∧ (x, ys) ∈ g}
Tactic:
simp
State after:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ direct_succ_list g x ↔ ∃ ys, a ∈ ys ∧ (x, ys) ∈ g

State before:
case h
Node : Type
inst✝ : DecidableEq Node
g : Graph Node
x a : Node
⊢ a ∈ direct_succ_list g x ↔ ∃ ys, a ∈ ys ∧ (x, ys) ∈ g
Tactic:
simp only [mem_direct_succ_list_iff]
State after:
no goals