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

State before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : S ⊆ ↑(x :: zs).toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Tactic:
simp only [list_cons_to_set_union] at h1
State after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : S ⊆ {x} ∪ ↑zs.toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset

State before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : S ⊆ {x} ∪ ↑zs.toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Tactic:
simp only [Set.subset_def] at h1
State after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, x_1 ∈ {x} ∪ ↑zs.toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset

State before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, x_1 ∈ {x} ∪ ↑zs.toFinset ∪ ↑ys.toFinset
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Tactic:
simp at h1
State after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset

State before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ↑(x :: ys).toFinset
Tactic:
simp only [list_cons_to_set_union]
State after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ({x} ∪ ↑ys.toFinset)

State before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑(xs ++ zs).toFinset ∪ ({x} ∪ ↑ys.toFinset)
Tactic:
simp only [list_append_to_set_union]
State after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑xs.toFinset ∪ ↑zs.toFinset ∪ ({x} ∪ ↑ys.toFinset)

State before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ↑xs.toFinset ∪ S ⊆ ↑xs.toFinset ∪ ↑zs.toFinset ∪ ({x} ∪ ↑ys.toFinset)
Tactic:
simp only [Set.subset_def]
State after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ∀ x_1 ∈ ↑xs.toFinset ∪ S, x_1 ∈ ↑xs.toFinset ∪ ↑zs.toFinset ∪ ({x} ∪ ↑ys.toFinset)

State before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ∀ x_1 ∈ ↑xs.toFinset ∪ S, x_1 ∈ ↑xs.toFinset ∪ ↑zs.toFinset ∪ ({x} ∪ ↑ys.toFinset)
Tactic:
simp
State after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ∀ (x_1 : Node), x_1 ∈ xs ∨ x_1 ∈ S → x_1 = x ∨ (x_1 ∈ xs ∨ x_1 ∈ zs) ∨ x_1 ∈ ys

State before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
⊢ ∀ (x_1 : Node), x_1 ∈ xs ∨ x_1 ∈ S → x_1 = x ∨ (x_1 ∈ xs ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
Tactic:
intro a a1
State after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
a : Node
a1 : a ∈ xs ∨ a ∈ S
⊢ a = x ∨ (a ∈ xs ∨ a ∈ zs) ∨ a ∈ ys

State before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x : Node
h1 : ∀ x_1 ∈ S, (x_1 = x ∨ x_1 ∈ zs) ∨ x_1 ∈ ys
a : Node
a1 : a ∈ xs ∨ a ∈ S
⊢ a = x ∨ (a ∈ xs ∨ a ∈ zs) ∨ a ∈ ys
Tactic:
specialize h1 a
State after:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x a : Node
a1 : a ∈ xs ∨ a ∈ S
h1 : a ∈ S → (a = x ∨ a ∈ zs) ∨ a ∈ ys
⊢ a = x ∨ (a ∈ xs ∨ a ∈ zs) ∨ a ∈ ys

State before:
Node : Type
inst : DecidableEq Node
xs ys zs : List Node
S : Set Node
x a : Node
a1 : a ∈ xs ∨ a ∈ S
h1 : a ∈ S → (a = x ∨ a ∈ zs) ∨ a ∈ ys
⊢ a = x ∨ (a ∈ xs ∨ a ∈ zs) ∨ a ∈ ys
Tactic:
tauto
State after:
no goals