feat(group_theory/subgroup/basic): apply_mem_map_injective (#9637)

A translation of `function.injective.mem_set_image`.

src/group_theory/subgroup/basic.lean

@@ -842,6 +842,11 @@ lemma mem_map_equiv {f : G ≃* N} {K : subgroup G} {x : N} :
   x ∈ K.map f.to_monoid_hom ↔ f.symm x ∈ K :=
 @set.mem_image_equiv _ _ ↑K f.to_equiv x
 
+@[to_additive]
+lemma mem_map_iff_mem {f : G →* N} (hf : function.injective f) {K : subgroup G} {x : G} :
+  f x ∈ K.map f ↔ x ∈ K :=
+hf.mem_set_image
+
 @[to_additive]
 lemma map_equiv_eq_comap_symm (f : G ≃* N) (K : subgroup G) :
   K.map f.to_monoid_hom = K.comap f.symm.to_monoid_hom :=

src/group_theory/submonoid/operations.lean

@@ -208,6 +208,11 @@ mem_map_of_mem f x.prop
 lemma map_map (g : N →* P) (f : M →* N) : (S.map f).map g = S.map (g.comp f) :=
 set_like.coe_injective $ image_image _ _ _
 
+@[to_additive]
+lemma mem_map_iff_mem {f : M →* N} (hf : function.injective f) {S : submonoid M} {x : M} :
+  f x ∈ S.map f ↔ x ∈ S :=
+hf.mem_set_image
+
 @[to_additive]
 lemma map_le_iff_le_comap {f : M →* N} {S : submonoid M} {T : submonoid N} :
   S.map f ≤ T ↔ S ≤ T.comap f :=