Theorem: liftedSet.index_union (Var/liftedSet.lean)

State before:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ ((s₁ | ρ) ∪ s₂ | ρ) = (s₁ ∪ s₂) | ρ
Tactic:
simp [Set.union_def]
State after:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a ∈ s₁ | ρ) ∨ a ∈ s₂ | ρ} = {a | a ∈ s₁ ∨ a ∈ s₂} | ρ

State before:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a ∈ s₁ | ρ) ∨ a ∈ s₂ | ρ} = {a | a ∈ s₁ ∨ a ∈ s₂} | ρ
Tactic:
simp [index_mem]
State after:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = {a | a ∈ s₁ ∨ a ∈ s₂} | ρ

State before:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = {a | a ∈ s₁ ∨ a ∈ s₂} | ρ
Tactic:
simp [vset.Variational]
State after:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = vset.index {a | a ∈ s₁ ∨ a ∈ s₂} ρ

State before:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = vset.index {a | a ∈ s₁ ∨ a ∈ s₂} ρ
Tactic:
unfold vset.index
State after:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = fun x => {a | a ∈ s₁ ∨ a ∈ s₂} (x, ρ)

State before:
α F : Type
s₁ s₂ : vset F α
ρ : SPL.Config F
⊢ {a | (a, ρ) ∈ s₁ ∨ (a, ρ) ∈ s₂} = fun x => {a | a ∈ s₁ ∨ a ∈ s₂} (x, ρ)
Tactic:
simp [vset.index, Set.union, Set.union_def, Set.mem_def, setOf]
State after:
no goals