Theorem: IdealHelpers.subsets_h (Diploma/Algebra/IdealHelpers.lean)

State before:
α : Type u_1
l : List α
s : Set α
h : ∀ (e : α), e ∈ l → e ∈ s
⊢ asSet l ⊆ s
Tactic:
rw [asSet]
State after:
α : Type u_1
l : List α
s : Set α
h : ∀ (e : α), e ∈ l → e ∈ s
⊢ { x | x ∈ l } ⊆ s

State before:
α : Type u_1
l : List α
s : Set α
h : ∀ (e : α), e ∈ l → e ∈ s
⊢ { x | x ∈ l } ⊆ s
Tactic:
exact h
State after:
no goals