diff --git a/library/init/lean/path.lean b/library/init/lean/path.lean
index 3f23f61e3b..86d3aed061 100644
--- a/library/init/lean/path.lean
+++ b/library/init/lean/path.lean
@@ -23,7 +23,7 @@ do curr ← IO.realPath ".";
 constant searchPathRef : IO.Ref (Array String) := default _
 
 def setSearchPath (s : List String) : IO Unit :=
-do s ← s.mmap (fun p => IO.realPath (System.FilePath.normalizePathSeparators p));
+do s ← s.mmap (fun p => IO.realPath (System.FilePath.normalizePath p));
    searchPathRef.set s.toArray
 
 def setSearchPathFromString (s : String) : IO Unit :=
@@ -64,7 +64,7 @@ match path with
     setSearchPath [path, curr]
 
 def findFile (fname : String) : IO (Option String) :=
-do let fname := System.FilePath.normalizePathSeparators fname;
+do let fname := System.FilePath.normalizePath fname;
    paths ← searchPathRef.get;
    paths.mfind $ fun path => do
      let path := path ++ pathSep;
@@ -96,7 +96,7 @@ def findLean (modName : Name) : IO String :=
 findLeanFile modName "lean"
 
 def findAtSearchPath (fname : String) : IO String :=
-do fname ← IO.realPath (System.FilePath.normalizePathSeparators fname);
+do fname ← IO.realPath (System.FilePath.normalizePath fname);
    paths ← searchPathRef.get;
    match paths.find (fun path => if path.isPrefixOf fname then some path else none) with
    | some r => pure r
@@ -106,7 +106,7 @@ do fname ← IO.realPath (System.FilePath.normalizePathSeparators fname);
 def moduleNameOfFileName (fname : String) : IO Name :=
 do
 path  ← findAtSearchPath fname;
-fname ← IO.realPath (System.FilePath.normalizePathSeparators fname);
+fname ← IO.realPath (System.FilePath.normalizePath fname);
 let fnameSuffix := fname.drop path.length;
 let fnameSuffix := if fnameSuffix.get 0 == pathSeparator then fnameSuffix.drop 1 else fnameSuffix;
 if path ++ pathSep ++ fnameSuffix != fname then
diff --git a/library/init/system/filepath.lean b/library/init/system/filepath.lean
index 34f860ccea..0da3c679b4 100644
--- a/library/init/system/filepath.lean
+++ b/library/init/system/filepath.lean
@@ -27,13 +27,19 @@ if isWindows then ';' else ':'
 def extSeparator : Char :=
 '.'
 
-def normalizePathSeparators (fname : String) : String :=
-if pathSeparators.length == 1 then fname
+/-- Case-insensitive file system -/
+def isCaseInsensitive : Bool :=
+isWindows || isOSX
+
+def normalizePath (fname : String) : String :=
+if pathSeparators.length == 1 && !isCaseInsensitive then fname
 else fname.map (fun c =>
-  if pathSeparators.any (fun c' => c == c') then pathSeparator else c)
+  if pathSeparators.any (fun c' => c == c') then pathSeparator
+  else if isCaseInsensitive then c.toLower
+  else c)
 
 def dirName (fname : String) : String :=
-let fname := normalizePathSeparators fname;
+let fname := normalizePath fname;
 match fname.revPosOf pathSeparator with
 | none => "."
 | some pos => { Substring . str := fname, startPos := 0, stopPos := pos }.toString