feat(group_theory/subgroup): add several trivial lemmas (#16633)

* add `subgroup.top_to_submonoid` and `subgroup.bot_to_submonoid`;
* add `free_monoid.mrange_lift`.

src/group_theory/subgroup/basic.lean

@@ -648,11 +648,12 @@ instance : inhabited (subgroup G) := ⟨⊥⟩
 
 @[to_additive] instance : unique (⊥ : subgroup G) := ⟨⟨1⟩, λ g, subtype.ext g.2⟩
 
+@[simp, to_additive] lemma top_to_submonoid : (⊤ : subgroup G).to_submonoid = ⊤ := rfl
+
+@[simp, to_additive] lemma bot_to_submonoid : (⊥ : subgroup G).to_submonoid = ⊥ := rfl
+
 @[to_additive] lemma eq_bot_iff_forall : H = ⊥ ↔ ∀ x ∈ H, x = (1 : G) :=
-begin
-  rw set_like.ext'_iff,
-  simp only [coe_bot, set.eq_singleton_iff_unique_mem, set_like.mem_coe, H.one_mem, true_and],
-end
+to_submonoid_injective.eq_iff.symm.trans $ submonoid.eq_bot_iff_forall _
 
 @[to_additive] lemma eq_bot_of_subsingleton [subsingleton H] : H = ⊥ :=
 begin

src/group_theory/submonoid/membership.lean

@@ -280,10 +280,14 @@ mem_closure_singleton.2 ⟨1, pow_one y⟩
 lemma closure_singleton_one : closure ({1} : set M) = ⊥ :=
 by simp [eq_bot_iff_forall, mem_closure_singleton]
 
+@[to_additive] lemma _root_.free_monoid.mrange_lift {α} (f : α → M) :
+  (free_monoid.lift f).mrange = closure (set.range f) :=
+by rw [mrange_eq_map, ← free_monoid.closure_range_of, map_mclosure, ← set.range_comp,
+  free_monoid.lift_comp_of]
+
 @[to_additive]
 lemma closure_eq_mrange (s : set M) : closure s = (free_monoid.lift (coe : s → M)).mrange :=
-by rw [mrange_eq_map, ← free_monoid.closure_range_of, map_mclosure, ← set.range_comp,
-  free_monoid.lift_comp_of, subtype.range_coe]
+by rw [free_monoid.mrange_lift, 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} :=