chore(data/set/pointwise): split file and reduce imports (#17991)

src/algebra/bounds.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
 import algebra.order.group.order_iso
+import algebra.order.monoid.order_dual
 import data.set.pointwise.basic
 import order.bounds.order_iso
 import order.conditionally_complete_lattice.basic

src/data/finset/pointwise.lean

@@ -6,6 +6,7 @@ Authors: Floris van Doorn, Yaël Dillies
 import data.finset.n_ary
 import data.finset.preimage
 import data.set.pointwise.smul
+import data.set.pointwise.list_of_fn
 
 /-!
 # Pointwise operations of finsets

src/data/set/pointwise/basic.lean

@@ -3,8 +3,11 @@ Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Floris van Doorn
 -/
+import algebra.group_power.basic
+import algebra.hom.equiv.basic
+import algebra.hom.units
 import data.set.lattice
-import data.list.of_fn
+import data.nat.order.basic
 
 /-!
 # Pointwise operations of sets
@@ -443,32 +446,6 @@ begin
     exact ih.trans (subset_mul_right _ hs) }
 end
 
-@[to_additive] lemma mem_prod_list_of_fn {a : α} {s : fin n → set α} :
-  a ∈ (list.of_fn s).prod ↔ ∃ f : (Π i : fin n, s i), (list.of_fn (λ i, (f i : α))).prod = a :=
-begin
-  induction n with n ih generalizing a,
-  { simp_rw [list.of_fn_zero, list.prod_nil, fin.exists_fin_zero_pi, eq_comm, set.mem_one] },
-  { simp_rw [list.of_fn_succ, list.prod_cons, fin.exists_fin_succ_pi, fin.cons_zero, fin.cons_succ,
-      mem_mul, @ih, exists_and_distrib_left, exists_exists_eq_and, set_coe.exists, subtype.coe_mk,
-      exists_prop] }
-end
-
-@[to_additive] lemma mem_list_prod {l : list (set α)} {a : α} :
-  a ∈ l.prod ↔ ∃ l' : list (Σ s : set α, ↥s),
-    list.prod (l'.map (λ x, (sigma.snd x : α))) = a ∧ l'.map sigma.fst = l :=
-begin
-  induction l using list.of_fn_rec with n f,
-  simp_rw [list.exists_iff_exists_tuple, list.map_of_fn, list.of_fn_inj', and.left_comm,
-    exists_and_distrib_left, exists_eq_left, heq_iff_eq, function.comp, mem_prod_list_of_fn],
-  split,
-  { rintros ⟨fi, rfl⟩,  exact ⟨λ i, ⟨_, fi i⟩, rfl, rfl⟩, },
-  { rintros ⟨fi, rfl, rfl⟩, exact ⟨λ i, _, rfl⟩, },
-end
-
-@[to_additive] lemma mem_pow {a : α} {n : ℕ} :
-  a ∈ s ^ n ↔ ∃ f : fin n → s, (list.of_fn (λ i, (f i : α))).prod = a :=
-by rw [←mem_prod_list_of_fn, list.of_fn_const, list.prod_repeat]
-
 @[simp, to_additive] lemma empty_pow {n : ℕ} (hn : n ≠ 0) : (∅ : set α) ^ n = ∅ :=
 by rw [← tsub_add_cancel_of_le (nat.succ_le_of_lt $ nat.pos_of_ne_zero hn), pow_succ, empty_mul]
 

src/data/set/pointwise/list_of_fn.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2022 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+
+import data.set.pointwise.basic
+import data.list.of_fn
+
+/-!
+# Pointwise operations with lists of sets
+
+This file proves some lemmas about pointwise algebraic operations with lists of sets.
+-/
+
+namespace set
+
+variables {F α β γ : Type*}
+variables [monoid α] {s t : set α} {a : α} {m n : ℕ}
+
+open_locale pointwise
+
+@[to_additive] lemma mem_prod_list_of_fn {a : α} {s : fin n → set α} :
+  a ∈ (list.of_fn s).prod ↔ ∃ f : (Π i : fin n, s i), (list.of_fn (λ i, (f i : α))).prod = a :=
+begin
+  induction n with n ih generalizing a,
+  { simp_rw [list.of_fn_zero, list.prod_nil, fin.exists_fin_zero_pi, eq_comm, set.mem_one] },
+  { simp_rw [list.of_fn_succ, list.prod_cons, fin.exists_fin_succ_pi, fin.cons_zero, fin.cons_succ,
+      mem_mul, @ih, exists_and_distrib_left, exists_exists_eq_and, set_coe.exists, subtype.coe_mk,
+      exists_prop] }
+end
+
+@[to_additive] lemma mem_list_prod {l : list (set α)} {a : α} :
+  a ∈ l.prod ↔ ∃ l' : list (Σ s : set α, ↥s),
+    list.prod (l'.map (λ x, (sigma.snd x : α))) = a ∧ l'.map sigma.fst = l :=
+begin
+  induction l using list.of_fn_rec with n f,
+  simp_rw [list.exists_iff_exists_tuple, list.map_of_fn, list.of_fn_inj', and.left_comm,
+    exists_and_distrib_left, exists_eq_left, heq_iff_eq, function.comp, mem_prod_list_of_fn],
+  split,
+  { rintros ⟨fi, rfl⟩,  exact ⟨λ i, ⟨_, fi i⟩, rfl, rfl⟩, },
+  { rintros ⟨fi, rfl, rfl⟩, exact ⟨λ i, _, rfl⟩, },
+end
+
+@[to_additive] lemma mem_pow {a : α} {n : ℕ} :
+  a ∈ s ^ n ↔ ∃ f : fin n → s, (list.of_fn (λ i, (f i : α))).prod = a :=
+by rw [←mem_prod_list_of_fn, list.of_fn_const, list.prod_repeat]
+
+end set

src/data/set/pointwise/smul.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin, Floris van Doorn
 import algebra.module.basic
 import data.set.pairwise
 import data.set.pointwise.basic
+import tactic.by_contra
 
 /-!
 # Pointwise operations of sets