chore: fix many typos (#4983)

These are all doc fixes

Cache/Requests.lean

@@ -124,7 +124,7 @@ end Get
 
 section Put
 
-/-- Formats the config file for `curl`, containing the list of files to be uploades -/
+/-- Formats the config file for `curl`, containing the list of files to be uploaded -/
 def mkPutConfigContent (fileNames : Array String) (token : String) : IO String := do
   let l ← fileNames.data.mapM fun fileName : String => do
     pure s!"-T {(IO.CACHEDIR / fileName).toString}\nurl = {← mkFileURL fileName (some token)}"
@@ -159,7 +159,7 @@ def getGitCommitHash : IO String := do
   | _ => throw $ IO.userError "Invalid format for the return of `git log -1`"
 
 /--
-Sends a commit file to the server, containing the hashes of the respective commited files.
+Sends a commit file to the server, containing the hashes of the respective committed files.
 
 The file name is the current Git hash and the `c/` prefix means that it's a commit file.
 -/

Mathlib/Algebra/Abs.lean

@@ -46,15 +46,15 @@ class Abs (α : Type _) where
 
 export Abs (abs)
 
-/-- The positive part of an element admiting a decomposition into positive and negative parts.
+/-- The positive part of an element admitting a decomposition into positive and negative parts.
 -/
 class PosPart (α : Type _) where
   /-- The positive part function. -/
   pos : α → α
 
 #align has_pos_part PosPart
 
-/-- The negative part of an element admiting a decomposition into positive and negative parts.
+/-- The negative part of an element admitting a decomposition into positive and negative parts.
 -/
 class NegPart (α : Type _) where
   /-- The negative part function. -/

Mathlib/Algebra/CharP/Invertible.lean

@@ -27,7 +27,7 @@ section Field
 
 variable [Field K]
 
-/-- A natural number `t` is invertible in a field `K` if the charactistic of `K` does not divide
+/-- A natural number `t` is invertible in a field `K` if the characteristic of `K` does not divide
 `t`. -/
 def invertibleOfRingCharNotDvd {t : ℕ} (not_dvd : ¬ringChar K ∣ t) : Invertible (t : K) :=
   invertibleOfNonzero fun h => not_dvd ((ringChar.spec K t).mp h)
@@ -38,7 +38,7 @@ theorem not_ringChar_dvd_of_invertible {t : ℕ} [Invertible (t : K)] : ¬ringCh
   exact nonzero_of_invertible (t : K)
 #align not_ring_char_dvd_of_invertible not_ringChar_dvd_of_invertible
 
-/-- A natural number `t` is invertible in a field `K` of charactistic `p` if `p` does not divide
+/-- A natural number `t` is invertible in a field `K` of characteristic `p` if `p` does not divide
 `t`. -/
 def invertibleOfCharPNotDvd {p : ℕ} [CharP K p] {t : ℕ} (not_dvd : ¬p ∣ t) : Invertible (t : K) :=
   invertibleOfNonzero fun h => not_dvd ((CharP.cast_eq_zero_iff K p t).mp h)

Mathlib/Algebra/DirectSum/Ring.lean

@@ -66,7 +66,7 @@ instances for:
 * `A : ι → Subgroup S`:
   `DirectSum.GSemiring.ofAddSubgroups`, `DirectSum.GCommSemiring.ofAddSubgroups`.
 * `A : ι → Submodule S`:
-  `DirectSum.GSemiring.ofSubmodules`, `DirectSum.GcommSemiring.ofSubmodules`.
+  `DirectSum.GSemiring.ofSubmodules`, `DirectSum.GCommSemiring.ofSubmodules`.
 
 If `CompleteLattice.independent (Set.range A)`, these provide a gradation of `⨆ i, A i`, and the
 mapping `⨁ i, A i →+ ⨆ i, A i` can be obtained as

Mathlib/Algebra/GradedMonoid.lean

@@ -170,19 +170,19 @@ theorem gnpowRec_succ (n : ℕ) (a : GradedMonoid A) :
 
 end GMonoid
 
-/-- A tactic to for use as an optional value for `Gmonoid.gnpow_zero'' -/
+/-- A tactic to for use as an optional value for `GMonoid.gnpow_zero'`. -/
 macro "apply_gmonoid_gnpowRec_zero_tac" : tactic => `(tactic| apply GMonoid.gnpowRec_zero)
-/-- A tactic to for use as an optional value for `Gmonoid.gnpow_succ'' -/
+/-- A tactic to for use as an optional value for `GMonoid.gnpow_succ'`. -/
 macro "apply_gmonoid_gnpowRec_succ_tac" : tactic => `(tactic| apply GMonoid.gnpowRec_succ)
 
 /-- A graded version of `Monoid`
 
 Like `Monoid.npow`, this has an optional `GMonoid.gnpow` field to allow definitional control of
 natural powers of a graded monoid. -/
 class GMonoid [AddMonoid ι] extends GMul A, GOne A where
-  /-- Muliplication by `one` on the left is the identity -/
+  /-- Multiplication by `one` on the left is the identity -/
   one_mul (a : GradedMonoid A) : 1 * a = a
-  /-- Muliplication by `one` on the right is the identity -/
+  /-- Multiplication by `one` on the right is the identity -/
   mul_one (a : GradedMonoid A) : a * 1 = a
   /-- Multiplication is associative -/
   mul_assoc (a b c : GradedMonoid A) : a * b * c = a * (b * c)

Mathlib/Algebra/Group/Prod.lean

@@ -592,7 +592,7 @@ variable {M' : Type _} {N' : Type _} [MulOneClass M'] [MulOneClass N'] [MulOneCl
   (f : M →* M') (g : N →* N')
 
 /-- `prod.map` as a `MonoidHom`. -/
-@[to_additive prodMap "`prod.map` as an `AddHonoidHom`"]
+@[to_additive prodMap "`prod.map` as an `AddMonoidHom`."]
 def prodMap : M × N →* M' × N' :=
   (f.comp (fst M N)).prod (g.comp (snd M N))
 #align monoid_hom.prod_map MonoidHom.prodMap

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -54,7 +54,7 @@ class MulZeroClass (M₀ : Type u) extends Mul M₀, Zero M₀ where
 
 /-- A mixin for left cancellative multiplication by nonzero elements. -/
 class IsLeftCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
-  /-- Multiplicatin by a nonzero element is left cancellative. -/
+  /-- Multiplication by a nonzero element is left cancellative. -/
   protected mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c
 #align is_left_cancel_mul_zero IsLeftCancelMulZero
 

Mathlib/Algebra/Homology/LocalCohomology.lean

@@ -104,7 +104,7 @@ in an ideal `J`, `local_cohomology` and `local_cohomology.of_self_le_radical`.
 
 TODO: Show that any functor cofinal with `I` gives the same result.
  -/
-/-- `local_cohomology.of_diagram I i` is the the functor sending a module `M` over a commutative
+/-- `local_cohomology.of_diagram I i` is the functor sending a module `M` over a commutative
 ring `R` to the direct limit of `Ext^i(R/J, M)`, where `J` ranges over a collection of ideals
 of `R`, represented as a functor `I`. -/
 def ofDiagram (I : D ⥤ Ideal R) (i : ℕ) : ModuleCat.{max u v} R ⥤ ModuleCat.{max u v} R :=

Mathlib/Algebra/Module/Hom.lean

@@ -18,7 +18,7 @@ This file defines instances for `Module`, `MulAction` and related structures on
 These are analogous to the instances in `Algebra.Module.Pi`, but for bundled instead of unbundled
 functions.
 
-We also define bundled versions of `(c • ·)` and `(· • ·)` as `AddMonoidhom.smulLeft` and
+We also define bundled versions of `(c • ·)` and `(· • ·)` as `AddMonoidHom.smulLeft` and
 `AddMonoidHom.smul`, respectively.
 -/
 

Mathlib/Algebra/Module/Torsion.lean

@@ -491,7 +491,7 @@ theorem torsionBySet_isInternal {p : ι → Ideal R}
     (CompleteLattice.independent_iff_supIndep.mpr <| supIndep_torsionBySet_ideal hp)
     (by
       apply (iSup_subtype'' ↑S fun i => torsionBySet R M <| p i).trans
-      -- Porting note: timesout if we change apply below to <|
+      -- Porting note: times out if we change apply below to <|
       apply (iSup_torsionBySet_ideal_eq_torsionBySet_iInf hp).trans <|
         (Module.isTorsionBySet_iff_torsionBySet_eq_top _).mp hM)
 #align submodule.torsion_by_set_is_internal Submodule.torsionBySet_isInternal

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

@@ -22,15 +22,15 @@ universe u
 
 variable {α : Type u}
 
-/-- An `OrderCommMonoid` with one-sided 'division' in the sense that
+/-- An `OrderedCommMonoid` with one-sided 'division' in the sense that
 if `a ≤ b`, there is some `c` for which `a * c = b`. This is a weaker version
 of the condition on canonical orderings defined by `CanonicallyOrderedMonoid`. -/
 class ExistsMulOfLE (α : Type u) [Mul α] [LE α] : Prop where
   /-- For `a ≤ b`, `a` left divides `b` -/
   exists_mul_of_le : ∀ {a b : α}, a ≤ b → ∃ c : α, b = a * c
 #align has_exists_mul_of_le ExistsMulOfLE
 
-/-- An `OrderAddCommMonoid` with one-sided 'subtraction' in the sense that
+/-- An `OrderedAddCommMonoid` with one-sided 'subtraction' in the sense that
 if `a ≤ b`, then there is some `c` for which `a + c = b`. This is a weaker version
 of the condition on canonical orderings defined by `CanonicallyOrderedAddMonoid`. -/
 class ExistsAddOfLE (α : Type u) [Add α] [LE α] : Prop where

Mathlib/AlgebraicTopology/SplitSimplicialObject.lean

@@ -187,8 +187,8 @@ def epiComp {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} (A : IndexSet Δ₁) (p : Δ
 
 variable {Δ' : SimplexCategoryᵒᵖ} (θ : Δ ⟶ Δ')
 
-/-- When `A : index_set Δ` and `θ : Δ → Δ'` is a morphism in `simplex_categoryᵒᵖ`,
-an element in `index_set Δ'` can be defined by using the epi-mono factorisation
+/-- When `A : IndexSet Δ` and `θ : Δ → Δ'` is a morphism in `SimplexCategoryᵒᵖ`,
+an element in `IndexSet Δ'` can be defined by using the epi-mono factorisation
 of `θ.unop ≫ A.e`. -/
 def pull : IndexSet Δ' :=
   mk (factorThruImage (θ.unop ≫ A.e))
@@ -244,7 +244,7 @@ variable [HasFiniteCoproducts C]
 --porting note: removed @[nolint has_nonempty_instance]
 /-- A splitting of a simplicial object `X` consists of the datum of a sequence
 of objects `N`, a sequence of morphisms `ι : N n ⟶ X _[n]` such that
-for all `Δ : SimplexCategoryhᵒᵖ`, the canonical map `Splitting.map X ι Δ`
+for all `Δ : SimplexCategoryᵒᵖ`, the canonical map `Splitting.map X ι Δ`
 is an isomorphism. -/
 structure Splitting (X : SimplicialObject C) where
   N : ℕ → C

Mathlib/Analysis/Calculus/LHopital.lean

@@ -14,7 +14,7 @@ import Mathlib.Analysis.Calculus.Deriv.Inv
 /-!
 # L'Hôpital's rule for 0/0 indeterminate forms
 
-In this file, we prove several forms of "L'Hopital's rule" for computing 0/0
+In this file, we prove several forms of "L'Hôpital's rule" for computing 0/0
 indeterminate forms. The proof of `HasDerivAt.lhopital_zero_right_on_Ioo`
 is based on the one given in the corresponding
 [Wikibooks](https://en.wikibooks.org/wiki/Calculus/L%27H%C3%B4pital%27s_Rule)

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -1985,7 +1985,7 @@ The connection to the subobject spelling is shown in `orthogonalFamily_iff_pairw
 
 This definition is less lightweight, but allows for better definitional properties when the inner
 product space structure on each of the submodules is important -- for example, when considering
-their Hilbert sum (`Pilp V 2`).  For example, given an orthonormal set of vectors `v : ι → E`,
+their Hilbert sum (`PiLp V 2`).  For example, given an orthonormal set of vectors `v : ι → E`,
 we have an associated orthogonal family of one-dimensional subspaces of `E`, which it is convenient
 to be able to discuss using `ι → 𝕜` rather than `Π i : ι, span 𝕜 (v i)`. -/
 def OrthogonalFamily (G : ι → Type _) [∀ i, NormedAddCommGroup (G i)]

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -28,7 +28,7 @@ between `E` and `EuclideanSpace 𝕜 ι`. Then `stdOrthonormalBasis` shows that
 always exists if `E` is finite dimensional. We provide language for converting between a basis
 that is orthonormal and an orthonormal basis (e.g. `Basis.toOrthonormalBasis`). We show that
 orthonormal bases for each summand in a direct sum of spaces can be combined into an orthonormal
-basis for the the whole sum in `DirectSum.IsInternal.subordinateOrthonormalBasis`. In
+basis for the whole sum in `DirectSum.IsInternal.subordinateOrthonormalBasis`. In
 the last section, various properties of matrices are explored.
 
 ## Main definitions

Mathlib/Analysis/NormedSpace/PiLp.lean

@@ -28,7 +28,7 @@ We give instances of this construction for emetric spaces, metric spaces, normed
 spaces.
 
 To avoid conflicting instances, all these are defined on a copy of the original Π-type, named
-`PiLp p α`. The assumpion `[Fact (1 ≤ p)]` is required for the metric and normed space instances.
+`PiLp p α`. The assumption `[Fact (1 ≤ p)]` is required for the metric and normed space instances.
 
 We ensure that the topology, bornology and uniform structure on `PiLp p α` are (defeq to) the
 product topology, product bornology and product uniformity, to be able to use freely continuity

Mathlib/Analysis/NormedSpace/Spectrum.lean

@@ -398,7 +398,7 @@ protected theorem nonempty : (spectrum ℂ a).Nonempty := by
   have H₀ : resolventSet ℂ a = Set.univ := by rwa [spectrum, Set.compl_empty_iff] at h
   have H₁ : Differentiable ℂ fun z : ℂ => resolvent a z := fun z =>
     (hasDerivAt_resolvent (H₀.symm ▸ Set.mem_univ z : z ∈ resolventSet ℂ a)).differentiableAt
-  /- The norm of the resolvent is small for all sufficently large `z`, and by compactness and
+  /- The norm of the resolvent is small for all sufficiently large `z`, and by compactness and
     continuity it is bounded on the complement of a large ball, thus uniformly bounded on `ℂ`.
     By Liouville's theorem `fun z ↦ resolvent a z` is constant. -/
   have H₂ := norm_resolvent_le_forall (𝕜 := ℂ) a
@@ -413,7 +413,7 @@ protected theorem nonempty : (spectrum ℂ a).Nonempty := by
     refine' Or.elim (em (‖w‖ ≤ R)) (fun hw => _) fun hw => _
     · exact (hC w (mem_closedBall_zero_iff.mpr hw)).trans (le_max_left _ _)
     · exact (hR w (not_le.mp hw).le).trans (le_max_right _ _)
-  -- `resolvent a 0 = 0`, which is a contradition because it isn't a unit.
+  -- `resolvent a 0 = 0`, which is a contradiction because it isn't a unit.
   have H₅ : resolvent a (0 : ℂ) = 0 := by
     refine' norm_eq_zero.mp (le_antisymm (le_of_forall_pos_le_add fun ε hε => _) (norm_nonneg _))
     rcases H₂ ε hε with ⟨R, _, hR⟩

Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean

@@ -1,6 +1,6 @@
 /-
 Copyright (c) 2022 Jireh Loreaux. All rights reserved.
-Reeased under Apache 2.0 license as described in the file LICENSE.
+Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 
 ! This file was ported from Lean 3 source module analysis.normed_space.star.gelfand_duality
@@ -52,7 +52,7 @@ and even an equivalence between C⋆-algebras.
 * Conclude using the previous fact that the functors `C(⬝, ℂ)` and `characterSpace ℂ ⬝` along with
   the canonical homeomorphisms described above constitute a natural contravariant equivalence of
   the categories of compact Hausdorff spaces (with continuous maps) and commutative unital
-  C⋆-algebras (with unital ⋆-algebra homomoprhisms); this is known as **Gelfand duality**.
+  C⋆-algebras (with unital ⋆-algebra homomorphisms); this is known as **Gelfand duality**.
 
 ## Tags
 
@@ -91,7 +91,7 @@ theorem Ideal.toCharacterSpace_apply_eq_zero_of_mem {a : A} (ha : a ∈ I) :
   exact Set.eq_of_mem_singleton (Set.singleton_nonempty (0 : ℂ)).some_mem
 #align ideal.to_character_space_apply_eq_zero_of_mem Ideal.toCharacterSpace_apply_eq_zero_of_mem
 
-/-- If `a : A` is not a unit, then some character takes the value zero at `a`. This is equivlaent
+/-- If `a : A` is not a unit, then some character takes the value zero at `a`. This is equivalent
 to `gelfandTransform ℂ A a` takes the value zero at some character. -/
 theorem WeakDual.CharacterSpace.exists_apply_eq_zero {a : A} (ha : ¬IsUnit a) :
     ∃ f : characterSpace ℂ A, f a = 0 := by

Mathlib/CategoryTheory/Abelian/Exact.lean

@@ -366,7 +366,7 @@ variable [PreservesFiniteLimits L] [PreservesFiniteColimits L]
 
 /-- A functor preserving finite limits and finite colimits preserves exactness. The converse
 result is also true, see `Functor.preservesFiniteLimitsOfMapExact` and
-`Functor.preservesFiniteCoimitsOfMapExact`. -/
+`Functor.preservesFiniteColimitsOfMapExact`. -/
 theorem map_exact {X Y Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) (e1 : Exact f g) :
     Exact (L.map f) (L.map g) := by
   let hcoker := isColimitOfHasCokernelOfPreservesColimit L f

Mathlib/CategoryTheory/Bicategory/Basic.lean

@@ -38,7 +38,7 @@ require this functor directly. Instead, it requires the whiskering functions. Fo
 2-morphism `whiskerLeft f η : f ≫ g ⟶ f ≫ h`. Similarly, for a 2-morphism `η : f ⟶ g`
 between 1-morphisms `f g : a ⟶ b` and a 1-morphism `f : b ⟶ c`, there is a 2-morphism
 `whiskerRight η h : f ≫ h ⟶ g ≫ h`. These satisfy the exchange law
-`whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerReft g θ`,
+`whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ`,
 which is required as an axiom in the definition here.
 -/
 

Mathlib/CategoryTheory/Bicategory/NaturalTransformation.lean

@@ -199,7 +199,7 @@ def vcomp (η : OplaxNatTrans F G) (θ : OplaxNatTrans G H) : OplaxNatTrans F H
       whiskerLeft_rightUnitor_inv, Iso.hom_inv_id, comp_id, whiskerRight_naturality_id_assoc,
       leftUnitor_whiskerRight, triangle_assoc, inv_hom_whiskerRight_assoc, whiskerRight_comp]
   naturality_naturality {_ _ _ _} _ := by
-    -- Porting note: this used to be automatic via `tidy`, wich did `intros, simp`
+    -- Porting note: this used to be automatic via `tidy`, which did `intros, simp`
     simp only [whiskerRight_comp, assoc, Iso.hom_inv_id_assoc,
       whiskerRight_naturality_naturality_assoc, Iso.inv_hom_id_assoc,
       whiskerLeft_naturality_naturality_assoc, comp_whiskerLeft]
@@ -286,7 +286,7 @@ end
 def vcomp (Γ : Modification η θ) (Δ : Modification θ ι) : Modification η ι where
   app a := Γ.app a ≫ Δ.app a
   naturality := by
-    -- Porting note: this used to be automatic via `tidy`, wich did `intros, simp`
+    -- Porting note: this used to be automatic via `tidy`, which did `intros, simp`
     intros
     simp only [whiskerLeft_comp, assoc, naturality, naturality_assoc, comp_whiskerRight]
 #align category_theory.oplax_nat_trans.modification.vcomp CategoryTheory.OplaxNatTrans.Modification.vcomp

Mathlib/CategoryTheory/Equivalence.lean

@@ -18,7 +18,7 @@ import Mathlib.Tactic.CategoryTheory.Slice
 
 An equivalence of categories `C` and `D` is a pair of functors `F : C ⥤ D` and `G : D ⥤ C` such
 that `η : 𝟭 C ≅ F ⋙ G` and `ε : G ⋙ F ≅ 𝟭 D`. In many situations, equivalences are a better
-notion of "sameness" of categories than the stricter isomorphims of categories.
+notion of "sameness" of categories than the stricter isomorphism of categories.
 
 Recall that one way to express that two functors `F : C ⥤ D` and `G : D ⥤ C` are adjoint is using
 two natural transformations `η : 𝟭 C ⟶ F ⋙ G` and `ε : G ⋙ F ⟶ 𝟭 D`, called the unit and the

Mathlib/CategoryTheory/GlueData.lean

@@ -338,7 +338,7 @@ theorem diagramIso_inv_app_right (i : D.J) :
 
 variable [HasMulticoequalizer D.diagram] [PreservesColimit D.diagram.multispan F]
 
--- porting note: commented out omi
+-- porting note: commented out omit
 -- omit H
 
 theorem hasColimit_multispan_comp : HasColimit (D.diagram.multispan ⋙ F) :=

Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean

@@ -1032,7 +1032,7 @@ def Cone.ofPullbackCone {F : WalkingCospan ⥤ C} (t : PullbackCone (F.map inl)
 
 /-- This is a helper construction that can be useful when verifying that a category has all
     pushout. Given `F : WalkingSpan ⥤ C`, which is really the same as
-    `span (F.map fst) (F.mal snd)`, and a pushout cocone on `F.map fst` and `F.map snd`,
+    `span (F.map fst) (F.map snd)`, and a pushout cocone on `F.map fst` and `F.map snd`,
     we get a cocone on `F`.
 
     If you're thinking about using this, have a look at `hasPushouts_of_hasColimit_span`, which

Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean

@@ -204,7 +204,7 @@ theorem IsTerminal.subsingleton_to (hI : IsTerminal I) {A : C} : Subsingleton (I
 
 variable {J : Type v} [SmallCategory J]
 
-/-- If all but one object in a diagram is strict terminal, the the limit is isomorphic to the
+/-- If all but one object in a diagram is strict terminal, then the limit is isomorphic to the
 said object via `limit.π`. -/
 theorem limit_π_isIso_of_is_strict_terminal (F : J ⥤ C) [HasLimit F] (i : J)
     (H : ∀ (j) (_ : j ≠ i), IsTerminal (F.obj j)) [Subsingleton (i ⟶ i)] : IsIso (limit.π F i) := by

Mathlib/CategoryTheory/Limits/Shapes/Types.lean

@@ -569,7 +569,7 @@ def pullbackLimitCone (f : X ⟶ Z) (g : Y ⟶ Z) : Limits.LimitCone (cospan f g
 #align category_theory.limits.types.pullback_limit_cone CategoryTheory.Limits.Types.pullbackLimitCone
 
 /-- The pullback cone given by the instance `HasPullbacks (Type u)` is isomorphic to the
-explicit pullback cone given by `pullbacklimitCone`.
+explicit pullback cone given by `pullbackLimitCone`.
 -/
 noncomputable def pullbackConeIsoPullback : limit.cone (cospan f g) ≅ pullbackCone f g :=
   (limit.isLimit _).uniqueUpToIso (pullbackLimitCone f g).isLimit

Mathlib/CategoryTheory/Monad/Adjunction.lean

@@ -94,7 +94,7 @@ def adjToComonadIso (G : Comonad C) : G.adj.toComonad ≅ G :=
 
 end Adjunction
 
-/-- Gven any adjunction `L ⊣ R`, there is a comparison functor `CategoryTheory.Monad.comparison R`
+/-- Given any adjunction `L ⊣ R`, there is a comparison functor `CategoryTheory.Monad.comparison R`
 sending objects `Y : D` to Eilenberg-Moore algebras for `L ⋙ R` with underlying object `R.obj X`.
 
 We later show that this is full when `R` is full, faithful when `R` is faithful,
@@ -142,7 +142,7 @@ instance (T : Monad C) : EssSurj (Monad.comparison T.adj) where
     ⟨Monad.Algebra.isoMk (Iso.refl _)⟩⟩
 
 /--
-Gven any adjunction `L ⊣ R`, there is a comparison functor `CategoryTheory.Comonad.comparison L`
+Given any adjunction `L ⊣ R`, there is a comparison functor `CategoryTheory.Comonad.comparison L`
 sending objects `X : C` to Eilenberg-Moore coalgebras for `L ⋙ R` with underlying object
 `L.obj X`.
 -/