doc: fix typos (leanprover-community#10171)

Fix minor typos in the following files:

- [x] `GroupTheory/Nilpotent.lean`
- [x] `GroupTheory/PushoutI.lean`
- [x] `SetTheory/Cardinal/ENat.lean`
- [x] `SetTheory/Cardinal/Subfield.lean`
- [x] `RepresentationTheory/Action/Basic.lean`
- [x] `RepresentationTheory/Action/Limits.lean`
- [x] `Logic/Function/OfArity.lean`

Author: pitmonticone

Mathlib/GroupTheory/Nilpotent.lean

@@ -53,7 +53,7 @@ subgroup `G` of `G`, and `⊥` denotes the trivial subgroup `{1}`.
 * `nilpotent_iff_finite_descending_central_series` : `G` is nilpotent iff some descending central
     series reaches `⊥`.
 * `nilpotent_iff_lower` : `G` is nilpotent iff the lower central series reaches `⊥`.
-* The `nilpotency_class` can likeways be obtained from these equivalent
+* The `nilpotency_class` can likewise be obtained from these equivalent
   definitions, see `least_ascending_central_series_length_eq_nilpotencyClass`,
   `least_descending_central_series_length_eq_nilpotencyClass` and
   `lowerCentralSeries_length_eq_nilpotencyClass`.
@@ -887,7 +887,7 @@ theorem isNilpotent_of_product_of_sylow_group
 #align is_nilpotent_of_product_of_sylow_group isNilpotent_of_product_of_sylow_group
 
 /-- A finite group is nilpotent iff the normalizer condition holds, and iff all maximal groups are
-normal and iff all sylow groups are normal and iff the group is the direct product of its sylow
+normal and iff all Sylow groups are normal and iff the group is the direct product of its Sylow
 groups. -/
 theorem isNilpotent_of_finite_tFAE :
     List.TFAE

Mathlib/GroupTheory/PushoutI.lean

@@ -143,7 +143,7 @@ theorem hom_ext_nonempty [hn : Nonempty ι]
       rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]
 
 /-- The equivalence that is part of the universal property of the pushout. A hom out of
-the pushout is just a morphism out of all groups in the pushout that satsifies a commutativity
+the pushout is just a morphism out of all groups in the pushout that satisfies a commutativity
 condition. -/
 @[simps]
 def homEquiv :

Mathlib/Logic/Function/OfArity.lean

@@ -10,7 +10,7 @@ import Mathlib.Mathport.Rename
 /-! # Function types of a given arity
 
 This provides `FunctionOfArity`, such that `OfArity α β 2 = α → α → β`.
-Note that it is often preferrable to use `(Fin n → α) → β` in place of `OfArity n α β`.
+Note that it is often preferable to use `(Fin n → α) → β` in place of `OfArity n α β`.
 
 ## Main definitions
 

Mathlib/RepresentationTheory/Action/Basic.lean

@@ -176,7 +176,7 @@ set_option linter.uppercaseLean3 false in
 
 namespace FunctorCategoryEquivalence
 
-/-- Auxilliary definition for `functorCategoryEquivalence`. -/
+/-- Auxiliary definition for `functorCategoryEquivalence`. -/
 @[simps]
 def functor : Action V G ⥤ SingleObj G ⥤ V where
   obj M :=
@@ -190,7 +190,7 @@ def functor : Action V G ⥤ SingleObj G ⥤ V where
 set_option linter.uppercaseLean3 false in
 #align Action.functor_category_equivalence.functor Action.FunctorCategoryEquivalence.functor
 
-/-- Auxilliary definition for `functorCategoryEquivalence`. -/
+/-- Auxiliary definition for `functorCategoryEquivalence`. -/
 @[simps]
 def inverse : (SingleObj G ⥤ V) ⥤ Action V G where
   obj F :=
@@ -205,14 +205,14 @@ def inverse : (SingleObj G ⥤ V) ⥤ Action V G where
 set_option linter.uppercaseLean3 false in
 #align Action.functor_category_equivalence.inverse Action.FunctorCategoryEquivalence.inverse
 
-/-- Auxilliary definition for `functorCategoryEquivalence`. -/
+/-- Auxiliary definition for `functorCategoryEquivalence`. -/
 @[simps!]
 def unitIso : 𝟭 (Action V G) ≅ functor ⋙ inverse :=
   NatIso.ofComponents fun M => mkIso (Iso.refl _)
 set_option linter.uppercaseLean3 false in
 #align Action.functor_category_equivalence.unit_iso Action.FunctorCategoryEquivalence.unitIso
 
-/-- Auxilliary definition for `functorCategoryEquivalence`. -/
+/-- Auxiliary definition for `functorCategoryEquivalence`. -/
 @[simps!]
 def counitIso : inverse ⋙ functor ≅ 𝟭 (SingleObj G ⥤ V) :=
   NatIso.ofComponents fun M => NatIso.ofComponents fun X => Iso.refl _

Mathlib/RepresentationTheory/Action/Limits.lean

@@ -334,7 +334,7 @@ end Linear
 
 section Abelian
 
-/-- Auxilliary construction for the `Abelian (Action V G)` instance. -/
+/-- Auxiliary construction for the `Abelian (Action V G)` instance. -/
 def abelianAux : Action V G ≌ ULift.{u} (SingleObj G) ⥤ V :=
   (functorCategoryEquivalence V G).trans (Equivalence.congrLeft ULift.equivalence)
 set_option linter.uppercaseLean3 false in

Mathlib/SetTheory/Cardinal/ENat.lean

@@ -11,7 +11,7 @@ import Mathlib.Algebra.Order.Hom.Ring
 
 In this file we define a coercion `Cardinal.ofENat : ℕ∞ → Cardinal`
 and a projection `Cardinal.toENat : Cardinal →+*o ℕ∞`.
-We also prove basic theorems about these definitons.
+We also prove basic theorems about these definitions.
 
 ## Implementation notes
 

Mathlib/SetTheory/Cardinal/Subfield.lean

@@ -14,7 +14,7 @@ import Mathlib.Tactic.FinCases
 generated by a set is bounded by the cardinality of the set unless it is finite.
 
 The method used to prove this (via `WType`) can be easily generalized to other algebraic
-structures, but those cardinalites can usually be obtained by other means, using some
+structures, but those cardinalities can usually be obtained by other means, using some
 explicit universal objects.
 
 -/