doc(Tactic): fix typos (leanprover-community#36521)

Found by `PyCharm`'s code inspection tool.

Author: harahu

Mathlib/Tactic/CategoryTheory/Elementwise.lean

@@ -74,7 +74,7 @@ def elementwiseThms : List Name :=
 /--
 Given an equation `f = g` between morphisms `X ⟶ Y` in a category `C`
 (possibly after a `∀` binder), produce the equation `∀ (x : X), f x = g x` or
-`∀ FC CC _ [ConreteCategory C FC] (x : X), f x = g x` as needed (after the `∀` binder), but
+`∀ FC CC _ [ConcreteCategory C FC] (x : X), f x = g x` as needed (after the `∀` binder), but
 with compositions fully right associated and identities removed.
 
 Returns the proof of the new theorem along with (optionally) a new level metavariable

Mathlib/Tactic/Simproc/ExistsAndEq.lean

@@ -189,7 +189,7 @@ example {α β : Type} (f : β → α) {p : α → Prop} :
   refine Exists.intro (f b) ?_
   -- then we traverse `newBody` and goal simultaneously
   refine And.intro ?_ ?_
-  -- at branches outside the path `h` must concide with goal
+  -- at branches outside the path `h` must coincide with goal
   · replace h := h.left
     exact h
   -- inside path we substitute variables from `fvars` into existential quantifiers.
@@ -341,7 +341,7 @@ example {α β : Type} (f : β → α) {p : α → Prop} :
   have h' := ha
   refine Exists.intro b ?_
   refine And.intro ?_ ?_
-  -- outside the path goal must concide with `h_eq ▸ h'`
+  -- outside the path goal must coincide with `h_eq ▸ h'`
   · replace h' := h'.left
     exact Eq.mp (congrArg (fun t ↦ p t) h_eq) h'
   -- inside the path:

Mathlib/Tactic/Translate/Reorder.lean

@@ -141,7 +141,7 @@ private def fixBinderInfos (bis : List BinderInfo) (e : Expr) : Expr :=
 /-
 In the implementation of `reorderForall` and `reorderLambda` we use metavariables.
 To reorder the arguments in one, we assign it to a reordered new metavariable.
-This trick lets us avoid traversing the expression manually when handling recurive reorderings.
+This trick lets us avoid traversing the expression manually when handling recursive reorderings.
 Instead, we implicitly rely on `instantiateMVars`.
 -/
 mutual
@@ -196,7 +196,7 @@ private def depForallDepth : Expr → Nat
 type `e₁` to type `e₂`. If there is no good guess, default to `[]`.
 The heuristic that we use is to compare the conclusions of `e₁` and `e₂`,
 and to observe which variables are swapped.
-We also apply this heuristic recurisvely in hypotheses. -/
+We also apply this heuristic recursively in hypotheses. -/
 partial def guessReorder (src tgt : Expr) : MetaM Reorder := withReducible do
   let src ← whnf src; let tgt ← whnf tgt
   let depth := depForallDepth src