chore: fix grammar in docs (#5668)

Archive/MiuLanguage/DecisionSuf.lean

@@ -75,7 +75,7 @@ where `d ≡ c [MOD 3]`.
 Given the above lemmas, the desired result reduces to an arithmetic result, given in the file
 `arithmetic.lean`.
 
-We'll use this result to show we can derive an `Miustr` of the form `M::z` where `z` is an string
+We'll use this result to show we can derive an `Miustr` of the form `M::z` where `z` is a string
 consisting only of `I`s such that `count I z ≡ 1 or 2 [MOD 3]`.
 
 As an intermediate step, we show that derive `z` from `zt`, where `t` is an `Miustr` consisting of

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -151,7 +151,7 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
       Prod.ext_iff]
     rintro ⟨i, rfl, rfl⟩
     specialize q i
-    -- Show `1 ≤ a_i` and `1 ≤ b_i`, which is easy from the fact that `{i}` is a increasing and
+    -- Show `1 ≤ a_i` and `1 ≤ b_i`, which is easy from the fact that `{i}` is an increasing and
     -- decreasing subsequence which we did right near the top.
     have z : 1 ≤ (ab i).1 ∧ 1 ≤ (ab i).2 := by
       simp only [← hab]

Mathlib/Algebra/Category/SemigroupCat/Basic.lean

@@ -111,7 +111,7 @@ def ofHom {X Y : Type u} [Mul X] [Mul Y] (f : X →ₙ* Y) : of X ⟶ of Y := f
 #align Magma.of_hom MagmaCat.ofHom
 #align AddMagma.of_hom AddMagmaCat.ofHom
 
-/-- Typecheck a `AddHom` as a morphism in `AddMagmaCat`. -/
+/-- Typecheck an `AddHom` as a morphism in `AddMagmaCat`. -/
 add_decl_doc AddMagmaCat.ofHom
 
 @[to_additive] -- Porting note: simp removed, simpNF says LHS simplifies to itself
@@ -197,7 +197,7 @@ def ofHom {X Y : Type u} [Semigroup X] [Semigroup Y] (f : X →ₙ* Y) : of X 
 #align Semigroup.of_hom SemigroupCat.ofHom
 #align AddSemigroup.of_hom AddSemigroupCat.ofHom
 
-/-- Typecheck a `AddHom` as a morphism in `AddSemigroupCat`. -/
+/-- Typecheck an `AddHom` as a morphism in `AddSemigroupCat`. -/
 add_decl_doc AddSemigroupCat.ofHom
 
 @[to_additive] -- Porting note: simp removed, simpNF says LHS simplifies to itself

Mathlib/Algebra/Group/WithOne/Defs.lean

@@ -125,9 +125,9 @@ def recOneCoe {C : WithOne α → Sort _} (h₁ : C 1) (h₂ : ∀ a : α, C a)
 attribute [elab_as_elim] WithZero.recZeroCoe
 
 
-/-- Deconstruct a `x : WithOne α` to the underlying value in `α`, given a proof that `x ≠ 1`. -/
+/-- Deconstruct an `x : WithOne α` to the underlying value in `α`, given a proof that `x ≠ 1`. -/
 @[to_additive unzero
-      "Deconstruct a `x : WithZero α` to the underlying value in `α`, given a proof that `x ≠ 0`."]
+      "Deconstruct an `x : WithZero α` to the underlying value in `α`, given a proof that `x ≠ 0`."]
 def unone {x : WithOne α} (hx : x ≠ 1) : α :=
   WithBot.unbot x hx
 #align with_one.unone WithOne.unone

Mathlib/Algebra/Hom/Freiman.lean

@@ -14,7 +14,7 @@ import Mathlib.Data.FunLike.Basic
 /-!
 # Freiman homomorphisms
 
-In this file, we define Freiman homomorphisms. A `n`-Freiman homomorphism on `A` is a function
+In this file, we define Freiman homomorphisms. An `n`-Freiman homomorphism on `A` is a function
 `f : α → β` such that `f (x₁) * ... * f (xₙ) = f (y₁) * ... * f (yₙ)` for all
 `x₁, ..., xₙ, y₁, ..., yₙ ∈ A` such that `x₁ * ... * xₙ = y₁ * ... * yₙ`. In particular, any
 `MulHom` is a Freiman homomorphism.
