doc: fix some typos

assinged -> assigned
collction -> collection

src/Lean/Elab/Tactic/Basic.lean

@@ -342,7 +342,7 @@ def ensureHasNoMVars (e : Expr) : TacticM Unit := do
   if e.hasExprMVar then
     throwError "tactic failed, resulting expression contains metavariables{indentExpr e}"
 
-/-- Close main goal using the given expression. If `checkUnassigned == true`, then `val` must not contain unassinged metavariables. -/
+/-- Close main goal using the given expression. If `checkUnassigned == true`, then `val` must not contain unassigned metavariables. -/
 def closeMainGoal (val : Expr) (checkUnassigned := true): TacticM Unit := do
   if checkUnassigned then
     ensureHasNoMVars val

src/Lean/Environment.lean

@@ -101,7 +101,7 @@ the kernel is to type check these declarations and refuse type incorrect ones. T
 kernel does not allow declarations containing metavariables and/or free variables
 to be added to an environment. Environments are never destructively updated.
 
-The environment also contains a collction of extensions. For example, the `simp` theorems
+The environment also contains a collection of extensions. For example, the `simp` theorems
 declared by users are stored in an environment extension. Users can declare new extensions
 using meta-programming.
 -/

src/Lean/Meta/SynthInstance.lean

@@ -324,7 +324,7 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array
 def tryResolve (mvar : Expr) (inst : Expr) : MetaM (Option (MetavarContext × List Expr)) := do
   let mvar ← instantiateMVars mvar
   if !(← hasAssignableMVar mvar) then
-    /- The metavariable `mvar` may have been assinged when solving typing constraints.
+    /- The metavariable `mvar` may have been assigned when solving typing constraints.
        This may happen when a local instance type depends on other local instances.
        For example, in Mathlib, we have
        ```