doc: fix typos

src/Lean/Expr.lean

@@ -774,8 +774,8 @@ instance : BEq Expr where
   beq := Expr.eqv
 
 /--
-Return true iff `a` and `b` are equal.
-Binder names and annotations are taking into account.
+Return `true` iff `a` and `b` are equal.
+Binder names and annotations are taken into account.
 -/
 @[extern "lean_expr_equal"]
 opaque equal (a : @& Expr) (b : @& Expr) : Bool
@@ -831,7 +831,7 @@ def isConst : Expr → Bool
   | _        => false
 
 /--
-Return `true` if the given expression is a constant of the give name.
+Return `true` if the given expression is a constant of the given name.
 Examples:
 - `` (.const `Nat []).isConstOf `Nat `` is `true`
 - `` (.const `Nat []).isConstOf `False `` is `false`

src/Lean/Meta/CollectMVars.lean

@@ -28,12 +28,12 @@ partial def collectMVars (e : Expr) : StateRefT CollectMVars.State MetaM Unit :=
     | none   => pure ()
     | some d => collectMVars (mkMVar d.mvarIdPending)
 
-/-- Return metavariables in occurring the given expression. See `collectMVars` -/
+/-- Return metavariables occurring in the given expression. See `collectMVars` -/
 def getMVars (e : Expr) : MetaM (Array MVarId) := do
   let (_, s) ← (collectMVars e).run {}
   pure s.result
 
-/-- Similar to getMVars, but removes delayed assignments. -/
+/-- Similar to `getMVars`, but removes delayed assignments. -/
 def getMVarsNoDelayed (e : Expr) : MetaM (Array MVarId) := do
   let mvarIds ← getMVars e
   mvarIds.filterM fun mvarId => not <$> mvarId.isDelayedAssigned