@@ -67,12 +67,12 @@ structure AddFreimanHom (A : Set α) (β : Type _) [AddCommMonoid α] [AddCommMo
     (s.map toFun).sum = (t.map toFun).sum
 #align add_freiman_hom AddFreimanHom
 
-/-- A `n`-Freiman homomorphism on a set `A` is a map which preserves products of `n` elements. -/
+/-- An `n`-Freiman homomorphism on a set `A` is a map which preserves products of `n` elements. -/
 @[to_additive AddFreimanHom]
 structure FreimanHom (A : Set α) (β : Type _) [CommMonoid α] [CommMonoid β] (n : ℕ) where
   /-- The underlying function. -/
   toFun : α → β
-  /-- A `n`-Freiman homomorphism preserves products of `n` elements. -/
+  /-- An `n`-Freiman homomorphism preserves products of `n` elements. -/
   map_prod_eq_map_prod' {s t : Multiset α} (hsA : ∀ ⦃x⦄, x ∈ s → x ∈ A) (htA : ∀ ⦃x⦄, x ∈ t → x ∈ A)
     (hs : Multiset.card s = n) (ht : Multiset.card t = n) (h : s.prod = t.prod) :
     (s.map toFun).prod = (t.map toFun).prod
@@ -106,7 +106,7 @@ You should extend this class when you extend `FreimanHom`. -/
       sums-preserving morphisms. You should extend this class when you extend `AddFreimanHom`."]
 class FreimanHomClass (F : Type _) (A : outParam <| Set α) (β : outParam <| Type _) [CommMonoid α]
   [CommMonoid β] (n : ℕ) [FunLike F α fun _ => β] : Prop where
-  /-- A `n`-Freiman homomorphism preserves products of `n` elements. -/
+  /-- An `n`-Freiman homomorphism preserves products of `n` elements. -/
   map_prod_eq_map_prod' (f : F) {s t : Multiset α} (hsA : ∀ ⦃x⦄, x ∈ s → x ∈ A)
     (htA : ∀ ⦃x⦄, x ∈ t → x ∈ A) (hs : Multiset.card s = n) (ht : Multiset.card t = n)
     (h : s.prod = t.prod) :
@@ -534,7 +534,7 @@ def FreimanHom.toFreimanHom (h : m ≤ n) (f : A →*[n] β) : A →*[m] β wher
 #align freiman_hom.to_freiman_hom FreimanHom.toFreimanHom
 #align add_freiman_hom.to_add_freiman_hom AddFreimanHom.toAddFreimanHom
 
-/-- A `n`-Freiman homomorphism is also a `m`-Freiman homomorphism for any `m ≤ n`. -/
+/-- An `n`-Freiman homomorphism is also a `m`-Freiman homomorphism for any `m ≤ n`. -/
 @[to_additive AddFreimanHom.addFreimanHomClass_of_le
       "An additive `n`-Freiman homomorphism is
       also an additive `m`-Freiman homomorphism for any `m ≤ n`."]

Mathlib/Algebra/Homology/Augment.lean

@@ -25,7 +25,7 @@ variable {V : Type u} [Category.{v} V]
 
 namespace ChainComplex
 
-/-- The truncation of a `ℕ`-indexed chain complex,
+/-- The truncation of an `ℕ`-indexed chain complex,
 deleting the object at `0` and shifting everything else down.
 -/
 @[simps]
@@ -204,7 +204,7 @@ end ChainComplex
 
 namespace CochainComplex
 
-/-- The truncation of a `ℕ`-indexed cochain complex,
+/-- The truncation of an `ℕ`-indexed cochain complex,
 deleting the object at `0` and shifting everything else down.
 -/
 @[simps]

Mathlib/Algebra/Homology/Single.lean

@@ -20,7 +20,7 @@ Similarly `single₀ V : V ⥤ ChainComplex V ℕ` is the special case for
 `ℕ`-indexed chain complexes, with the object supported in degree `0`,
 but with better definitional properties.
 
-In `toSingle₀Equiv` we characterize chain maps to a `ℕ`-indexed complex concentrated in degree 0;
+In `toSingle₀Equiv` we characterize chain maps to an `ℕ`-indexed complex concentrated in degree 0;
 they are equivalent to `{ f : C.X 0 ⟶ X // C.d 1 0 ≫ f = 0 }`.
 (This is useful translating between a projective resolution and
 an augmented exact complex of projectives.)
@@ -221,7 +221,7 @@ end
 
 variable {V}
 
-/-- Morphisms from a `ℕ`-indexed chain complex `C`
+/-- Morphisms from an `ℕ`-indexed chain complex `C`
 to a single object chain complex with `X` concentrated in degree 0
 are the same as morphisms `f : C.X 0 ⟶ X` such that `C.d 1 0 ≫ f = 0`.
 -/
@@ -263,7 +263,7 @@ theorem to_single₀_ext {C : ChainComplex V ℕ} {X : V} (f g : C ⟶ (single
 #align chain_complex.to_single₀_ext ChainComplex.to_single₀_ext
 
 /-- Morphisms from a single object chain complex with `X` concentrated in degree 0
-to a `ℕ`-indexed chain complex `C` are the same as morphisms `f : X → C.X`.
+to an `ℕ`-indexed chain complex `C` are the same as morphisms `f : X → C.X`.
 -/
 @[simps]
 def fromSingle₀Equiv (C : ChainComplex V ℕ) (X : V) : ((single₀ V).obj X ⟶ C) ≃ (X ⟶ C.X 0) where
@@ -419,7 +419,7 @@ end
 variable {V}
 
 /-- Morphisms from a single object cochain complex with `X` concentrated in degree 0
-to a `ℕ`-indexed cochain complex `C`
+to an `ℕ`-indexed cochain complex `C`
 are the same as morphisms `f : X ⟶ C.X 0` such that `f ≫ C.d 0 1 = 0`.
 -/
 def fromSingle₀Equiv (C : CochainComplex V ℕ) (X : V) :

Mathlib/Algebra/Module/LinearMap.lean

@@ -738,7 +738,7 @@ abbrev Module.End (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Modu
   M →ₗ[R] M
 #align module.End Module.End
 
-/-- Reinterpret an additive homomorphism as a `ℕ`-linear map. -/
+/-- Reinterpret an additive homomorphism as an `ℕ`-linear map. -/
 def AddMonoidHom.toNatLinearMap [AddCommMonoid M] [AddCommMonoid M₂] (f : M →+ M₂) : M →ₗ[ℕ] M₂
     where
   toFun := f

Mathlib/Algebra/Star/Subalgebra.lean

@@ -775,7 +775,7 @@ theorem ext_adjoin_singleton {a : A} [StarAlgHomClass F R (adjoin R ({a} : Set A
       h
 #align star_alg_hom.ext_adjoin_singleton StarAlgHom.ext_adjoin_singleton
 
-/-- Range of an `StarAlgHom` as a star subalgebra. -/
+/-- Range of a `StarAlgHom` as a star subalgebra. -/
 protected def range
     (φ : A →⋆ₐ[R] B) : StarSubalgebra R B where
   toSubalgebra := φ.toAlgHom.range

Mathlib/Algebra/Tropical/Basic.lean

@@ -159,7 +159,7 @@ theorem surjective_untrop : Function.Surjective (untrop : Tropical R → R) :=
 instance [Inhabited R] : Inhabited (Tropical R) :=
   ⟨trop default⟩
 
-/-- Recursing on a `x' : Tropical R` is the same as recursing on an `x : R` reinterpreted
+/-- Recursing on an `x' : Tropical R` is the same as recursing on an `x : R` reinterpreted
 as a term of `Tropical R` via `trop x`. -/
 @[simp]
 def tropRec {F : Tropical R → Sort v} (h : ∀ X, F (trop X)) : ∀ X, F X := fun X => h (untrop X)

Mathlib/AlgebraicGeometry/Gluing.lean

@@ -41,7 +41,7 @@ Given a family of gluing data of schemes, we may glue them together.
   (intersection) of `U i` and `U j` over the glued space.
 * `AlgebraicGeometry.Scheme.GlueData.ι_eq_iff` : `ι i x = ι j y` if and only if they coincide
   when restricted to `V i i`.
-* `AlgebraicGeometry.Scheme.GlueData.isOpen_iff` : An subset of the glued scheme is open iff
+* `AlgebraicGeometry.Scheme.GlueData.isOpen_iff` : A subset of the glued scheme is open iff
   all its preimages in `U i` are open.
 
 ## Implementation details
@@ -69,8 +69,8 @@ namespace Scheme
 
 /-- A family of gluing data consists of
 1. An index type `J`
-2. An scheme `U i` for each `i : J`.
-3. An scheme `V i j` for each `i j : J`.
+2. A scheme `U i` for each `i : J`.
+3. A scheme `V i j` for each `i j : J`.
   (Note that this is `J × J → Scheme` rather than `J → J → Scheme` to connect to the
   limits library easier.)
 4. An open immersion `f i j : V i j ⟶ U i` for each `i j : ι`.

Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

@@ -89,7 +89,7 @@ protected def Scheme.affineTargetIsIso : AffineTargetMorphismProperty := fun _ _
 instance : Inhabited AffineTargetMorphismProperty :=
   ⟨Scheme.affineTargetIsIso⟩
 
-/-- A `affine_target_morphism_property` can be extended to a `morphism_property` such that it
+/-- An `affine_target_morphism_property` can be extended to a `morphism_property` such that it
 *never* holds when the target is not affine -/
 def AffineTargetMorphismProperty.toProperty (P : AffineTargetMorphismProperty) :
     MorphismProperty Scheme := fun _ _ f => ∃ h, @P _ _ f h

Mathlib/AlgebraicGeometry/OpenImmersion/Scheme.lean

@@ -236,7 +236,7 @@ def affineBasisCoverOfAffine (R : CommRingCat) : OpenCover (Spec.obj (Opposite.o
   IsOpen x := AlgebraicGeometry.Scheme.basic_open_isOpenImmersion x
 #align algebraic_geometry.Scheme.affine_basis_cover_of_affine AlgebraicGeometry.Scheme.affineBasisCoverOfAffine
 
-/-- We may bind the basic open sets of an open affine cover to form a affine cover that is also
+/-- We may bind the basic open sets of an open affine cover to form an affine cover that is also
 a basis. -/
 def affineBasisCover (X : Scheme) : OpenCover X :=
   X.affineCover.bind fun _ => affineBasisCoverOfAffine _

Mathlib/AlgebraicGeometry/Scheme.lean

@@ -35,7 +35,7 @@ open Opposite
 
 namespace AlgebraicGeometry
 
-/-- We define `Scheme` as a `X : LocallyRingedSpace`,
+/-- We define `Scheme` as an `X : LocallyRingedSpace`,
 along with a proof that every point has an open neighbourhood `U`
 so that that the restriction of `X` to `U` is isomorphic,
 as a locally ringed space, to `Spec.toLocallyRingedSpace.obj (op R)`

Mathlib/Analysis/Analytic/IsolatedZeros.lean

@@ -41,7 +41,7 @@ open scoped Topology BigOperators
 variable {𝕜 : Type _} [NontriviallyNormedField 𝕜] {E : Type _} [NormedAddCommGroup E]
   [NormedSpace 𝕜 E] {s : E} {p q : FormalMultilinearSeries 𝕜 𝕜 E} {f g : 𝕜 → E} {n : ℕ} {z z₀ : 𝕜}
 --  {y : Fin n → 𝕜} -- Porting note: This is used nowhere and creates problem since it is sometimes
--- automatically included as an hypothesis
+-- automatically included as a hypothesis
 
 namespace HasSum
 

Mathlib/Analysis/Calculus/Taylor.lean

@@ -237,7 +237,7 @@ theorem has_deriv_within_taylorWithinEval_at_Icc {f : ℝ → E} {a b t : ℝ} (
 
 We assume that `f` is `n+1`-times continuously differentiable in the closed set `Icc x₀ x` and
 `n+1`-times differentiable on the open set `Ioo x₀ x`, and `g` is a differentiable function on
-`Ioo x₀ x` and continuous on `Icc x₀ x`. Then there exists a `x' ∈ Ioo x₀ x` such that
+`Ioo x₀ x` and continuous on `Icc x₀ x`. Then there exists an `x' ∈ Ioo x₀ x` such that
 $$f(x) - (P_n f)(x₀, x) = \frac{(x - x')^n}{n!} \frac{g(x) - g(x₀)}{g' x'},$$
 where $P_n f$ denotes the Taylor polynomial of degree $n$. -/
 theorem taylor_mean_remainder {f : ℝ → ℝ} {g g' : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x)
@@ -265,8 +265,8 @@ theorem taylor_mean_remainder {f : ℝ → ℝ} {g g' : ℝ → ℝ} {x x₀ : 
 /-- **Taylor's theorem** with the Lagrange form of the remainder.
 
 We assume that `f` is `n+1`-times continuously differentiable in the closed set `Icc x₀ x` and
-`n+1`-times differentiable on the open set `Ioo x₀ x`. Then there exists a `x' ∈ Ioo x₀ x` such that
-$$f(x) - (P_n f)(x₀, x) = \frac{f^{(n+1)}(x') (x - x₀)^{n+1}}{(n+1)!},$$
+`n+1`-times differentiable on the open set `Ioo x₀ x`. Then there exists an `x' ∈ Ioo x₀ x` such
+that $$f(x) - (P_n f)(x₀, x) = \frac{f^{(n+1)}(x') (x - x₀)^{n+1}}{(n+1)!},$$
 where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated
 derivative. -/
 theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x)
@@ -306,8 +306,8 @@ theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ
 /-- **Taylor's theorem** with the Cauchy form of the remainder.
 
 We assume that `f` is `n+1`-times continuously differentiable on the closed set `Icc x₀ x` and
-`n+1`-times differentiable on the open set `Ioo x₀ x`. Then there exists a `x' ∈ Ioo x₀ x` such that
-$$f(x) - (P_n f)(x₀, x) = \frac{f^{(n+1)}(x') (x - x')^n (x-x₀)}{n!},$$
+`n+1`-times differentiable on the open set `Ioo x₀ x`. Then there exists an `x' ∈ Ioo x₀ x` such
+that $$f(x) - (P_n f)(x₀, x) = \frac{f^{(n+1)}(x') (x - x')^n (x-x₀)}{n!},$$
 where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated
 derivative. -/
 theorem taylor_mean_remainder_cauchy {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x)

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -20,7 +20,7 @@ import Mathlib.Tactic.LinearCombination
 
 This file defines `UpperHalfPlane` to be the upper half plane in `ℂ`.
 
-We furthermore equip it with the structure of an `GLPos 2 ℝ` action by
+We furthermore equip it with the structure of a `GLPos 2 ℝ` action by
 fractional linear transformations.
 
 We define the notation `ℍ` for the upper half plane available in the locale

Mathlib/Analysis/Convolution.lean

@@ -88,7 +88,7 @@ The following notations are localized in the locale `convolution`:
   This might require a generalization of `MeasureTheory.Memℒp.smul` where `smul` is generalized
   to a continuous bilinear map.
   (see e.g. [Fremlin, *Measure Theory* (volume 2)][fremlin_vol2], 255K)
-* The convolution is a `AEStronglyMeasurable` function
+* The convolution is an `AEStronglyMeasurable` function
   (see e.g. [Fremlin, *Measure Theory* (volume 2)][fremlin_vol2], 255I).
 * Prove properties about the convolution if both functions are rapidly decreasing.
 * Use `@[to_additive]` everywhere
@@ -843,7 +843,7 @@ variable [SeminormedAddCommGroup G]
 on `Metric.ball x₀ R`.
 
 We can simplify the RHS further if we assume `f` is integrable, but also if `L = (•)` or more
-generally if `L` has a `AntilipschitzWith`-condition. -/
+generally if `L` has an `AntilipschitzWith`-condition. -/
 theorem convolution_eq_right' {x₀ : G} {R : ℝ} (hf : support f ⊆ ball (0 : G) R)
     (hg : ∀ x ∈ ball x₀ R, g x = g x₀) : (f ⋆[L, μ] g) x₀ = ∫ t, L (f t) (g x₀) ∂μ := by
   have h2 : ∀ t, L (f t) (g (x₀ - t)) = L (f t) (g x₀) := fun t ↦ by

Mathlib/CategoryTheory/Enriched/Basic.lean

@@ -20,7 +20,7 @@ We set up the basic theory of `V`-enriched categories,
 for `V` an arbitrary monoidal category.
 
 We do not assume here that `V` is a concrete category,
-so there does not need to be a "honest" underlying category!
+so there does not need to be an "honest" underlying category!
 
 Use `X ⟶[V] Y` to obtain the `V` object of morphisms from `X` to `Y`.
 

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -345,7 +345,7 @@ instance (priority := 100) hasProduct_unique : HasProduct f :=
   HasLimit.mk (limitConeOfUnique f)
 #align category_theory.limits.has_product_unique CategoryTheory.Limits.hasProduct_unique
 
-/-- A product over a index type with exactly one term is just the object over that term. -/
+/-- A product over an index type with exactly one term is just the object over that term. -/
 @[simps!]
 def productUniqueIso : ∏ f ≅ f default :=
   IsLimit.conePointUniqueUpToIso (limit.isLimit _) (limitConeOfUnique f).isLimit

Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean

@@ -139,16 +139,16 @@ end
 variable (f g)
 
 /--
-The pair `f,g` is a split pair if there is a `h : Y ⟶ Z` so that `f, g, h` forms a split coequalizer
-in `C`.
+The pair `f,g` is a split pair if there is an `h : Y ⟶ Z` so that `f, g, h` forms a split
+coequalizer in `C`.
 -/
 class HasSplitCoequalizer : Prop where
   /-- There is some split coequalizer -/
   splittable : ∃ (Z : C) (h : Y ⟶ Z), Nonempty (IsSplitCoequalizer f g h)
 #align category_theory.has_split_coequalizer CategoryTheory.HasSplitCoequalizer
 
 /--
-The pair `f,g` is a `G`-split pair if there is a `h : G Y ⟶ Z` so that `G f, G g, h` forms a split
+The pair `f,g` is a `G`-split pair if there is an `h : G Y ⟶ Z` so that `G f, G g, h` forms a split
 coequalizer in `D`.
 -/
 abbrev Functor.IsSplitPair : Prop :=

Mathlib/CategoryTheory/Preadditive/InjectiveResolution.lean

@@ -15,7 +15,7 @@ import Mathlib.Algebra.Homology.Single
 # Injective resolutions
 
 An injective resolution `I : InjectiveResolution Z` of an object `Z : C` consists of
-a `ℕ`-indexed cochain complex `I.cocomplex` of injective objects,
+an `ℕ`-indexed cochain complex `I.cocomplex` of injective objects,
 along with a cochain map `I.ι` from cochain complex consisting just of `Z` in degree zero to `C`,
 so that the augmented cochain complex is exact.
 ```

Mathlib/CategoryTheory/Preadditive/ProjectiveResolution.lean

@@ -16,7 +16,7 @@ import Mathlib.Algebra.Homology.HomotopyCategory
 # Projective resolutions
 
 A projective resolution `P : ProjectiveResolution Z` of an object `Z : C` consists of
-a `ℕ`-indexed chain complex `P.complex` of projective objects,
+an `ℕ`-indexed chain complex `P.complex` of projective objects,
 along with a chain map `P.π` from `C` to the chain complex consisting just of `Z` in degree zero,
 so that the augmented chain complex is exact.
 

Mathlib/Combinatorics/SetFamily/Shadow.lean

@@ -87,7 +87,7 @@ theorem shadow_monotone : Monotone (shadow : Finset (Finset α) → Finset (Fins
   sup_mono
 #align finset.shadow_monotone Finset.shadow_monotone
 
-/-- `s` is in the shadow of `𝒜` iff there is an `t ∈ 𝒜` from which we can remove one element to
+/-- `s` is in the shadow of `𝒜` iff there is a `t ∈ 𝒜` from which we can remove one element to
 get `s`. -/
 theorem mem_shadow_iff : s ∈ ∂ 𝒜 ↔ ∃ t ∈ 𝒜, ∃ a ∈ t, erase t a = s := by
   simp only [shadow, mem_sup, mem_image]
@@ -203,7 +203,7 @@ theorem upShadow_monotone : Monotone (upShadow : Finset (Finset α) → Finset (
   fun _ _ => sup_mono
 #align finset.up_shadow_monotone Finset.upShadow_monotone
 
-/-- `s` is in the upper shadow of `𝒜` iff there is an `t ∈ 𝒜` from which we can remove one element
+/-- `s` is in the upper shadow of `𝒜` iff there is a `t ∈ 𝒜` from which we can remove one element
 to get `s`. -/
 theorem mem_upShadow_iff : s ∈ ∂⁺ 𝒜 ↔ ∃ t ∈ 𝒜, ∃ (a : _) (_ : a ∉ t), insert a t = s := by
   simp_rw [upShadow, mem_sup, mem_image, exists_prop, mem_compl]