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

State before:
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x :: zs ⊆ xs
Tactic:
simp
State after:
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x ∈ xs ∧ zs ⊆ xs

State before:
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x ∈ xs ∧ zs ⊆ xs
Tactic:
constructor
State after:
case left
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x ∈ xs

case right
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ zs ⊆ xs

State before:
case left
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x ∈ xs
Tactic:
apply Set.mem_of_subset_of_mem h3 h2
State after:
no goals

State before:
case right
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ zs ⊆ xs
Tactic:
exact h1
State after:
no goals