doc: fix a/an articles (4/4) (#32293)

harahu · harahu · commit 2ddd611e3a7c · 2025-12-01T21:50:44.000Z
Found and fixed by a script (due to Codex). Then manually reviewed.
diff --git a/Mathlib/Tactic/CC/Addition.lean b/Mathlib/Tactic/CC/Addition.lean
@@ -9,7 +9,7 @@ public meta import Mathlib.Data.Option.Defs
 public meta import Mathlib.Tactic.CC.MkProof
 
 /-!
-# Process when an new equation is added to a congruence closure
+# Process when a new equation is added to a congruence closure
 -/
 
 public meta section
@@ -505,7 +505,7 @@ def setACVar (e : Expr) : CCM Unit := do
     let newRootEntry := { rootEntry with acVar := some e }
     modify fun ccs => { ccs with entries := ccs.entries.insert eRoot newRootEntry }
 
-/-- If `e` isn't an AC variable, set `e` as an new AC variable. -/
+/-- If `e` isn't an AC variable, set `e` as a new AC variable. -/
 def internalizeACVar (e : Expr) : CCM Bool := do
   let ccs ← get
   if ccs.acEntries.contains e then return false
@@ -963,7 +963,7 @@ partial def processSubsingletonElem (e : Expr) : CCM Unit := do
       { ccs with
         subsingletonReprs := ccs.subsingletonReprs.insert typeRoot e }
 
-/-- Add an new entry for `e` to the congruence closure. -/
+/-- Add a new entry for `e` to the congruence closure. -/
 partial def mkEntry (e : Expr) (interpreted : Bool) : CCM Unit := do
   if (← getEntry e).isSome then return
   let constructor ← isConstructorApp e
diff --git a/Mathlib/Tactic/DeriveEncodable.lean b/Mathlib/Tactic/DeriveEncodable.lean
@@ -36,7 +36,7 @@ inductive S : Type where
   | nat (n : ℕ)
   | cons (a b : S)
 ```
-We start by constructing a equivalence `S ≃ ℕ` using the `Nat.pair` function.
+We start by constructing an equivalence `S ≃ ℕ` using the `Nat.pair` function.
 
 Here is an example of how this module constructs an encoding.
 
diff --git a/Mathlib/Tactic/FieldSimp.lean b/Mathlib/Tactic/FieldSimp.lean
@@ -448,7 +448,7 @@ partial def normalize (disch : ∀ {u : Level} (type : Q(Sort u)), MetaM Q($type
     let ⟨G, pf_y⟩ := ← Sign.div iM y₁ y₂ g₁ g₂
     pure ⟨q($y₁ / $y₂), ⟨G, q(Eq.trans (congr_arg₂ HDiv.hDiv $pf₁_sgn $pf₂_sgn) $pf_y)⟩,
       qNF.div l₁ l₂, q(NF.div_eq_eval $pf₁ $pf₂ $pf)⟩
-  /- normalize a inversion: `y⁻¹` -/
+  /- normalize an inversion: `y⁻¹` -/
   | ~q($y⁻¹) =>
     let ⟨y', ⟨g, pf_sgn⟩, l, pf⟩ ← normalize disch iM y
     let pf_y ← Sign.inv iM y' g
diff --git a/Mathlib/Tactic/GCongr/Core.lean b/Mathlib/Tactic/GCongr/Core.lean
@@ -16,7 +16,7 @@ import all Lean.Meta.Tactic.Apply
 # The `gcongr` ("generalized congruence") tactic
 
 The `gcongr` tactic applies "generalized congruence" rules, reducing a relational goal
-between a LHS and RHS matching the same pattern to relational subgoals between the differing
+between an LHS and RHS matching the same pattern to relational subgoals between the differing
 inputs to the pattern.  For example,
 ```
 example {a b x c d : ℝ} (h1 : a + 1 ≤ b + 1) (h2 : c + 2 ≤ d + 2) :
@@ -25,7 +25,7 @@ example {a b x c d : ℝ} (h1 : a + 1 ≤ b + 1) (h2 : c + 2 ≤ d + 2) :
   · linarith
   · linarith
 ```
-This example has the goal of proving the relation `≤` between a LHS and RHS both of the pattern
+This example has the goal of proving the relation `≤` between an LHS and RHS both of the pattern
 ```
 x ^ 2 * ?_ + ?_
 ```
@@ -608,15 +608,15 @@ partial def _root_.Lean.MVarId.gcongr
       \n  attempted lemmas: {lemmas.map (·.declName)}"
 
 /-- The `gcongr` tactic applies "generalized congruence" rules, reducing a relational goal
-between a LHS and RHS.  For example,
+between an LHS and RHS.  For example,
 ```
 example {a b x c d : ℝ} (h1 : a + 1 ≤ b + 1) (h2 : c + 2 ≤ d + 2) :
     x ^ 2 * a + c ≤ x ^ 2 * b + d := by
   gcongr
   · linarith
   · linarith
 ```
-This example has the goal of proving the relation `≤` between a LHS and RHS both of the pattern
+This example has the goal of proving the relation `≤` between an LHS and RHS both of the pattern
 ```
 x ^ 2 * ?_ + ?_
 ```
diff --git a/Mathlib/Tactic/Linarith/Frontend.lean b/Mathlib/Tactic/Linarith/Frontend.lean
@@ -75,7 +75,7 @@ There are two oracles that can be used in `linarith` so far.
   large problems. You can use it with `linarith (oracle := .fourierMotzkin)`.
 
 2. **Simplex Algorithm (default).**
-  This oracle reduces the search for a unsatisfiability certificate to some Linear Programming
+  This oracle reduces the search for an unsatisfiability certificate to some Linear Programming
   problem. The problem is then solved by a standard Simplex Algorithm. We use
   [Bland's pivot rule](https://en.wikipedia.org/wiki/Bland%27s_rule) to guarantee that the algorithm
   terminates.
diff --git a/Mathlib/Tactic/TermCongr.lean b/Mathlib/Tactic/TermCongr.lean
@@ -321,7 +321,7 @@ def CongrResult.trans (res1 res2 : CongrResult) : CongrResult where
         | .eq => do mkEqTrans (← res1.eq) (← res2.eq)
         | .heq => do mkHEqTrans (← res1.heq) (← res2.heq)
 
-/-- Make a `CongrResult` from a LHS, a RHS, and a proof of an Iff, Eq, or HEq.
+/-- Make a `CongrResult` from an LHS, an RHS, and a proof of an Iff, Eq, or HEq.
 The proof is allowed to have a metavariable for its type.
 Validates the inputs and throws errors in the `pf?` function.
 
diff --git a/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean b/Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
@@ -359,7 +359,7 @@ theorem toHomeomorph_eq_coe (f : M ≃ₜ* N) : f.toHomeomorph = f :=
 
 /-- Makes a continuous multiplicative isomorphism from
 a homeomorphism which preserves multiplication. -/
-@[to_additive /-- Makes an continuous additive isomorphism from
+@[to_additive /-- Makes a continuous additive isomorphism from
 a homeomorphism which preserves addition. -/]
 def mk' (f : M ≃ₜ N) (h : ∀ x y, f (x * y) = f x * f y) : M ≃ₜ* N :=
   ⟨⟨f.toEquiv,h⟩, f.continuous_toFun, f.continuous_invFun⟩
diff --git a/Mathlib/Topology/Algebra/Group/Quotient.lean b/Mathlib/Topology/Algebra/Group/Quotient.lean
@@ -106,7 +106,7 @@ instance instT1Space [hN : IsClosed (N : Set G)] :
     T1Space (G ⧸ N) :=
   t1Space_iff.mpr hN
 
--- TODO: `IsOpen` should be an class and this should be an instance
+-- TODO: `IsOpen` should be a class and this should be an instance
 @[to_additive]
 theorem discreteTopology (hN : IsOpen (N : Set G)) :
     DiscreteTopology (G ⧸ N) :=
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean b/Mathlib/Topology/Algebra/InfiniteSum/GroupCompletion.lean
@@ -19,7 +19,7 @@ open UniformSpace.Completion
 variable {α β : Type*} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α]
 {L : SummationFilter β}
 
-/-- A function `f` has a sum in an uniform additive group `α` if and only if it has that sum in the
+/-- A function `f` has a sum in a uniform additive group `α` if and only if it has that sum in the
 completion of `α`. -/
 theorem hasSum_iff_hasSum_compl (f : β → α) (a : α) :
     HasSum (toCompl ∘ f) a L ↔ HasSum f a L := (isDenseInducing_toCompl α).hasSum_iff f a
diff --git a/Mathlib/Topology/Algebra/Module/LinearMap.lean b/Mathlib/Topology/Algebra/Module/LinearMap.lean
@@ -1218,7 +1218,7 @@ lemma IsIdempotentElem.commute_iff {f T : M →L[R] M}
 
 variable [IsTopologicalAddGroup M]
 
-/-- An idempotent operator `f` commutes with an unit operator `T` if and only if
+/-- An idempotent operator `f` commutes with a unit operator `T` if and only if
 `T (range f) = range f` and `T (ker f) = ker f`. -/
 theorem IsIdempotentElem.commute_iff_of_isUnit {f T : M →L[R] M} (hT : IsUnit T)
     (hf : IsIdempotentElem f) :
diff --git a/Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean b/Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
@@ -407,7 +407,7 @@ homomorphisms `φ j : R₁ (f j) → R₂ j` sending `B₁ (f j)` into `B₂ j`
 @[to_additive
 /-- Given two restricted products `Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁]` and
 `Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂]` of additive monoids, `RestrictedProduct.mapAlongAddMonoidHom`
-gives a additive monoid homomorphism between them. The data needed is a function `f : ι₂ → ι₁` such
+gives an additive monoid homomorphism between them. The data needed is a function `f : ι₂ → ι₁` such
 that `𝓕₂` tends to `𝓕₁` along `f`, and additive monoid homomorphisms `φ j : R₁ (f j) → R₂ j`
 sending `B₁ (f j)` into `B₂ j` for an `𝓕₂`-large set of `j`'s. -/]
 def mapAlongMonoidHom : Πʳ i, [R₁ i, B₁ i]_[𝓕₁] →* Πʳ j, [R₂ j, B₂ j]_[𝓕₂] where
diff --git a/Mathlib/Topology/Algebra/UniformRing.lean b/Mathlib/Topology/Algebra/UniformRing.lean
@@ -242,7 +242,7 @@ theorem inseparableSetoid_ring (α) [Ring α] [TopologicalSpace α] [IsTopologic
     addGroup_inseparable_iff.trans <| .trans (by rfl) (Submodule.quotientRel_def _).symm
 
 /-- Given a topological ring `α` equipped with a uniform structure that makes subtraction uniformly
-continuous, get an homeomorphism between the separated quotient of `α` and the quotient ring
+continuous, get a homeomorphism between the separated quotient of `α` and the quotient ring
 corresponding to the closure of zero. -/
 def sepQuotHomeomorphRingQuot (α) [CommRing α] [TopologicalSpace α] [IsTopologicalRing α] :
     SeparationQuotient α ≃ₜ α ⧸ (⊥ : Ideal α).closure where
diff --git a/Mathlib/Topology/Convenient/GeneratedBy.lean b/Mathlib/Topology/Convenient/GeneratedBy.lean
@@ -15,7 +15,7 @@ Let `Y` be a topological space. We introduce a type synonym
 `WithGeneratedByTopology X Y` for `Y`. This type is endowed
 with the `X`-generated topology, which is coinduced by
 all continuous maps `X i → Y`. When the bijection
-`WithGeneratedByTopology X Y ≃ Y` is an homeomorphism,
+`WithGeneratedByTopology X Y ≃ Y` is a homeomorphism,
 we say that `Y` is `X`-generated (typeclass `IsGeneratedBy X Y`).
 
 ## TODO (@joelriou)
@@ -114,7 +114,7 @@ namespace Topology
 variable (X Y) in
 /-- Given a family of topological spaces `X i`, we say that a topological space is
 `X`-generated (`IsGeneratedBy X Y`) when the topology on `Y` is the `X`-generated
-topology, i.e. when the identity is an homeomorphism
+topology, i.e. when the identity is a homeomorphism
 `WithGeneratedByTopology X Y ≃ₜ Y` (see `IsGeneratedBy.homeomorph`). -/
 @[mk_iff]
 class IsGeneratedBy : Prop where
diff --git a/Mathlib/Topology/Homotopy/Equiv.lean b/Mathlib/Topology/Homotopy/Equiv.lean
@@ -41,11 +41,11 @@ are both homotopic to corresponding identity maps.
 -/
 @[ext]
 structure HomotopyEquiv (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] where
-  /-- The forward map of an homotopy.
+  /-- The forward map of a homotopy.
 
   Do NOT use directly. Use the coercion instead. -/
   toFun : C(X, Y)
-  /-- The backward map of an homotopy.
+  /-- The backward map of a homotopy.
 
   Do NOT use `e.invFun` directly. Use the coercion of `e.symm` instead. -/
   invFun : C(Y, X)
diff --git a/Mathlib/Topology/Maps/Proper/Basic.lean b/Mathlib/Topology/Maps/Proper/Basic.lean
@@ -255,7 +255,7 @@ lemma isProperMap_iff_isClosedMap_of_inj (f_cont : Continuous f) (f_inj : f.Inje
   rw [isProperMap_iff_isClosedMap_and_compact_fibers]
   exact ⟨f_cont, h, fun y ↦ (subsingleton_singleton.preimage f_inj).isCompact⟩
 
-/-- A injective continuous and closed map is proper. -/
+/-- An injective continuous and closed map is proper. -/
 lemma isProperMap_of_isClosedMap_of_inj (f_cont : Continuous f) (f_inj : f.Injective)
     (f_closed : IsClosedMap f) : IsProperMap f :=
   (isProperMap_iff_isClosedMap_of_inj f_cont f_inj).2 f_closed
diff --git a/Mathlib/Topology/Maps/Proper/UniversallyClosed.lean b/Mathlib/Topology/Maps/Proper/UniversallyClosed.lean
@@ -49,7 +49,7 @@ theorem isProperMap_iff_isClosedMap_filter {X : Type u} {Y : Type v} [Topologica
   -- The above shows that `(y, 𝒰) = (f x, 𝒰)`, for some `x : X` such that `(x, 𝒰) ∈ F`.
     rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩
   -- We already know that `f x = y`, so to finish the proof we just have to check that `𝒰` tends
-  -- to `x`. So, for `U ∈ 𝓝 x` arbitrary, let's show that `U ∈ 𝒰`. Since `𝒰` is a ultrafilter,
+  -- to `x`. So, for `U ∈ 𝓝 x` arbitrary, let's show that `U ∈ 𝒰`. Since `𝒰` is an ultrafilter,
   -- it is enough to show that `Uᶜ` is not in `𝒰`.
     refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_notMem_iff.mp fun hUc ↦ ?_⟩
     rw [mem_closure_iff_nhds] at hx
diff --git a/Mathlib/Topology/Order/LowerUpperTopology.lean b/Mathlib/Topology/Order/LowerUpperTopology.lean
@@ -409,7 +409,7 @@ instance : ClosedIicTopology α :=
 theorem isClosed_lowerClosure (h : s.Finite) : IsClosed (lowerClosure s : Set α) :=
   IsLower.isClosed_upperClosure (α := αᵒᵈ) h
 
-/-- Every set open in the upper topology is a upper set. -/
+/-- Every set open in the upper topology is an upper set. -/
 theorem isUpperSet_of_isOpen (h : IsOpen s) : IsUpperSet s :=
   IsLower.isLowerSet_of_isOpen (α := αᵒᵈ) h
 
diff --git a/Mathlib/Topology/VectorBundle/Riemannian.lean b/Mathlib/Topology/VectorBundle/Riemannian.lean
@@ -69,7 +69,7 @@ section Trivial
 
 variable {F₁ : Type*} [NormedAddCommGroup F₁] [InnerProductSpace ℝ F₁]
 
-/-- A trivial vector bundle, in which the model fiber has a inner product,
+/-- A trivial vector bundle, in which the model fiber has an inner product,
 is a Riemannian bundle. -/
 instance : IsContinuousRiemannianBundle F₁ (Bundle.Trivial B F₁) := by
   refine ⟨fun x ↦ innerSL ℝ, ?_, fun x v w ↦ rfl⟩
