chore: fix grammar 3/3 (#5003)

Part 3 of #5001

Mathlib/Order/BooleanAlgebra.lean

@@ -90,7 +90,7 @@ class GeneralizedBooleanAlgebra (α : Type u) extends DistribLattice α, SDiff 
   inf_inf_sdiff : ∀ a b : α, a ⊓ b ⊓ a \ b = ⊥
 #align generalized_boolean_algebra GeneralizedBooleanAlgebra
 
--- We might want a `IsCompl_of` predicate (for relative complements) generalizing `IsCompl`,
+-- We might want an `IsCompl_of` predicate (for relative complements) generalizing `IsCompl`,
 -- however we'd need another type class for lattices with bot, and all the API for that.
 section GeneralizedBooleanAlgebra
 

Mathlib/Order/CompleteLattice.lean

@@ -1330,7 +1330,7 @@ theorem iSup_and' {p q : Prop} {s : p → q → α} :
   Eq.symm iSup_and
 #align supr_and' iSup_and'
 
-/-- The symmetric case of `iInf_and`, useful for rewriting into a infimum over a conjunction -/
+/-- The symmetric case of `iInf_and`, useful for rewriting into an infimum over a conjunction -/
 theorem iInf_and' {p q : Prop} {s : p → q → α} :
     (⨅ (h₁ : p) (h₂ : q), s h₁ h₂) = ⨅ h : p ∧ q, s h.1 h.2 :=
   Eq.symm iInf_and

Mathlib/Order/Extension/Well.lean

@@ -54,7 +54,7 @@ necessarily injective but respects the order `r`; the other map is the identity
 chosen well-order on `α`), which is injective but doesn't respect `r`.
 
 By taking the lexicographic product of the two, we get both properties, so we can pull it back and
-get an well-order that extend our original order `r`. Another way to view this is that we choose an
+get a well-order that extend our original order `r`. Another way to view this is that we choose an
 arbitrary well-order to serve as a tiebreak between two elements of same rank.
 -/
 noncomputable def wellOrderExtension : LinearOrder α :=

Mathlib/Order/Heyting/Basic.lean

@@ -15,7 +15,7 @@ import Mathlib.Order.PropInstances
 
 This file defines Heyting, co-Heyting and bi-Heyting algebras.
 
