feat(data/list/basic): add list.range_map (#13777)

* add `list.range_map` and `list.range_map_coe`;
* add `submonoid.closure_eq_image_prod` and `add_submonoid.closure_eq_image_prod`.

Author: urkud

src/data/list/basic.lean

@@ -185,17 +185,28 @@ lemma map_bind (g : β → list γ) (f : α → β) :
 | [] := rfl
 | (a::l) := by simp only [cons_bind, map_cons, map_bind l]
 
+lemma range_map (f : α → β) : set.range (map f) = {l | ∀ x ∈ l, x ∈ set.range f} :=
+begin
+  refine set.subset.antisymm (set.range_subset_iff.2 $
+    λ l, forall_mem_map_iff.2 $ λ y _, set.mem_range_self _) (λ l hl, _),
+  induction l with a l ihl, { exact ⟨[], rfl⟩ },
+  rcases ihl (λ x hx, hl x $ subset_cons _ _ hx) with ⟨l, rfl⟩,
+  rcases hl a (mem_cons_self _ _) with ⟨a, rfl⟩,
+  exact ⟨a :: l, map_cons _ _ _⟩
+end
+
+lemma range_map_coe (s : set α) : set.range (map (coe : s → α)) = {l | ∀ x ∈ l, x ∈ s} :=
+by rw [range_map, subtype.range_coe]
+
 /-- If each element of a list can be lifted to some type, then the whole list can be lifted to this
 type. -/
 instance [h : can_lift α β] : can_lift (list α) (list β) :=
 { coe := list.map h.coe,
   cond := λ l, ∀ x ∈ l, can_lift.cond β x,
   prf  := λ l H,
     begin
-      induction l with a l ihl, { exact ⟨[], rfl⟩ },
-      rcases ihl (λ x hx, H x (or.inr hx)) with ⟨l, rfl⟩,
-      rcases can_lift.prf a (H a (or.inl rfl)) with ⟨a, rfl⟩,
-      exact ⟨a :: l, rfl⟩
+      rw [← set.mem_range, range_map],
+      exact λ a ha, can_lift.prf a (H a ha),
     end}
 
 /-! ### length -/

src/group_theory/submonoid/membership.lean

@@ -285,14 +285,17 @@ lemma closure_eq_mrange (s : set M) : closure s = (free_monoid.lift (coe : s →
 by rw [mrange_eq_map, ← free_monoid.closure_range_of, map_mclosure, ← set.range_comp,
   free_monoid.lift_comp_of, subtype.range_coe]
 
+@[to_additive] lemma closure_eq_image_prod (s : set M) :
+  (closure s : set M) = list.prod '' {l : list M | ∀ x ∈ l, x ∈ s} :=
+begin
+  rw [closure_eq_mrange, coe_mrange, ← list.range_map_coe, ← set.range_comp],
+  refl
+end
+
 @[to_additive]
 lemma exists_list_of_mem_closure {s : set M} {x : M} (hx : x ∈ closure s) :
   ∃ (l : list M) (hl : ∀ y ∈ l, y ∈ s), l.prod = x :=
-begin
-  rw [closure_eq_mrange, mem_mrange] at hx,
-  rcases hx with ⟨l, hx⟩,
-  exact ⟨list.map coe l, λ y hy, let ⟨z, hz, hy⟩ := list.mem_map.1 hy in hy ▸ z.2, hx⟩
-end
+by rwa [← set_like.mem_coe, closure_eq_image_prod, set.mem_image_iff_bex] at hx
 
 @[to_additive]
 lemma exists_multiset_of_mem_closure {M : Type*} [comm_monoid M] {s : set M}