doc: fix typos (#10271)

Fix typos in docstrings and code.

Mathlib/NumberTheory/ArithmeticFunction.lean

@@ -552,7 +552,7 @@ theorem pdiv_apply [GroupWithZero R] (f g : ArithmeticFunction R) (n : ℕ) :
     pdiv f g n = f n / g n := rfl
 
 /-- This result only holds for `DivisionSemiring`s instead of `GroupWithZero`s because zeta takes
-values in ℕ, and hence the coersion requires an `AddMonoidWithOne`. TODO: Generalise zeta -/
+values in ℕ, and hence the coercion requires an `AddMonoidWithOne`. TODO: Generalise zeta -/
 @[simp]
 theorem pdiv_zeta [DivisionSemiring R] (f : ArithmeticFunction R) :
     pdiv f zeta = f := by

Mathlib/Tactic/FunProp/AEMesurable.lean

@@ -70,7 +70,7 @@ attribute [fun_prop]
   Measurable.aemeasurable
 
 
--- Notice that no theorems about measuability of log are used. It is infered from continuity.
+-- Notice that no theorems about measurability of log are used. It is inferred from continuity.
 example : AEMeasurable (fun x => x * (Real.log x) ^ 2 - Real.exp x / x) :=
   by fun_prop
 

Mathlib/Tactic/FunProp/ContDiff.lean

@@ -79,7 +79,7 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace K E]
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace K F]
 
 /-- Original version `ContDiff.differentiable_iteratedDeriv` introduces a new variable `(n:ℕ∞)`
-and `funProp` can't work with such theorem. The theorem should be state where `n` is explicitely
+and `funProp` can't work with such theorem. The theorem should be state where `n` is explicitly
 the smallest possible value i.e. `n=m+1`.
 
 In conjunction with `ContDiff.of_le` we can recover the full power of the original theorem.  -/

Mathlib/Tactic/FunProp/Core.lean

@@ -58,7 +58,7 @@ def unfoldFunHeadRec? (e : Expr) : MetaM (Option Expr) := do
     return none
 
 /-- Synthesize instance of type `type` and
-  1. assign it to `x` if `x` is meta veriable
+  1. assign it to `x` if `x` is meta variable
   2. check it is equal to `x` -/
 def synthesizeInstance (thmId : Origin) (x type : Expr) : MetaM Bool := do
   match (← trySynthInstance type) with
@@ -388,7 +388,7 @@ For example:
  - for `Continuous fun xy => f xy.1 xy.2` this function returns fvar id of `f` and `#[0,1]`
 
 This function is assuming:
- - that `e` is taling about function property `funPropDecl`
+ - that `e` is talking about function property `funPropDecl`
  - the function `f` in `e` can't be expressed as composition of two non-trivial functions
    this means that `f == (← splitLambdaToComp f).1` is true -/
 def isFVarFunProp (funPropDecl : FunPropDecl) (e : Expr) :

Mathlib/Tactic/FunProp/Measurable.lean

@@ -67,7 +67,7 @@ attribute [fun_prop]
 @[fun_prop]
 theorem ContinuousOn.log' : ContinuousOn Real.log {0}ᶜ := ContinuousOn.log (by fun_prop) (by aesop)
 
--- Notice that no theorems about measuability of log are used. It is infered from continuity.
+-- Notice that no theorems about measurability of log are used. It is inferred from continuity.
 example : Measurable (fun x => x * (Real.log x) ^ 2 - Real.exp x / x) :=
   by fun_prop
 

Mathlib/Tactic/FunProp/Mor.lean

@@ -14,7 +14,7 @@ import Mathlib.Tactic.FunProp.ToStd
 
 Function application in normal lean expression looks like `.app f x` but when we work with bundled
 morphism `f` it looks like `.app (.app coe f) x` where `f`. In mathlib the convention is that `coe`
-is aplication of `DFunLike.coe` and this is assumed through out this file. It does not work with
+is application of `DFunLike.coe` and this is assumed through out this file. It does not work with
 Lean's `CoeFun.coe`.
 
 The main difference when working with expression involving morphisms is that the notion the head of