-An Heyting algebra is a bounded distributive lattice with an implication operation `⇨` such that
+A Heyting algebra is a bounded distributive lattice with an implication operation `⇨` such that
 `a ≤ b ⇨ c ↔ a ⊓ b ≤ c`. It also comes with a pseudo-complement `ᶜ`, such that `aᶜ = a ⇨ ⊥`.
 
 Co-Heyting algebras are dual to Heyting algebras. They have a difference `\` and a negation `￢`

Mathlib/Order/Heyting/Regular.lean

@@ -13,7 +13,7 @@ import Mathlib.Order.GaloisConnection
 /-!
 # Heyting regular elements
 
-This file defines Heyting regular elements, elements of an Heyting algebra that are their own double
+This file defines Heyting regular elements, elements of a Heyting algebra that are their own double
 complement, and proves that they form a boolean algebra.
 
 From a logic standpoint, this means that we can perform classical logic within intuitionistic logic
@@ -41,7 +41,7 @@ section HasCompl
 
 variable [HasCompl α] {a : α}
 
-/-- An element of an Heyting algebra is regular if its double complement is itself. -/
+/-- An element of a Heyting algebra is regular if its double complement is itself. -/
 def IsRegular (a : α) : Prop :=
   aᶜᶜ = a
 #align heyting.is_regular Heyting.IsRegular

Mathlib/Order/Hom/Basic.lean

@@ -54,7 +54,7 @@ because the more bundled version usually does not work with dot notation.
 * `Pi.evalOrderHom`: evaluation of a function at a point `Function.eval i` as a bundled
   monotone map;
 * `OrderHom.coeFnHom`: coercion to function as a bundled monotone map;
-* `OrderHom.apply`: application of a `OrderHom` at a point as a bundled monotone map;
+* `OrderHom.apply`: application of an `OrderHom` at a point as a bundled monotone map;
 * `OrderHom.pi`: combine a family of monotone maps `f i : α →o π i` into a monotone map
   `α →o Π i, π i`;
 * `OrderHom.piIso`: order isomorphism between `α →o Π i, π i` and `Π i, α →o π i`;
@@ -381,7 +381,7 @@ theorem id_comp (f : α →o β) : comp id f = f := by
   rfl
 #align order_hom.id_comp OrderHom.id_comp
 
-/-- Constant function bundled as a `OrderHom`. -/
+/-- Constant function bundled as an `OrderHom`. -/
 @[simps (config := { fullyApplied := false })]
 def const (α : Type _) [Preorder α] {β : Type _} [Preorder β] : β →o α →o β where
   toFun b := ⟨Function.const α b, fun _ _ _ => le_rfl⟩
@@ -426,7 +426,7 @@ def prodₘ : (α →o β) →o (α →o γ) →o α →o β × γ :=
 #align order_hom.prodₘ OrderHom.prodₘ
 #align order_hom.prodₘ_coe_coe_coe OrderHom.prodₘ_coe_coe_coe
 
-/-- Diagonal embedding of `α` into `α × α` as a `OrderHom`. -/
+/-- Diagonal embedding of `α` into `α × α` as an `OrderHom`. -/
 @[simps!]
 def diag : α →o α × α :=
   id.prod id
@@ -440,14 +440,14 @@ def onDiag (f : α →o α →o β) : α →o β :=
 #align order_hom.on_diag OrderHom.onDiag
 #align order_hom.on_diag_coe OrderHom.onDiag_coe
 
-/-- `Prod.fst` as a `OrderHom`. -/
+/-- `Prod.fst` as an `OrderHom`. -/
 @[simps]
 def fst : α × β →o α :=
   ⟨Prod.fst, fun _ _ h => h.1⟩
 #align order_hom.fst OrderHom.fst
 #align order_hom.fst_coe OrderHom.fst_coe
 
-/-- `Prod.snd` as a `OrderHom`. -/
+/-- `Prod.snd` as an `OrderHom`. -/
 @[simps]
 def snd : α × β →o β :=
   ⟨Prod.snd, fun _ _ h => h.2⟩
@@ -483,7 +483,7 @@ def prodIso : (α →o β × γ) ≃o (α →o β) × (α →o γ) where
 #align order_hom.prod_iso_apply OrderHom.prodIso_apply
 #align order_hom.prod_iso_symm_apply OrderHom.prodIso_symm_apply
 
-/-- `Prod.map` of two `OrderHom`s as a `OrderHom`. -/
+/-- `Prod.map` of two `OrderHom`s as an `OrderHom`. -/
 @[simps]
 def prodMap (f : α →o β) (g : γ →o δ) : α × γ →o β × δ :=
   ⟨Prod.map f g, fun _ _ h => ⟨f.mono h.1, g.mono h.2⟩⟩
@@ -492,7 +492,7 @@ def prodMap (f : α →o β) (g : γ →o δ) : α × γ →o β × δ :=
 
 variable {ι : Type _} {π : ι → Type _} [∀ i, Preorder (π i)]
 
-/-- Evaluation of an unbundled function at a point (`Function.eval`) as a `OrderHom`. -/
+/-- Evaluation of an unbundled function at a point (`Function.eval`) as an `OrderHom`. -/
 @[simps (config := { fullyApplied := false })]
 def _root_.Pi.evalOrderHom (i : ι) : (∀ j, π j) →o π i :=
   ⟨Function.eval i, Function.monotone_eval i⟩
@@ -735,7 +735,7 @@ def subtype (p : α → Prop) : Subtype p ↪o α :=
 #align order_embedding.subtype OrderEmbedding.subtype
 #align order_embedding.subtype_apply OrderEmbedding.subtype_apply
 
-/-- Convert an `OrderEmbedding` to a `OrderHom`. -/
+/-- Convert an `OrderEmbedding` to an `OrderHom`. -/
 @[simps (config := { fullyApplied := false })]
 def toOrderHom {X Y : Type _} [Preorder X] [Preorder Y] (f : X ↪o Y) : X →o Y where
   toFun := f

Mathlib/Order/Interval.lean

@@ -454,7 +454,7 @@ variable [PartialOrder α] [PartialOrder β] {s t : Interval α} {a b : α}
 instance partialOrder : PartialOrder (Interval α) :=
   WithBot.partialOrder
 
-/-- Consider a interval `[a, b]` as the set `[a, b]`. -/
+/-- Consider an interval `[a, b]` as the set `[a, b]`. -/
 def coeHom : Interval α ↪o Set α :=
   OrderEmbedding.ofMapLEIff
     (fun s =>

Mathlib/Order/Iterate.lean

@@ -239,7 +239,7 @@ theorem monotone_iterate_of_le_map (hf : Monotone f) (hx : x ≤ f x) : Monotone
 #align monotone.monotone_iterate_of_le_map Monotone.monotone_iterate_of_le_map
 
 /-- If `f` is a monotone map and `f x ≤ x` at some point `x`, then the iterates `f^[n] x` form
-a antitone sequence. -/
+an antitone sequence. -/
 theorem antitone_iterate_of_map_le (hf : Monotone f) (hx : f x ≤ x) : Antitone fun n => (f^[n]) x :=
   hf.dual.monotone_iterate_of_le_map hx
 #align monotone.antitone_iterate_of_map_le Monotone.antitone_iterate_of_map_le

Mathlib/Order/Lattice.lean

@@ -1211,25 +1211,25 @@ end Antitone
 
 namespace AntitoneOn
 
-/-- Pointwise supremum of two antitone functions is a antitone function. -/
+/-- Pointwise supremum of two antitone functions is an antitone function. -/
 protected theorem sup [Preorder α] [SemilatticeSup β] {f g : α → β} {s : Set α}
     (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (f ⊔ g) s :=
   fun _ hx _ hy h => sup_le_sup (hf hx hy h) (hg hx hy h)
 #align antitone_on.sup AntitoneOn.sup
 
-/-- Pointwise infimum of two antitone functions is a antitone function. -/
+/-- Pointwise infimum of two antitone functions is an antitone function. -/
 protected theorem inf [Preorder α] [SemilatticeInf β] {f g : α → β} {s : Set α}
     (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (f ⊓ g) s :=
   (hf.dual.sup hg.dual).dual
 #align antitone_on.inf AntitoneOn.inf
 
-/-- Pointwise maximum of two antitone functions is a antitone function. -/
+/-- Pointwise maximum of two antitone functions is an antitone function. -/
 protected theorem max [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s)
     (hg : AntitoneOn g s) : AntitoneOn (fun x => max (f x) (g x)) s :=
   hf.sup hg
 #align antitone_on.max AntitoneOn.max
 
-/-- Pointwise minimum of two antitone functions is a antitone function. -/
+/-- Pointwise minimum of two antitone functions is an antitone function. -/
 protected theorem min [Preorder α] [LinearOrder β] {f g : α → β} {s : Set α} (hf : AntitoneOn f s)
     (hg : AntitoneOn g s) : AntitoneOn (fun x => min (f x) (g x)) s :=
   hf.inf hg

Mathlib/Order/OmegaCompletePartialOrder.lean

@@ -185,7 +185,7 @@ variable {α : Type u} {β : Type v} {γ : Type _}
 
 variable [OmegaCompletePartialOrder α]
 
-/-- Transfer a `OmegaCompletePartialOrder` on `β` to a `OmegaCompletePartialOrder` on `α`
+/-- Transfer an `OmegaCompletePartialOrder` on `β` to an `OmegaCompletePartialOrder` on `α`
 using a strictly monotone function `f : β →o α`, a definition of ωSup and a proof that `f` is
 continuous with regard to the provided `ωSup` and the ωCPO on `α`. -/
 @[reducible]
@@ -581,7 +581,7 @@ attribute [nolint docBlame] ContinuousHom.toOrderHom
 infixr:25 " →𝒄 " => ContinuousHom
 -- Input: \r\MIc
 
-/-! todo: should we make this a OrderHomClass instead of a CoeFun? -/
+/-! todo: should we make this an OrderHomClass instead of a CoeFun? -/
 instance : CoeFun (α →𝒄 β) fun _ => α → β :=
   ⟨fun f => f.toOrderHom.toFun⟩
 

Mathlib/Order/OrdContinuous.lean

@@ -215,7 +215,7 @@ theorem lt_iff (hf : RightOrdContinuous f) (h : Injective f) {x y} : f x < f y 
 
 variable (f)
 
-/-- Convert an injective left order continuous function to a `OrderEmbedding`. -/
+/-- Convert an injective left order continuous function to an `OrderEmbedding`. -/
 def toOrderEmbedding (hf : RightOrdContinuous f) (h : Injective f) : α ↪o β :=
   ⟨⟨f, h⟩, hf.le_iff h⟩
 #align right_ord_continuous.to_order_embedding RightOrdContinuous.toOrderEmbedding

Mathlib/Order/PrimeIdeal.lean

@@ -19,7 +19,7 @@ import Mathlib.Order.PFilter
 Throughout this file, `P` is at least a preorder, but some sections require more
 structure, such as a bottom element, a top element, or a join-semilattice structure.
 
-- `Order.Ideal.PrimePair`: A pair of an `Order.Ideal` and a `Order.PFilter` which form a partition
+- `Order.Ideal.PrimePair`: A pair of an `Order.Ideal` and an `Order.PFilter` which form a partition
   of `P`.  This is useful as giving the data of a prime ideal is the same as giving the data of a
   prime filter.
 - `Order.Ideal.IsPrime`: a predicate for prime ideals. Dual to the notion of a prime filter.
@@ -44,7 +44,7 @@ variable {P : Type _}
 
 namespace Ideal
 
-/-- A pair of an `Order.Ideal` and a `Order.PFilter` which form a partition of `P`.
+/-- A pair of an `Order.Ideal` and an `Order.PFilter` which form a partition of `P`.
 -/
 -- porting note: no attr @[nolint has_nonempty_instance]
 structure PrimePair (P : Type _) [Preorder P] where

Mathlib/Order/RelClasses.lean

@@ -184,7 +184,7 @@ theorem extensional_of_trichotomous_of_irrefl (r : α → α → Prop) [IsTricho
     <| irrefl b
 #align extensional_of_trichotomous_of_irrefl extensional_of_trichotomous_of_irrefl
 
-/-- Construct a partial order from a `isStrictOrder` relation.
+/-- Construct a partial order from an `isStrictOrder` relation.
 
 See note [reducible non-instances]. -/
 @[reducible]
@@ -469,7 +469,7 @@ noncomputable def IsWellOrder.linearOrder (r : α → α → Prop) [IsWellOrder
   linearOrderOfSTO r
 #align is_well_order.linear_order IsWellOrder.linearOrder
 
-/-- Derive a `WellFoundedRelation` instance from a `IsWellOrder` instance. -/
+/-- Derive a `WellFoundedRelation` instance from an `IsWellOrder` instance. -/
 def IsWellOrder.toHasWellFounded [LT α] [hwo : IsWellOrder α (· < ·)] : WellFoundedRelation α where
   rel := (· < ·)
   wf := hwo.wf

Mathlib/Order/RelIso/Basic.lean

@@ -493,7 +493,7 @@ alias wellFounded_liftOn₂'_iff ↔ WellFounded.of_quotient_liftOn₂' WellFoun
 
 namespace RelEmbedding
 
-/-- To define an relation embedding from an antisymmetric relation `r` to a reflexive relation `s`
+/-- To define a relation embedding from an antisymmetric relation `r` to a reflexive relation `s`
 it suffices to give a function together with a proof that it satisfies `s (f a) (f b) ↔ r a b`.
 -/
 def ofMapRelIff (f : α → β) [IsAntisymm α r] [IsRefl β s] (hf : ∀ a b, s (f a) (f b) ↔ r a b) :
@@ -629,7 +629,7 @@ infixl:25 " ≃r " => RelIso
 
 namespace RelIso
 
-/-- Convert an `RelIso` to a `RelEmbedding`. This function is also available as a coercion
+/-- Convert a `RelIso` to a `RelEmbedding`. This function is also available as a coercion
 but often it is easier to write `f.toRelEmbedding` than to write explicitly `r` and `s`
 in the target type. -/
 def toRelEmbedding (f : r ≃r s) : r ↪r s :=

Mathlib/Order/UpperLower/Basic.lean

@@ -29,8 +29,8 @@ This file defines upper and lower sets in an order.
 * `lowerClosure`: The least lower set containing a set.
 * `UpperSet.Ici`: Principal upper set. `Set.Ici` as an upper set.
 * `UpperSet.Ioi`: Strict principal upper set. `Set.Ioi` as an upper set.
-* `LowerSet.Iic`: Principal lower set. `Set.Iic` as an lower set.
-* `LowerSet.Iio`: Strict principal lower set. `Set.Iio` as an lower set.
+* `LowerSet.Iic`: Principal lower set. `Set.Iic` as a lower set.
+* `LowerSet.Iio`: Strict principal lower set. `Set.Iio` as a lower set.
 
 ## Notation
 

Mathlib/Order/Zorn.lean

@@ -36,7 +36,7 @@ walkthrough:
 1. Know what relation on which type/set you're looking for. See Variants above. You can discharge
   some conditions to Zorn's lemma directly using a `_nonempty` variant.
 2. Write down the definition of your type/set, put a `suffices : ∃ m, ∀ a, m ≺ a → a ≺ m, { ... },`
-  (or whatever you actually need) followed by a `apply some_version_of_zorn`.
+  (or whatever you actually need) followed by an `apply some_version_of_zorn`.
 3. Fill in the details. This is where you start talking about chains.
 
 A typical proof using Zorn could look like this (TODO: update to mathlib4)

Mathlib/Order/ZornAtoms.lean

@@ -39,7 +39,7 @@ theorem IsCoatomic.of_isChain_bounded {α : Type _} [PartialOrder α] [OrderTop
   exact hyz.ne' (hy' z ⟨hxy.trans hyz.le, hz⟩ hyz.le)
 #align is_coatomic.of_is_chain_bounded IsCoatomic.of_isChain_bounded
 
-/-- **Zorn's lemma**: A partial order is atomic if every nonempty chain `c`, `⊥ ∉ c`, has an lower
+/-- **Zorn's lemma**: A partial order is atomic if every nonempty chain `c`, `⊥ ∉ c`, has a lower
 bound not equal to `⊥`. -/
 theorem IsAtomic.of_isChain_bounded {α : Type _} [PartialOrder α] [OrderBot α]
     (h :

Mathlib/Probability/Kernel/Basic.lean

@@ -28,7 +28,7 @@ Classes of kernels:
   if for all `a : α`, `k a` is a probability measure.
 * `ProbabilityTheory.IsFiniteKernel κ`: a kernel from `α` to `β` is said to be finite if there
   exists `C : ℝ≥0∞` such that `C < ∞` and for all `a : α`, `κ a univ ≤ C`. This implies in
-  particular that all measures in the image of `κ` are finite, but is stronger since it requires an
+  particular that all measures in the image of `κ` are finite, but is stronger since it requires a
   uniform bound. This stronger condition is necessary to ensure that the composition of two finite
   kernels is finite.
 * `ProbabilityTheory.IsSFiniteKernel κ`: a kernel is called s-finite if it is a countable

Mathlib/RepresentationTheory/Action.lean

@@ -119,7 +119,7 @@ namespace Hom
 attribute [reassoc] comm
 attribute [local simp] comm comm_assoc
 
-/-- The identity morphism on a `Action V G`. -/
+/-- The identity morphism on an `Action V G`. -/
 @[simps]
 def id (M : Action V G) : Action.Hom M M where hom := 𝟙 M.V
 set_option linter.uppercaseLean3 false in

Mathlib/RepresentationTheory/Basic.lean

@@ -44,7 +44,7 @@ section
 
 variable (k G V : Type _) [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V]
 
-/-- A representation of `G` on the `k`-module `V` is an homomorphism `G →* (V →ₗ[k] V)`.
+/-- A representation of `G` on the `k`-module `V` is a homomorphism `G →* (V →ₗ[k] V)`.
 -/
 abbrev Representation :=
   G →* V →ₗ[k] V

Mathlib/RingTheory/Algebraic.lean

@@ -239,7 +239,7 @@ theorem isAlgebraic_of_larger_base_of_injective (hinj : Function.Injective (alge
   _root_.isAlgebraic_of_larger_base_of_injective hinj (A_alg x)
 #align algebra.is_algebraic_of_larger_base_of_injective Algebra.isAlgebraic_of_larger_base_of_injective
 
-/-- If x is a algebraic over K, then x is algebraic over L when L is an extension of K -/
+/-- If x is algebraic over K, then x is algebraic over L when L is an extension of K -/
 theorem _root_.isAlgebraic_of_larger_base {x : A} (A_alg : _root_.IsAlgebraic K x) :
     _root_.IsAlgebraic L x :=
   _root_.isAlgebraic_of_larger_base_of_injective (algebraMap K L).injective A_alg

Mathlib/RingTheory/Artinian.lean

@@ -27,7 +27,7 @@ itself, or simply Artinian if it is both left and right Artinian.
 
 Let `R` be a ring and let `M` and `P` be `R`-modules. Let `N` be an `R`-submodule of `M`.
 
-* `IsArtinian R M` is the proposition that `M` is a Artinian `R`-module. It is a class,
+* `IsArtinian R M` is the proposition that `M` is an Artinian `R`-module. It is a class,
   implemented as the predicate that the `<` relation on submodules is well founded.
 * `IsArtinianRing R` is the proposition that `R` is a left Artinian ring.
 
@@ -216,7 +216,7 @@ theorem induction {P : Submodule R M → Prop} (hgt : ∀ I, (∀ J < I, P J) 
   (wellFounded_submodule_lt R M).recursion I hgt
 #align is_artinian.induction IsArtinian.induction
 
-/-- For any endomorphism of a Artinian module, there is some nontrivial iterate
+/-- For any endomorphism of an Artinian module, there is some nontrivial iterate
 with disjoint kernel and range. -/
 theorem exists_endomorphism_iterate_ker_sup_range_eq_top (f : M →ₗ[R] M) :
     ∃ n : ℕ, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊔ LinearMap.range (f ^ n) = ⊤ := by

Mathlib/RingTheory/Derivation/Basic.lean

@@ -23,7 +23,7 @@ This file defines derivation. A derivation `D` from the `R`-algebra `A` to the `
   and the composition is bilinear.
 
 See `ring_theory.derivation.lie` for
