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 : (i : Fin n) → ↑(s i)), List.sum (List.ofFn fun (i : Fin n) => ↑(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 : (i : Fin n) → ↑(s i)), List.prod (List.ofFn fun (i : Fin n) => ↑(f i)) = a

theorem Set.mem_list_sum {α : Type u_2} [AddMonoid α] {l : List (Set α)} {a : α} : a ∈ List.sum l ↔ ∃ (l' : List ((s : Set α) × ↑s)), List.sum (List.map (fun (x : (s : Set α) × ↑s) => ↑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 ((s : Set α) × ↑s)), List.prod (List.map (fun (x : (s : Set α) × ↑s) => ↑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 : Fin n → ↑s), List.sum (List.ofFn fun (i : Fin n) => ↑(f i)) = a

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