theorem Set.mem_pow_iff_fin_prod {α : Type u_1} [Monoid α] {a : α} {s : Set α} {n : ℕ} : a ∈ s ^ n ↔ ∃ (f : Fin n → α), (∀ (i : Fin n), f i ∈ s) ∧ Fin.prod f = a

theorem Set.mem_pow_iff_list_prod {α : Type u_1} [Monoid α] {a : α} {s : Set α} {n : ℕ} : a ∈ s ^ n ↔ ∃ (l : List α), l.length = n ∧ (∀ (x : α), x ∈ l → x ∈ s) ∧ l.prod = a

theorem Set.pow_subset {α : Type u_1} [Monoid α] {s t : Set α} {n : ℕ} : s ^ n ⊆ t ↔ ∀ (l : List α), l.length = n → (∀ (x : α), x ∈ l → x ∈ s) → l.prod ∈ t