-- `derivation.lie_algebra`: The `R`-derivations from `A` to `A` form an lie algebra over `R`.
+- `derivation.lie_algebra`: The `R`-derivations from `A` to `A` form a lie algebra over `R`.
 
 and `ring_theory.derivation.to_square_zero` for
 - `derivation_to_square_zero_equiv_lift`: The `R`-derivations from `A` into a square-zero ideal `I`

Mathlib/RingTheory/Derivation/ToSquareZero.lean

@@ -49,7 +49,7 @@ theorem diffToIdealOfQuotientCompEq_apply (f₁ f₂ : A →ₐ[R] B)
 variable [Algebra A B] [IsScalarTower R A B]
 
 /-- Given a tower of algebras `R → A → B`, and a square-zero `I : Ideal B`, each lift `A →ₐ[R] B`
-of the canonical map `A →ₐ[R] B ⧸ I` corresponds to a `R`-derivation from `A` to `I`. -/
+of the canonical map `A →ₐ[R] B ⧸ I` corresponds to an `R`-derivation from `A` to `I`. -/
 def derivationToSquareZeroOfLift (f : A →ₐ[R] B)
     (e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)) :
     Derivation R A I := by

Mathlib/RingTheory/FreeCommRing.lean

@@ -136,7 +136,7 @@ private def liftToMultiset : (α → R) ≃ (Multiplicative (Multiset α) →* R
       erw [← Multiset.map_map (fun x => F' x) (fun x => {x}), ← AddMonoidHom.map_multiset_sum]
       exact F.congr_arg (Multiset.sum_map_singleton x')
 
-/-- Lift a map `α → R` to a additive group homomorphism `FreeCommRing α → R`. -/
+/-- Lift a map `α → R` to an additive group homomorphism `FreeCommRing α → R`. -/
 def lift : (α → R) ≃ (FreeCommRing α →+* R) :=
   Equiv.trans liftToMultiset FreeAbelianGroup.liftMonoid
 #align free_comm_ring.lift FreeCommRing.lift