@@ -32,7 +32,7 @@ namespace Meta.FunProp
 
 namespace Mor
 
-/-- Argument of morphism aplication that stores corresponding coercion if necessary -/
+/-- Argument of morphism application that stores corresponding coercion if necessary -/
 structure Arg where
   /-- argument of type `α` -/
   expr : Expr
@@ -126,7 +126,7 @@ def constArity (decl : Name) : MetaM Nat := do
 
 /-- `(fun x => e) a` ==> `e[x/a]`
 
-An example when coersions are involved:
+An example when coercions are involved:
 `(fun x => ⇑((fun y => e) a)) b` ==> `e[y/a, x/b]`. -/
 def headBeta (e : Expr) : Expr :=
   Mor.withApp e fun f xs =>
@@ -140,7 +140,7 @@ end Mor
 
 
 /--
-Split morphism function into composition by specifying over which auguments in the lambda body this
+Split morphism function into composition by specifying over which arguments in the lambda body this
 split should be done.
  -/
 def splitMorToCompOverArgs (e : Expr) (argIds : Array Nat) : MetaM (Option (Expr × Expr)) := do
@@ -199,7 +199,7 @@ def splitMorToCompOverArgs (e : Expr) (argIds : Array Nat) : MetaM (Option (Expr
 
 
 /--
-Split morphism function into composition by specifying over which auguments in the lambda body this
+Split morphism function into composition by specifying over which arguments in the lambda body this
 split should be done.
  -/
 def splitMorToComp (e : Expr) : MetaM (Option (Expr × Expr)) := do

Mathlib/Tactic/FunProp/RefinedDiscrTree.lean

@@ -35,7 +35,7 @@ I document here what is not in the original.
   For example, matching `(1 + 2) + 3` with `add_comm` gives a score of 3,
   since the pattern of commutativity is [⟨Hadd.hadd, 6⟩, *0, *0, *0, *1, *2, *3],
   so matching `⟨Hadd.hadd, 6⟩` gives 1 point,
-  and matching `*0` two times after its first appearence gives another 2 points.
+  and matching `*0` two times after its first appearance gives another 2 points.
   Similarly, matching it with `add_assoc` gives a score of 7.
 
   TODO?: the third type parameter of `Hadd.hadd` is an outparam,
@@ -146,7 +146,7 @@ private def Key.format : Key → Format
 
 instance : ToFormat Key := ⟨Key.format⟩
 
-/-- Return the number of argumets that the `Key` takes. -/
+/-- Return the number of arguments that the `Key` takes. -/
 def Key.arity : Key → Nat
   | .const _ a  => a
   | .fvar _ a   => a

Mathlib/Tactic/FunProp/Theorems.lean

@@ -41,12 +41,12 @@ inductive LambdaTheoremArgs
 
 /-- There are 5(+1) basic lambda theorems
 
-- id      `Continous fun x => x`
-- const   `Continous fun x => y`
-- proj    `Continous fun (f : X → Y) => f x`
-- projDep `Continous fun (f : (x : X) → Y x => f x)`
-- comp    `Continous f → Continous g → Continous fun x => f (g x)`
-- pi      `∀ y, Continuous (f · y) → Continous fun x y => f x y` -/
+- id      `Continuous fun x => x`
+- const   `Continuous fun x => y`
+- proj    `Continuous fun (f : X → Y) => f x`
+- projDep `Continuous fun (f : (x : X) → Y x => f x)`
+- comp    `Continuous f → Continuous g → Continuous fun x => f (g x)`
+- pi      `∀ y, Continuous (f · y) → Continuous fun x y => f x y` -/
 inductive LambdaTheoremType
   | id  | const | proj| projDep | comp  | pi
   deriving Inhabited, BEq, Repr, Hashable
@@ -165,7 +165,7 @@ inductive TheoremForm where
   deriving Inhabited, BEq, Repr
 
 
-/-- theorem about specific function (eiter declared constant or free variable) -/
+/-- theorem about specific function (either declared constant or free variable) -/
 structure FunctionTheorem where
   /-- function property name -/
   funPropName : Name
@@ -232,7 +232,7 @@ structure GeneralTheorem where
   funPropName   : Name
   /-- theorem name -/
   thmName     : Name
-  /-- discreminatory tree keys used to index this theorem -/
+  /-- discriminatory tree keys used to index this theorem -/
   keys        : List RefinedDiscrTree.DTExpr
   /-- priority -/
   priority    : Nat  := eval_prio default
@@ -278,13 +278,13 @@ initialize morTheoremsExt : GeneralTheoremsExt ←
 - lam - theorem about basic lambda calculus terms
 - function - theorem about a specific function(declared or free variable) in specific arguments
 - mor - special theorems talking about bundled morphisms/DFunLike.coe
-- transition - theorems infering one function property from another
+- transition - theorems inferring one function property from another
 
 Examples:
 - lam
 ```
-  theorem Continuous_id : Continous fun x => x
-  theorem Continuous_comp (hf : Continuous f) (hg : Continuous g) : Continous fun x => f (g x)
+  theorem Continuous_id : Continuous fun x => x
+  theorem Continuous_comp (hf : Continuous f) (hg : Continuous g) : Continuous fun x => f (g x)
 ```
 - function
 ```
@@ -302,7 +302,7 @@ Examples:
 - transition - the conclusion has to be in the form `P f` where `f` is a free variable
 ```
   theorem linear_is_continuous [FiniteDimensional ℝ E] {f : E → F} (hf : IsLinearMap 𝕜 f) :
-      Conttinuous f
+      Continuous f
 ```
 -/
 inductive Theorem where
@@ -357,7 +357,7 @@ def getTheoremFromConst (declName : Name) (prio : Nat := eval_prio default) : Me
         keys    := keys
         priority  := prio
       }
-      -- todo: maybe do a little bit more caraful detection of morphism and transition theorems
+      -- todo: maybe do a little bit more careful detection of morphism and transition theorems
       let lastArg := fData.args[fData.args.size-1]!
       if lastArg.coe.isSome then
         return .mor thm

Mathlib/Tactic/FunProp/ToStd.lean

@@ -17,7 +17,7 @@ open Lean Meta
 namespace Meta.FunProp
 set_option autoImplicit true
 
-/-- Check if `a` can be obtained by removing elemnts from `b`. -/
+/-- Check if `a` can be obtained by removing elements from `b`. -/
 def isOrderedSubsetOf {α} [Inhabited α] [DecidableEq α] (a b : Array α) : Bool :=
   Id.run do
   if a.size > b.size then
@@ -96,7 +96,7 @@ def mkProdProj (x : Expr) (i : Nat) (n : Nat) : MetaM Expr := do
   | 0, _ => mkAppM ``Prod.fst #[x]
   | i'+1, n'+1 => mkProdProj (← withTransparency .all <| mkAppM ``Prod.snd #[x]) i' n'
 
-/-- For an elemnt of a product type(of size`n`) `xs` create an array of all possible projections
+/-- For an element of a product type(of size`n`) `xs` create an array of all possible projections
 i.e. `#[xs.1, xs.2.1, xs.2.2.1, ..., xs.2..2]` -/
 def mkProdSplitElem (xs : Expr) (n : Nat) : MetaM (Array Expr) :=
   (Array.range n)

Mathlib/Tactic/FunProp/Types.lean

@@ -12,7 +12,7 @@ import Mathlib.Logic.Function.Basic
 /-!
 ## `funProp`
 
-this file defines enviroment extension for `funProp`
+this file defines environment extension for `funProp`
 -/
 
 
@@ -39,7 +39,7 @@ structure Config where
   /-- Custom discharger to satisfy theorem hypotheses. -/
   disch : Expr → MetaM (Option Expr) := fun _ => pure .none
   /-- Maximal number of transitions between function properties
-  e.g. infering differentiability from linearity -/
+  e.g. inferring differentiability from linearity -/
   maxTransitionDepth := 20
   /-- Stack of used theorem, used to prevent trivial loops. -/
   thmStack    : List Origin := []