doc: apply David's and Mario's suggestions

Co-authored-by: David Thrane Christiansen <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>

src/Init/Data/Repr.lean

@@ -22,7 +22,7 @@ input value.
 class Repr (α : Type u) where
   /--
   Turn a value of type `α` into `Format` at a given precedence. The precedence value can be used
-  to avoid parenthesis if they are not necessary.
+  to avoid parentheses if they are not necessary.
   -/
   reprPrec : α → Nat → Format
 

src/Init/WF.lean

@@ -18,8 +18,8 @@ universe u v
 inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop where
   /--
   A value is accessible if for all `y` such that `r y x`, `y` is also accessible.
-  Note that if there exists no `y` such that `r y x`, `x` is accessible, such an `x` is called a
-  base case.
+  Note that if there exists no `y` such that `r y x`, then `x` is accessible. Such an `x` is called a
+  _base case_.
   -/
   | intro (x : α) (h : (y : α) → r y x → Acc r y) : Acc r x
 
@@ -46,8 +46,8 @@ end Acc
 A relation `r` is `WellFounded` if all elements of `α` are accessible within `r`.
 If a relation is `WellFounded`, it does not allow for an infinite descent along the relation.
 
-This is used to prove that a recursive function, where the arguments of the recursive calls
-decrease according to a well founded relation, terminates.
+If the arguments of the recursive calls in a function definition decrease according to
+a well founded relation, then the function terminates.
 -/
 inductive WellFounded {α : Sort u} (r : α → α → Prop) : Prop where
   | intro (h : ∀ a, Acc r a) : WellFounded r

src/Lean/Meta/Basic.lean

@@ -303,20 +303,20 @@ structure Context where
 
 /--
 The `MetaM` monad is a core component of Lean's metaprogramming framework, facilitating the
-construction and manipulation, of expressions (`Lean.Expr`) within Lean.
+construction and manipulation of expressions (`Lean.Expr`) within Lean.
 
 It builds on top of `CoreM` and additionally provides:
 - A `LocalContext` for managing free variables.
-- A `MetavarContext` for managing meta variables.
-- A `Cache` for chaching results of the key `MetaM` operations.
+- A `MetavarContext` for managing metavariables.
+- A `Cache` for caching results of the key `MetaM` operations.
 
 The key operations provided by `MetaM` are:
-- `inferType`, it attempts to automatically infer the type of a given expression.
-- `whnf`, it reduces an expression to the point where the outermost part is no longer reducible
+- `inferType`, which attempts to automatically infer the type of a given expression.
+- `whnf`, which reduces an expression to the point where the outermost part is no longer reducible
   but the inside may still contain unreduced expression.
-- `isDefEq`, it determines whether two expressions are definitionally equal, possibly assigning
+- `isDefEq`, which determines whether two expressions are definitionally equal, possibly assigning
   meta variables in the process.
-- `forallTelescope` and `lambdaTelescope`, they make it possible to automatically move into
+- `forallTelescope` and `lambdaTelescope`, which make it possible to automatically move into
   (nested) binders while updating the local context.
 
 The following is a small example that demonstrates how to obtain and manipulate the type of a