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

State before:
α : Type u_1
inst✝ : Semiring α
l : List α
x : α
h : x ∈ l
⊢ x ∈ asIdeal l
Tactic:
have list_in_ideal := listInIdeal l
State after:
α : Type u_1
inst✝ : Semiring α
l : List α
x : α
h : x ∈ l
list_in_ideal : ∀ (x : α), x ∈ l → x ∈ asIdeal l
⊢ x ∈ asIdeal l

State before:
α : Type u_1
inst✝ : Semiring α
l : List α
x : α
h : x ∈ l
list_in_ideal : ∀ (x : α), x ∈ l → x ∈ asIdeal l
⊢ x ∈ asIdeal l
Tactic:
exact list_in_ideal x h
State after:
no goals