chore: fix grammar 2/3 (#5002)

Part 2 of #5001

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean

@@ -161,15 +161,15 @@ def preservesColimitsOfShapePemptyOfPreservesInitial [PreservesColimit (Functor.
 
 variable [HasInitial C]
 
-/-- If `G` preserves the initial object and `C` has a initial object, then the image of the initial
+/-- If `G` preserves the initial object and `C` has an initial object, then the image of the initial
 object is initial.
 -/
 def isColimitOfHasInitialOfPreservesColimit [PreservesColimit (Functor.empty.{0} C) G] :
     IsInitial (G.obj (⊥_ C)) :=
   initialIsInitial.isInitialObj G (⊥_ C)
 #align category_theory.limits.is_colimit_of_has_initial_of_preserves_colimit CategoryTheory.Limits.isColimitOfHasInitialOfPreservesColimit
 
-/-- If `C` has a initial object and `G` preserves initial objects, then `D` has a initial object
+/-- If `C` has an initial object and `G` preserves initial objects, then `D` has an initial object
 also.
 Note this property is somewhat unique to colimits of the empty diagram: for general `J`, if `C`
 has colimits of shape `J` and `G` preserves them, then `D` does not necessarily have colimits of

Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean

@@ -905,7 +905,7 @@ theorem coprod.map_id_comp {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryC
 #align category_theory.limits.coprod.map_id_comp CategoryTheory.Limits.coprod.map_id_comp
 
 /-- If the coproducts `W ⨿ X` and `Y ⨿ Z` exist, then every pair of isomorphisms `f : W ≅ Y` and
-   `g : W ≅ Z` induces a isomorphism `coprod.mapIso f g : W ⨿ X ≅ Y ⨿ Z`. -/
+   `g : W ≅ Z` induces an isomorphism `coprod.mapIso f g : W ⨿ X ≅ Y ⨿ Z`. -/
 @[simps]
 def coprod.mapIso {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ≅ Y)
     (g : X ≅ Z) : W ⨿ X ≅ Y ⨿ Z where

Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

@@ -406,7 +406,7 @@ theorem biproduct.bicone_ι (f : J → C) [HasBiproduct f] (b : J) :
     (biproduct.bicone f).ι b = biproduct.ι f b := rfl
 #align category_theory.limits.biproduct.bicone_ι CategoryTheory.Limits.biproduct.bicone_ι
 
-/-- Note that as this lemma has a `if` in the statement, we include a `DecidableEq` argument.
+/-- Note that as this lemma has an `if` in the statement, we include a `DecidableEq` argument.
 This means you may not be able to `simp` using this lemma unless you `open Classical`. -/
 @[reassoc]
 theorem biproduct.ι_π [DecidableEq J] (f : J → C) [HasBiproduct f] (j j' : J) :
@@ -946,7 +946,7 @@ instance (priority := 100) hasBiproduct_unique : HasBiproduct f :=
   HasBiproduct.mk (limitBiconeOfUnique f)
 #align category_theory.limits.has_biproduct_unique CategoryTheory.Limits.hasBiproduct_unique
 
-/-- A biproduct over a index type with exactly one term is just the object over that term. -/
+/-- A biproduct over an index type with exactly one term is just the object over that term. -/
 @[simps!]
 def biproductUniqueIso : ⨁ f ≅ f default :=
   (biproduct.uniqueUpToIso _ (limitBiconeOfUnique f).isBilimit).symm

Mathlib/CategoryTheory/Limits/Shapes/CommSq.lean

@@ -200,7 +200,7 @@ namespace IsPullback
 variable {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z}
 
 /-- The (limiting) `PullbackCone f g` implicit in the statement
-that we have a `IsPullback fst snd f g`.
+that we have an `IsPullback fst snd f g`.
 -/
 def cone (h : IsPullback fst snd f g) : PullbackCone f g :=
   h.toCommSq.cone
@@ -222,7 +222,7 @@ noncomputable def isLimit (h : IsPullback fst snd f g) : IsLimit h.cone :=
   h.isLimit'.some
 #align category_theory.is_pullback.is_limit CategoryTheory.IsPullback.isLimit
 
-/-- If `c` is a limiting pullback cone, then we have a `IsPullback c.fst c.snd f g`. -/
+/-- If `c` is a limiting pullback cone, then we have an `IsPullback c.fst c.snd f g`. -/
 theorem of_isLimit {c : PullbackCone f g} (h : Limits.IsLimit c) : IsPullback c.fst c.snd f g :=
   { w := c.condition
     isLimit' := ⟨IsLimit.ofIsoLimit h (Limits.PullbackCone.ext (Iso.refl _)
@@ -235,7 +235,7 @@ theorem of_isLimit' (w : CommSq fst snd f g) (h : Limits.IsLimit w.cone) :
   of_isLimit h
 #align category_theory.is_pullback.of_is_limit' CategoryTheory.IsPullback.of_isLimit'
 
-/-- The pullback provided by `HasPullback f g` fits into a `IsPullback`. -/
+/-- The pullback provided by `HasPullback f g` fits into an `IsPullback`. -/
 theorem of_hasPullback (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :
     IsPullback (pullback.fst : pullback f g ⟶ X) (pullback.snd : pullback f g ⟶ Y) f g :=
   of_isLimit (limit.isLimit (cospan f g))
@@ -331,7 +331,7 @@ namespace IsPushout
 variable {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P}
 
 /-- The (colimiting) `PushoutCocone f g` implicit in the statement
-that we have a `IsPushout f g inl inr`.
+that we have an `IsPushout f g inl inr`.
 -/
 def cocone (h : IsPushout f g inl inr) : PushoutCocone f g :=
   h.toCommSq.cocone
@@ -353,7 +353,7 @@ noncomputable def isColimit (h : IsPushout f g inl inr) : IsColimit h.cocone :=
   h.isColimit'.some
 #align category_theory.is_pushout.is_colimit CategoryTheory.IsPushout.isColimit
 
-/-- If `c` is a colimiting pushout cocone, then we have a `IsPushout f g c.inl c.inr`. -/
+/-- If `c` is a colimiting pushout cocone, then we have an `IsPushout f g c.inl c.inr`. -/
 theorem of_isColimit {c : PushoutCocone f g} (h : Limits.IsColimit c) : IsPushout f g c.inl c.inr :=
   { w := c.condition
     isColimit' :=
@@ -367,7 +367,7 @@ theorem of_isColimit' (w : CommSq f g inl inr) (h : Limits.IsColimit w.cocone) :
   of_isColimit h
 #align category_theory.is_pushout.of_is_colimit' CategoryTheory.IsPushout.of_isColimit'
 
-/-- The pushout provided by `HasPushout f g` fits into a `IsPushout`. -/
+/-- The pushout provided by `HasPushout f g` fits into an `IsPushout`. -/
 theorem of_hasPushout (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g] :
     IsPushout f g (pushout.inl : X ⟶ pushout f g) (pushout.inr : Y ⟶ pushout f g) :=
   of_isColimit (colimit.isColimit (span f g))

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -379,7 +379,7 @@ instance (priority := 100) hasCoproduct_unique : HasCoproduct f :=
   HasColimit.mk (colimitCoconeOfUnique f)
 #align category_theory.limits.has_coproduct_unique CategoryTheory.Limits.hasCoproduct_unique
 
-/-- A coproduct over a index type with exactly one term is just the object over that term. -/
+/-- A coproduct over an index type with exactly one term is just the object over that term. -/
 @[simps!]
 def coproductUniqueIso : ∐ f ≅ f default :=
   IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (colimitCoconeOfUnique f).isColimit

Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean

@@ -255,7 +255,7 @@ theorem span_map_id {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (w : WalkingSpan) :
     (span f g).map (WalkingSpan.Hom.id w) = 𝟙 _ := rfl
 #align category_theory.limits.span_map_id CategoryTheory.Limits.span_map_id
 
-/-- Every diagram indexing an pullback is naturally isomorphic (actually, equal) to a `cospan` -/
+/-- Every diagram indexing a pullback is naturally isomorphic (actually, equal) to a `cospan` -/
 -- @[simps (config := { rhsMd := semireducible })]  Porting note: no semireducible
 @[simps!]
 def diagramIsoCospan (F : WalkingCospan ⥤ C) : F ≅ cospan (F.map inl) (F.map inr) :=

Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean

@@ -494,7 +494,7 @@ theorem ι_colimitConstInitial_hom {J : Type _} [Category J] {C : Type _} [Categ
       initial.to _ := by apply Limits.colimit.hom_ext; aesop_cat
 #align category_theory.limits.ι_colimit_const_initial_hom CategoryTheory.Limits.ι_colimitConstInitial_hom
 
-/-- A category is a `InitialMonoClass` if the canonical morphism of an initial object is a
+/-- A category is an `InitialMonoClass` if the canonical morphism of an initial object is a
 monomorphism.  In practice, this is most useful when given an arbitrary morphism out of the chosen
 initial object, see `initial.mono_from`.
 Given a terminal object, this is equivalent to the assumption that the unique morphism from initial
@@ -519,7 +519,7 @@ instance (priority := 100) initial.mono_from [HasInitial C] [InitialMonoClass C]
   initialIsInitial.mono_from f
 #align category_theory.limits.initial.mono_from CategoryTheory.Limits.initial.mono_from
 
-/-- To show a category is a `InitialMonoClass` it suffices to give an initial object such that
+/-- To show a category is an `InitialMonoClass` it suffices to give an initial object such that
 every morphism out of it is a monomorphism. -/
 theorem InitialMonoClass.of_isInitial {I : C} (hI : IsInitial I) (h : ∀ X, Mono (hI.to X)) :
     InitialMonoClass C where
@@ -529,21 +529,21 @@ theorem InitialMonoClass.of_isInitial {I : C} (hI : IsInitial I) (h : ∀ X, Mon
     apply mono_comp
 #align category_theory.limits.initial_mono_class.of_is_initial CategoryTheory.Limits.InitialMonoClass.of_isInitial
 
-/-- To show a category is a `InitialMonoClass` it suffices to show every morphism out of the
+/-- To show a category is an `InitialMonoClass` it suffices to show every morphism out of the
 initial object is a monomorphism. -/
 theorem InitialMonoClass.of_initial [HasInitial C] (h : ∀ X : C, Mono (initial.to X)) :
     InitialMonoClass C :=
   InitialMonoClass.of_isInitial initialIsInitial h
 #align category_theory.limits.initial_mono_class.of_initial CategoryTheory.Limits.InitialMonoClass.of_initial
 
-/-- To show a category is a `InitialMonoClass` it suffices to show the unique morphism from an
+/-- To show a category is an `InitialMonoClass` it suffices to show the unique morphism from an
 initial object to a terminal object is a monomorphism. -/
 theorem InitialMonoClass.of_isTerminal {I T : C} (hI : IsInitial I) (hT : IsTerminal T)
     (_ : Mono (hI.to T)) : InitialMonoClass C :=
   InitialMonoClass.of_isInitial hI fun X => mono_of_mono_fac (hI.hom_ext (_ ≫ hT.from X) (hI.to T))
 #align category_theory.limits.initial_mono_class.of_is_terminal CategoryTheory.Limits.InitialMonoClass.of_isTerminal
 
-/-- To show a category is a `InitialMonoClass` it suffices to show the unique morphism from the
+/-- To show a category is an `InitialMonoClass` it suffices to show the unique morphism from the
 initial object to a terminal object is a monomorphism. -/
 theorem InitialMonoClass.of_terminal [HasInitial C] [HasTerminal C] (h : Mono (initial.to (⊤_ C))) :
     InitialMonoClass C :=

Mathlib/CategoryTheory/Limits/Shapes/Types.lean

@@ -304,7 +304,7 @@ theorem binaryCofan_isColimit_iff {X Y : Type u} (c : BinaryCofan X Y) :
         split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm
 #align category_theory.limits.types.binary_cofan_is_colimit_iff CategoryTheory.Limits.Types.binaryCofan_isColimit_iff
 
-/-- Any monomorphism in `Type` is an coproduct injection. -/
+/-- Any monomorphism in `Type` is a coproduct injection. -/
 noncomputable def isCoprodOfMono {X Y : Type u} (f : X ⟶ Y) [Mono f] :
     IsColimit (BinaryCofan.mk f (Subtype.val : ↑(Set.range fᶜ) → Y)) := by
   apply Nonempty.some

Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean

@@ -431,7 +431,7 @@ theorem idZeroEquivIsoZero_apply_inv (X : C) (h : 𝟙 X = 0) : ((idZeroEquivIso
   rfl
 #align category_theory.limits.id_zero_equiv_iso_zero_apply_inv CategoryTheory.Limits.idZeroEquivIsoZero_apply_inv
 
-/-- If `0 : X ⟶ Y` is an monomorphism, then `X ≅ 0`. -/
+/-- If `0 : X ⟶ Y` is a monomorphism, then `X ≅ 0`. -/
 @[simps]
 def isoZeroOfMonoZero {X Y : C} (h : Mono (0 : X ⟶ Y)) : X ≅ 0 where
   hom := 0

Mathlib/CategoryTheory/Monoidal/Category.lean

@@ -543,7 +543,7 @@ variable (C : Type u) [Category.{v} C] [MonoidalCategory.{v} C]
 
 /-- Tensoring on the left, as a functor from `C` into endofunctors of `C`.
 
-TODO: show this is a op-monoidal functor.
+TODO: show this is an op-monoidal functor.
 -/
 @[simps]
 def tensoringLeft : C ⥤ C ⥤ C where

Mathlib/CategoryTheory/Over.lean

@@ -473,8 +473,8 @@ theorem mono_of_mono_right {f g : Under X} (k : f ⟶ g) [hk : Mono k.right] : M
 #align category_theory.under.mono_of_mono_right CategoryTheory.Under.mono_of_mono_right
 
 /--
-If `k.right` is a epimorphism, then `k` is a epimorphism. In other words, `Under.forget X` reflects
-epimorphisms.
+If `k.right` is an epimorphism, then `k` is an epimorphism. In other words, `Under.forget X`
+reflects epimorphisms.
 The converse of `CategoryTheory.Under.epi_right_of_epi`.
 
 This lemma is not an instance, to avoid loops in type class inference.
@@ -484,8 +484,8 @@ theorem epi_of_epi_right {f g : Under X} (k : f ⟶ g) [hk : Epi k.right] : Epi
 #align category_theory.under.epi_of_epi_right CategoryTheory.Under.epi_of_epi_right
 
 /--
-If `k` is a epimorphism, then `k.right` is a epimorphism. In other words, `Under.forget X` preserves
-epimorphisms.
+If `k` is an epimorphism, then `k.right` is an epimorphism. In other words, `Under.forget X`
+preserves epimorphisms.
 The converse of `CategoryTheory.under.epi_of_epi_right`.
 -/
 instance epi_right_of_epi {f g : Under X} (k : f ⟶ g) [Epi k] : Epi k.right := by

Mathlib/CategoryTheory/Pi/Basic.lean

@@ -77,7 +77,7 @@ instance (f : J → I) : (j : J) → Category ((C ∘ f) j) := by
   dsimp
   infer_instance
 
-/-- Pull back an `I`-indexed family of objects to an `J`-indexed family, along a function `J → I`.
+/-- Pull back an `I`-indexed family of objects to a `J`-indexed family, along a function `J → I`.
 -/
 @[simps]
 def comap (h : J → I) : (∀ i, C i) ⥤  (∀ j, C (h j)) where

Mathlib/CategoryTheory/Preadditive/Injective.lean

@@ -216,7 +216,7 @@ section EnoughInjectives
 variable [EnoughInjectives C]
 
 /-- `Injective.under X` provides an arbitrarily chosen injective object equipped with
-an monomorphism `Injective.ι : X ⟶  Injective.under X`.
+a monomorphism `Injective.ι : X ⟶  Injective.under X`.
 -/
 def under (X : C) : C :=
   (EnoughInjectives.presentation X).some.J

Mathlib/CategoryTheory/Preadditive/InjectiveResolution.lean

@@ -14,7 +14,7 @@ import Mathlib.Algebra.Homology.Single
 /-!
 # Injective resolutions
 
-A injective resolution `I : InjectiveResolution Z` of an object `Z : C` consists of
+An injective resolution `I : InjectiveResolution Z` of an object `Z : C` consists of
 a `ℕ`-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.
@@ -71,7 +71,7 @@ attribute [inherit_doc InjectiveResolution]
 
 attribute [instance] InjectiveResolution.injective InjectiveResolution.mono
 
-/-- An object admits a injective resolution. -/
+/-- An object admits an injective resolution. -/
 class HasInjectiveResolution (Z : C) : Prop where
   out : Nonempty (InjectiveResolution Z)
 #align category_theory.has_injective_resolution CategoryTheory.HasInjectiveResolution

Mathlib/CategoryTheory/Shift/Basic.lean

@@ -24,7 +24,7 @@ would be the degree `i+n`-th term of `C`.
 ## Main definitions
 * `HasShift`: A typeclass asserting the existence of a shift functor.
 * `shiftEquiv`: When the indexing monoid is a group, then the functor indexed by `n` and `-n` forms
-  an self-equivalence of `C`.
+  a self-equivalence of `C`.
 * `shiftComm`: When the indexing monoid is commutative, then shifts commute as well.
 
 ## Implementation Notes

Mathlib/CategoryTheory/Sites/DenseSubsite.lean

@@ -126,8 +126,8 @@ theorem functorPullback_pushforward_covering [Full G] (H : CoverDense K G) {X :
   · simp
 #align category_theory.cover_dense.functor_pullback_pushforward_covering CategoryTheory.CoverDense.functorPullback_pushforward_covering
 
-/-- (Implementation). Given an hom between the pullbacks of two sheaves, we can whisker it with
-`coyoneda` to obtain an hom between the pullbacks of the sheaves of maps from `X`.
+/-- (Implementation). Given a hom between the pullbacks of two sheaves, we can whisker it with
+`coyoneda` to obtain a hom between the pullbacks of the sheaves of maps from `X`.
 -/
 @[simps!]
 def homOver {ℱ : Dᵒᵖ ⥤ A} {ℱ' : Sheaf K A} (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) (X : A) :
@@ -259,7 +259,7 @@ noncomputable def appIso {ℱ ℱ' : SheafOfTypes.{v} K} (i : G.op ⋙ ℱ.val 
     simp
 #align category_theory.cover_dense.types.app_iso CategoryTheory.CoverDense.Types.appIso
 
-/-- Given an natural transformation `G ⋙ ℱ ⟶ G ⋙ ℱ'` between presheaves of types, where `G` is
+/-- Given a natural transformation `G ⋙ ℱ ⟶ G ⋙ ℱ'` between presheaves of types, where `G` is
 full and cover-dense, and `ℱ'` is a sheaf, we may obtain a natural transformation between sheaves.
 -/
 @[simps]
@@ -273,7 +273,7 @@ noncomputable def presheafHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) : ℱ 
     -- porting note: Lean 3 proof continued with a rewrite but we're done here
 #align category_theory.cover_dense.types.presheaf_hom CategoryTheory.CoverDense.Types.presheafHom
 
-/-- Given an natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of types, where `G` is full
+/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of types, where `G` is full
 and cover-dense, and `ℱ, ℱ'` are sheaves, we may obtain a natural isomorphism between presheaves.
 -/
 @[simps!]
@@ -282,7 +282,7 @@ noncomputable def presheafIso {ℱ ℱ' : SheafOfTypes.{v} K} (i : G.op ⋙ ℱ.
   NatIso.ofComponents (fun X => appIso H i (unop X)) @(presheafHom H i.hom).naturality
 #align category_theory.cover_dense.types.presheaf_iso CategoryTheory.CoverDense.Types.presheafIso
 
-/-- Given an natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of types, where `G` is full
+/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of types, where `G` is full
 and cover-dense, and `ℱ, ℱ'` are sheaves, we may obtain a natural isomorphism between sheaves.
 -/
 @[simps]
@@ -350,7 +350,7 @@ noncomputable def sheafYonedaHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) :
     exact congr_fun ((α.app X).naturality i) x
 #align category_theory.cover_dense.sheaf_yoneda_hom CategoryTheory.CoverDense.sheafYonedaHom
 
-/-- Given an natural transformation `G ⋙ ℱ ⟶ G ⋙ ℱ'` between presheaves of arbitrary category,
+/-- Given a natural transformation `G ⋙ ℱ ⟶ G ⋙ ℱ'` between presheaves of arbitrary category,
 where `G` is full and cover-dense, and `ℱ'` is a sheaf, we may obtain a natural transformation
 between presheaves.
 -/
@@ -360,7 +360,7 @@ noncomputable def sheafHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) : ℱ ⟶ 
     naturality := fun X Y f => yoneda.map_injective (by simpa using α'.naturality f) }
 #align category_theory.cover_dense.sheaf_hom CategoryTheory.CoverDense.sheafHom
 
-/-- Given an natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of arbitrary category,
+/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of arbitrary category,
 where `G` is full and cover-dense, and `ℱ', ℱ` are sheaves,
 we may obtain a natural isomorphism between presheaves.
 -/
@@ -384,7 +384,7 @@ noncomputable def presheafIso {ℱ ℱ' : Sheaf K A} (i : G.op ⋙ ℱ.val ≅ G
   apply asIso (sheafHom H i.hom)
 #align category_theory.cover_dense.presheaf_iso CategoryTheory.CoverDense.presheafIso
 
-/-- Given an natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of arbitrary category,
+/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of arbitrary category,
 where `G` is full and cover-dense, and `ℱ', ℱ` are sheaves,
 we may obtain a natural isomorphism between presheaves.
 -/

Mathlib/CategoryTheory/Sites/Grothendieck.lean

@@ -518,7 +518,7 @@ structure Relation (S : J.Cover X) where
 
 attribute [reassoc] Relation.w
 
-/-- Map a `Arrow` along a refinement `S ⟶ T`. -/
+/-- Map an `Arrow` along a refinement `S ⟶ T`. -/
 @[simps]
 def Arrow.map {S T : J.Cover X} (I : S.Arrow) (f : S ⟶ T) : T.Arrow :=
   ⟨I.Y, I.f, f.le _ I.hf⟩

Mathlib/CategoryTheory/Sites/Subsheaf.lean

@@ -161,7 +161,7 @@ def Subpresheaf.sieveOfSection {U : Cᵒᵖ} (s : F.obj U) : Sieve (unop U) wher
     exact G.map _ hi
 #align category_theory.grothendieck_topology.subpresheaf.sieve_of_section CategoryTheory.GrothendieckTopology.Subpresheaf.sieveOfSection
 
-/-- Given a `F`-section `s` on `U` and a subpresheaf `G`, we may define a family of elements in
+/-- Given an `F`-section `s` on `U` and a subpresheaf `G`, we may define a family of elements in
 `G` consisting of the restrictions of `s` -/
 def Subpresheaf.familyOfElementsOfSection {U : Cᵒᵖ} (s : F.obj U) :
     (G.sieveOfSection s).1.FamilyOfElements G.toPresheaf := fun _ i hi => ⟨F.map i.op s, hi⟩

Mathlib/CategoryTheory/Subobject/Lattice.lean

@@ -513,7 +513,7 @@ section SemilatticeSup
 
 variable [HasImages C] [HasBinaryCoproducts C]
 
-/-- The functorial supremum on `MonoOver A` descends to an supremum on `Subobject A`. -/
+/-- The functorial supremum on `MonoOver A` descends to a supremum on `Subobject A`. -/
 def sup {A : C} : Subobject A ⥤ Subobject A ⥤ Subobject A :=
   ThinSkeleton.map₂ MonoOver.sup
 #align category_theory.subobject.sup CategoryTheory.Subobject.sup