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

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

State before:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
⊢ y ∈ asIdeal l
Tactic:
rw [asIdeal, asSet]
State after:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
⊢ y ∈ span { x | x ∈ l }

State before:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
⊢ y ∈ span { x | x ∈ l }
Tactic:
have in_set := listInSet l y h
State after:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ asSet l
⊢ y ∈ span { x | x ∈ l }

State before:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ asSet l
⊢ y ∈ span { x | x ∈ l }
Tactic:
rw [asSet] at in_set
State after:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ { x | x ∈ l }
⊢ y ∈ span { x | x ∈ l }

State before:
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ { x | x ∈ l }
⊢ y ∈ span { x | x ∈ l }
Tactic:
apply Ideal.subset_span
State after:
case a
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ { x | x ∈ l }
⊢ y ∈ { x | x ∈ l }

State before:
case a
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ { x | x ∈ l }
⊢ y ∈ { x | x ∈ l }
Tactic:
exact in_set
State after:
no goals