move lemma

Author: CoolRmal

Mathlib/GroupTheory/Nilpotent.lean

@@ -115,17 +115,8 @@ theorem upperCentralSeriesStep_eq_comap_center :
   rw [coe_mk', ← QuotientGroup.mk_mul, ← QuotientGroup.mk_mul, eq_comm, eq_iff_div_mem,
     div_eq_mul_inv, mul_inv_rev, mul_assoc]
 
-@[to_additive]
-theorem Subgroup.Characteristic.quotient [hH : Characteristic H] {K : Subgroup (G ⧸ H)}
-    (hK : K.Characteristic) :
-    Characteristic (K.comap (mk' H)) := by
-  refine characteristic_iff_map_le.2 fun ϕ x ⟨y, hy⟩ => ?_
-  have := characteristic_iff_map_eq.1 hK (congr H H ϕ (characteristic_iff_map_eq.1 hH ϕ))
-  have := mem_map_of_mem (congr H H ϕ (characteristic_iff_map_eq.1 hH ϕ)).toMonoidHom hy.1
-  simp_all
-
 instance [hH : H.Characteristic] : Characteristic (upperCentralSeriesStep H) :=
-  (upperCentralSeriesStep_eq_comap_center H) ▸ hH.quotient H centerCharacteristic
+  (upperCentralSeriesStep_eq_comap_center H) ▸ comap_Characteristic H centerCharacteristic
 
 variable (G)
 

Mathlib/GroupTheory/QuotientGroup/Basic.lean

@@ -390,6 +390,16 @@ theorem comap_comap_center {H₁ : Subgroup G} [H₁.Normal] {H₂ : Subgroup (G
   simp only [mk'_apply, Subgroup.mem_comap, Subgroup.mem_center_iff, forall_mk, ← mk_mul,
     eq_iff_div_mem, mk_div]
 
+open Subgroup in
+@[to_additive]
+theorem comap_Characteristic [hN : N.Characteristic] {K : Subgroup (G ⧸ N)}
+    (hK : K.Characteristic) :
+    Characteristic (K.comap (mk' N)) := by
+  refine characteristic_iff_map_le.2 fun ϕ x ⟨y, hy⟩ => ?_
+  have := characteristic_iff_map_eq.1 hK (congr N N ϕ (characteristic_iff_map_eq.1 hN ϕ))
+  have := mem_map_of_mem (congr N N ϕ (characteristic_iff_map_eq.1 hN ϕ)).toMonoidHom hy.1
+  simp_all
+
 end QuotientGroup
 
 namespace QuotientAddGroup