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

State before:
α : Type u_1
l : List α
⊢ ∀ (x : α), x ∈ l → x ∈ asSet l
Tactic:
intros y h
State after:
α : Type u_1
l : List α
y : α
h : y ∈ l
⊢ y ∈ asSet l

State before:
α : Type u_1
l : List α
y : α
h : y ∈ l
⊢ y ∈ asSet l
Tactic:
simp [asSet]
State after:
α : Type u_1
l : List α
y : α
h : y ∈ l
⊢ y ∈ l

State before:
α : Type u_1
l : List α
y : α
h : y ∈ l
⊢ y ∈ l
Tactic:
exact h
State after:
no goals