diff --git a/Mathlib/GroupTheory/Nilpotent.lean b/Mathlib/GroupTheory/Nilpotent.lean
index 0a3d276d65b99..2dc5083ee285d 100644
--- a/Mathlib/GroupTheory/Nilpotent.lean
+++ b/Mathlib/GroupTheory/Nilpotent.lean
@@ -374,8 +374,7 @@ theorem upperCentralSeries_eq_top_iff_nilpotencyClass_le {n : ℕ} :
   · intro h
     exact Nat.find_le h
   · intro h
-    apply eq_top_iff.mpr
-    rw [← upperCentralSeries_nilpotencyClass]
+    rw [eq_top_iff, ← upperCentralSeries_nilpotencyClass]
     exact upperCentralSeries_mono _ h
 #align upper_central_series_eq_top_iff_nilpotency_class_le upperCentralSeries_eq_top_iff_nilpotencyClass_le
 
@@ -413,7 +412,7 @@ theorem least_descending_central_series_length_eq_nilpotencyClass :
 
 /-- The nilpotency class of a nilpotent `G` is equal to the length of the lower central series. -/
 theorem lowerCentralSeries_length_eq_nilpotencyClass :
-    Nat.find (nilpotent_iff_lowerCentralSeries.mp hG) = @Group.nilpotencyClass G _ _ := by
+    Nat.find (nilpotent_iff_lowerCentralSeries.mp hG) = Group.nilpotencyClass (G := G) := by
   rw [← least_descending_central_series_length_eq_nilpotencyClass]
   refine' le_antisymm (Nat.find_mono _) (Nat.find_mono _)
   · rintro n ⟨H, ⟨hH, hn⟩⟩
@@ -437,8 +436,7 @@ theorem lowerCentralSeries_eq_bot_iff_nilpotencyClass_le {n : ℕ} :
     rw [← lowerCentralSeries_length_eq_nilpotencyClass]
     exact Nat.find_le h
   · intro h
-    apply eq_bot_iff.mpr
-    rw [← lowerCentralSeries_nilpotencyClass]
+    rw [eq_bot_iff, ← lowerCentralSeries_nilpotencyClass]
     exact lowerCentralSeries_antitone h
 #align lower_central_series_eq_bot_iff_nilpotency_class_le lowerCentralSeries_eq_bot_iff_nilpotencyClass_le
 
@@ -523,14 +521,14 @@ theorem isNilpotent_of_ker_le_center {H : Type*} [Group H] (f : G →* H) (hf1 :
 
 theorem nilpotencyClass_le_of_ker_le_center {H : Type*} [Group H] (f : G →* H)
     (hf1 : f.ker ≤ center G) (hH : IsNilpotent H) :
-    @Group.nilpotencyClass G _ (isNilpotent_of_ker_le_center f hf1 hH) ≤
+    Group.nilpotencyClass (hG := isNilpotent_of_ker_le_center f hf1 hH) ≤
       Group.nilpotencyClass H + 1 := by
   haveI : IsNilpotent G := isNilpotent_of_ker_le_center f hf1 hH
   rw [← lowerCentralSeries_length_eq_nilpotencyClass]
   -- Porting note: Lean needs to be told that predicates are decidable
   refine @Nat.find_min' _ (Classical.decPred _) _ _ ?_
   refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)
-  apply eq_bot_iff.mpr
+  rw [eq_bot_iff]
   apply le_trans (lowerCentralSeries.map f _)
   simp only [lowerCentralSeries_nilpotencyClass, le_bot_iff]
 #align nilpotency_class_le_of_ker_le_center nilpotencyClass_le_of_ker_le_center
@@ -553,11 +551,11 @@ theorem nilpotent_of_surjective {G' : Type*} [Group G'] [h : IsNilpotent G] (f :
 nilpotent group is less or equal the nilpotency class of the domain -/
 theorem nilpotencyClass_le_of_surjective {G' : Type*} [Group G'] (f : G →* G')
     (hf : Function.Surjective f) [h : IsNilpotent G] :
-    @Group.nilpotencyClass G' _ (nilpotent_of_surjective _ hf) ≤ Group.nilpotencyClass G := by
+    Group.nilpotencyClass (hG := nilpotent_of_surjective _ hf) ≤ Group.nilpotencyClass G := by
   -- Porting note: Lean needs to be told that predicates are decidable
   refine @Nat.find_mono _ _ (Classical.decPred _) (Classical.decPred _) ?_ _ _
   intro n hn
-  apply eq_top_iff.mpr
+  rw [eq_top_iff]
   calc
     ⊤ = f.range := symm (f.range_top_of_surjective hf)
     _ = Subgroup.map f ⊤ := (MonoidHom.range_eq_map _)
@@ -624,7 +622,7 @@ theorem nilpotencyClass_quotient_center [hH : IsNilpotent G] :
   · suffices Group.nilpotencyClass (G ⧸ center G) = n by simpa
     apply le_antisymm
     · apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp
-      apply @comap_injective G _ _ _ (mk' (center G)) (surjective_quot_mk _)
+      apply comap_injective (f := (mk' (center G))) (surjective_quot_mk _)
       rw [comap_upperCentralSeries_quotient_center, comap_top, ← hn]
       exact upperCentralSeries_nilpotencyClass
     · apply le_of_add_le_add_right
@@ -688,8 +686,7 @@ instance (priority := 100) CommGroup.isNilpotent {G : Type*} [CommGroup G] : IsN
 /-- Abelian groups have nilpotency class at most one -/
 theorem CommGroup.nilpotencyClass_le_one {G : Type*} [CommGroup G] :
     Group.nilpotencyClass G ≤ 1 := by
-  apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp
-  rw [upperCentralSeries_one]
+  rw [← upperCentralSeries_eq_top_iff_nilpotencyClass_le, upperCentralSeries_one]
   apply CommGroup.center_eq_top
 #align comm_group.nilpotency_class_le_one CommGroup.nilpotencyClass_le_one
 
@@ -800,9 +797,8 @@ instance isNilpotent_pi [Finite η] [∀ i, IsNilpotent (Gs i)] : IsNilpotent (
   refine' ⟨Finset.univ.sup fun i => Group.nilpotencyClass (Gs i), _⟩
   rw [lowerCentralSeries_pi_of_finite, pi_eq_bot_iff]
   intro i
-  apply lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr
-  exact
-    @Finset.le_sup _ _ _ _ Finset.univ (fun i => Group.nilpotencyClass (Gs i)) _ (Finset.mem_univ i)
+  rw [lowerCentralSeries_eq_bot_iff_nilpotencyClass_le]
+  exact Finset.le_sup (f := fun i => Group.nilpotencyClass (Gs i)) (Finset.mem_univ i)
 #align is_nilpotent_pi isNilpotent_pi
 
 /-- The nilpotency class of an n-ary product is the sup of the nilpotency classes of the factors -/