Pointwise operations with lists of sets

This file proves some lemmas about pointwise algebraic operations with lists of sets.

theorem Set.mem_sum_list_ofFn {α : Type u_2} [AddMonoid α] {n : ℕ} {a : α} {s : Fin n → Set α} : a ∈ List.sum (List.ofFn s) ↔ ∃ f, List.sum (List.ofFn fun i => ↑(f i)) = a

theorem Set.mem_prod_list_ofFn {α : Type u_2} [Monoid α] {n : ℕ} {a : α} {s : Fin n → Set α} : a ∈ List.prod (List.ofFn s) ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a

theorem Set.mem_list_sum {α : Type u_2} [AddMonoid α] {l : List (Set α)} {a : α} : a ∈ List.sum l ↔ ∃ l', List.sum (List.map (fun x => ↑x.snd) l') = a ∧ List.map Sigma.fst l' = l

theorem Set.mem_list_prod {α : Type u_2} [Monoid α] {l : List (Set α)} {a : α} : a ∈ List.prod l ↔ ∃ l', List.prod (List.map (fun x => ↑x.snd) l') = a ∧ List.map Sigma.fst l' = l

theorem Set.mem_nsmul {α : Type u_2} [AddMonoid α] {s : Set α} {a : α} {n : ℕ} : a ∈ n • s ↔ ∃ f, List.sum (List.ofFn fun i => ↑(f i)) = a

theorem Set.mem_pow {α : Type u_2} [Monoid α] {s : Set α} {a : α} {n : ℕ} : a ∈ s ^ n ↔ ∃ f, List.prod (List.ofFn fun i => ↑(f i)) = a