feat(algebra/pointwise): pow_mem_pow (#7822)

If `a ∈ s` then `a ^ n ∈ s ^ n`.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

Author: tb65536

src/algebra/pointwise.lean

@@ -141,6 +141,16 @@ instance [monoid α] : monoid (set α) :=
 { ..set.semigroup,
   ..set.mul_one_class }
 
+lemma pow_mem_pow [monoid α] (ha : a ∈ s) (n : ℕ) :
+  a ^ n ∈ s ^ n :=
+begin
+  induction n with n ih,
+  { rw pow_zero,
+    exact set.mem_singleton 1 },
+  { rw pow_succ,
+    exact set.mul_mem_mul ha ih },
+end
+
 @[to_additive]
 protected lemma mul_comm [comm_semigroup α] : s * t = t * s :=
 by simp only [← image2_mul, image2_swap _ s, mul_comm]
@@ -163,6 +173,16 @@ lemma mul_empty [has_mul α] : s * ∅ = ∅ := image2_empty_right
 lemma mul_subset_mul [has_mul α] (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ * s₂ ⊆ t₁ * t₂ :=
 image2_subset h₁ h₂
 
+lemma pow_subset_pow [monoid α] (hst : s ⊆ t) (n : ℕ) :
+  s ^ n ⊆ t ^ n :=
+begin
+  induction n with n ih,
+  { rw pow_zero,
+    exact subset.rfl },
+  { rw [pow_succ, pow_succ],
+    exact mul_subset_mul hst ih },
+end
+
 @[to_additive]
 lemma union_mul [has_mul α] : (s ∪ t) * u = (s * u) ∪ (t * u) := image2_union_left