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

State before:
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑(x :: ys).toFinset ∪ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
simp only [list_cons_to_set_union]
State after:
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ∪ ↑ys.toFinset ∪ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset

State before:
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ∪ ↑ys.toFinset ∪ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
apply Set.union_subset
State after:
case sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ∪ ↑ys.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset

case tr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset

State before:
case sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ∪ ↑ys.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
apply Set.union_subset
State after:
case sr.sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ⊆ ↑ys.toFinset ∪ ↑xs.toFinset

case sr.tr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑ys.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset

State before:
case sr.sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ {x} ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
simp
State after:
case sr.sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ x ∈ ys ∨ x ∈ xs

State before:
case sr.sr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ x ∈ ys ∨ x ∈ xs
Tactic:
right
State after:
case sr.sr.h
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ x ∈ xs

State before:
case sr.sr.h
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ x ∈ xs
Tactic:
exact h1
State after:
no goals

State before:
case sr.tr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑ys.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
exact Set.subset_union_left ys.toFinset.toSet xs.toFinset.toSet
State after:
no goals

State before:
case tr
α : Type
inst : DecidableEq α
xs ys : List α
x : α
h1 : x ∈ xs
⊢ ↑xs.toFinset ⊆ ↑ys.toFinset ∪ ↑xs.toFinset
Tactic:
exact Set.subset_union_right ys.toFinset.toSet xs.toFinset.toSet
State after:
no goals