change name

Author: CoolRmal

Mathlib/GroupTheory/Nilpotent.lean

@@ -115,8 +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]
 
-instance [hH : H.Characteristic] : Characteristic (upperCentralSeriesStep H) :=
-  (upperCentralSeriesStep_eq_comap_center H) ▸ centerCharacteristic.comap_quotient_mk
+instance [H.Characteristic] : Characteristic (upperCentralSeriesStep H) :=
+  (upperCentralSeriesStep_eq_comap_center H) ▸ Characteristic.comap_quotient_mk centerCharacteristic
 
 variable (G)
 

Mathlib/GroupTheory/QuotientGroup/Basic.lean

@@ -392,12 +392,12 @@ theorem comap_comap_center {H₁ : Subgroup G} [H₁.Normal] {H₂ : Subgroup (G
 
 open Subgroup in
 @[to_additive]
-theorem _root_.Subgroup.Characteristic.comap_quotient_mk {N : Subgroup G} [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
+theorem _root_.Subgroup.Characteristic.comap_quotient_mk {H : Subgroup G} [H.Characteristic]
+    {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 inferInstance ϕ))
+  have := mem_map_of_mem (congr H H ϕ (characteristic_iff_map_eq.1 inferInstance ϕ)).toMonoidHom hy
   simp_all
 
 end QuotientGroup