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

State before:
α : Type u_1
l₁ l₂ : List α
⊢ asSet (l₁ ++ l₂) = asSet l₁ ∪ asSet l₂
Tactic:
induction l₂
State after:
case nil
α : Type u_1
l₁ : List α
⊢ asSet (l₁ ++ []) = asSet l₁ ∪ asSet []

case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ asSet (l₁ ++ head✝ :: tail✝) = asSet l₁ ∪ asSet (head✝ :: tail✝)

State before:
case nil
α : Type u_1
l₁ : List α
⊢ asSet (l₁ ++ []) = asSet l₁ ∪ asSet []

case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ asSet (l₁ ++ head✝ :: tail✝) = asSet l₁ ∪ asSet (head✝ :: tail✝)
Tactic:
simp [asSet]
State after:
case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ asSet (l₁ ++ head✝ :: tail✝) = asSet l₁ ∪ asSet (head✝ :: tail✝)

State before:
case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ asSet (l₁ ++ head✝ :: tail✝) = asSet l₁ ∪ asSet (head✝ :: tail✝)
Tactic:
simp [asSet]
State after:
case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ { x | x ∈ l₁ ∨ x = head✝ ∨ x ∈ tail✝ } = { x | x ∈ l₁ } ∪ { x | x = head✝ ∨ x ∈ tail✝ }

State before:
case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ { x | x ∈ l₁ ∨ x = head✝ ∨ x ∈ tail✝ } = { x | x ∈ l₁ } ∪ { x | x = head✝ ∨ x ∈ tail✝ }
Tactic:
constructor
State after:
no goals