doc: fix typos in Defs and RecursiveDefs

Manual/Defs.lean

@@ -253,7 +253,7 @@ tag := "automatic-implicit-parameters"
 %%%
 
 
-By default, otherwise-unbound names that occur in signatures are converted into implicit parameters when possible
+By default, otherwise-unbound names that occur in signatures are converted into implicit parameters when possible.
 These parameters are called {deftech}_automatic implicit parameters_.
 This is possible when they are not in the function position of an application and when there is sufficient information available in the signature to infer their type and any ordering constraints on them.
 This process is iterated: if the inferred type for the freshly-inserted implicit parameter has dependencies that are not uniquely determined, then these dependencies are replaced with further implicit parameters.
@@ -392,7 +392,7 @@ AtLeast.add {n✝ : Nat} {i : Fin n✝} (x y : AtLeast i) : AtLeast i
 :::::
 
 Automatic implicit parameter insertion takes place after the insertion of parameters due to {tech}[section variables].
-Parameters that correspond to section variables have the same name as the corresponding variable, even when they do not correspond to a name written directly in the signature, and disabling automatic implicit parameters has no effect the parameters that correspond to section variables.
+Parameters that correspond to section variables have the same name as the corresponding variable, even when they do not correspond to a name written directly in the signature, and disabling automatic implicit parameters has no effect on the parameters that correspond to section variables.
 However, when automatic implicit parameters are enabled, section variable declarations that contain otherwise-unbound variables receive additional section variables that follow the same rules as those for implicit parameters.
 
 Automatic implicit parameters insertion is controlled by two options.

Manual/RecursiveDefs/CoinductivePredicates.lean

@@ -73,7 +73,7 @@ variable {R : α → α → Prop} (a : α) {pred : α → Prop}
 
 The coinductive reasoning principle takes a predicate {lean}`pred`.
 To prove that {lean}`a` is the start of an infinite {lean}`R`-sequence, it suffices to show that {lean}`R` relates each element that satisfies {lean}`pred` to some other such element.
-In other words, it that the presence of an infinite sequence can be demonstrated by providing one:
+In other words, the presence of an infinite sequence can be demonstrated by providing one:
 ```signature
 InfSeq.coinduct (R : α → α → Prop) (pred : α → Prop) :
   (∀ (a : α), pred a → ∃ y, R a y ∧ pred y) →

Manual/RecursiveDefs/PartialFixpoint.lean

@@ -40,12 +40,12 @@ As with the other strategies for defining recursive functions, compiled code use
 The term {tech}_partial fixpoint_ is specific to Lean.
 Functions declared {keywordOf Lean.Parser.Command.declaration}`partial` do not require termination proofs, so long as the type of their return values is inhabited, but they are completely opaque from the perspective of Lean's logic.
 Partial fixpoints, on the other hand, can be rewritten using their defining equations while writing proofs.
-Logically speaking, partial fixpoints are total functions that don't reduce {tech (key := "definitional equality")}[definitionally] when applied, but for which equational rewrite rule are provided.
+Logically speaking, partial fixpoints are total functions that don't reduce {tech (key := "definitional equality")}[definitionally] when applied, but for which equational rewrite rules are provided.
 They are _partial_ in the sense that the defining equation does not necessarily specify a value for all possible arguments.
 
 
 While partial fixpoints do allow functions to be defined that cannot be expressed using structural or well-founded recursion, the technique is also useful in other cases.
-Even in cases where the defining equation fully describes the function's behavior and a termination proof using {ref "well-founded-recursion"}[well-founded recursion] would be possible, it may simply be more convenient to define the function as a partial fixpoint to avoid a having to write a termination proof.
+Even in cases where the defining equation fully describes the function's behavior and a termination proof using {ref "well-founded-recursion"}[well-founded recursion] would be possible, it may simply be more convenient to define the function as a partial fixpoint to avoid having to write a termination proof.
 
 Defining recursive functions as partial fixpoints only occurs when explicitly requested by annotating the definition with {keywordOf Lean.Parser.Command.declaration}`partial_fixpoint`.
 
@@ -191,7 +191,7 @@ tag := "partial-fixpoint-monadic"
 
 
 Defining a function as a partial fixpoint is more powerful if the function's return type is a monad that is an instance of {name}`Lean.Order.MonoBind`, such as {name}`Option`.
-In this case, recursive call are not restricted to tail-positions, but may also occur inside higher-order monadic functions such as {name}`bind` and {name}`List.mapM`.
+In this case, recursive calls are not restricted to tail-positions, but may also occur inside higher-order monadic functions such as {name}`bind` and {name}`List.mapM`.
 
 The set of higher-order functions for which this works is {ref "partial-fixpoint-theory"}[extensible], so no exhaustive list is given here.
 The aspiration is that a monadic recursive function definition that is built using abstract monadic operations like {name}`bind`, but that does not open the abstraction of the monad (e.g. by matching on the {name}`Option` value), is accepted.

Manual/RecursiveDefs/Structural/RecursorExample.lean

@@ -76,7 +76,7 @@ noncomputable def half'' (n : Nat) : Nat :=
       | 0, _ | 1, _ => 0
       | _ + 2, ⟨_, ⟨h, _⟩⟩ => h + 1
 ```
-The function is marked {keywordOf Lean.Parser.Command.declaration}`noncomputable` because the compiler doesn't support generating code for course-of-values recursion, which is intended for reasoning rather that efficient code.
+The function is marked {keywordOf Lean.Parser.Command.declaration}`noncomputable` because the compiler doesn't support generating code for course-of-values recursion, which is intended for reasoning rather than efficient code.
 The kernel can still be used to test the function, however:
 ```lean (name := halfTest2)
 #reduce [0,1,2,3,4,5,6,7,8].map half''

Manual/RecursiveDefs/WF.lean

@@ -798,7 +798,7 @@ This is typically done in two steps:
 
   This theorem uses the {name}`binderNameHint` gadget to preserve a user-chosen binder name, should {lean}`f` be a lambda expression.
 
-By separating the introduction of {name}`List.attach` from the propagation of the introduced assumption, the desired the {lean}`x ∈ xs` assumption is made available to {lean}`f` even in chains such as `(xs.reverse.filter p).map f`.
+By separating the introduction of {name}`List.attach` from the propagation of the introduced assumption, the desired {lean}`x ∈ xs` assumption is made available to {lean}`f` even in chains such as `(xs.reverse.filter p).map f`.
 
 :::