diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean
index 88a013c49040..aff17800c028 100644
--- a/src/Lean/Elab/Import.lean
+++ b/src/Lean/Elab/Import.lean
@@ -39,7 +39,7 @@ def parseImports (input : String) (fileName : Option String := none) : IO (Array
 def printImports (input : String) (fileName : Option String) : IO Unit := do
   let (deps, _, _) ← parseImports input fileName
   for dep in deps do
-    let fname ← findOLean dep.module
+    let fname ← findOLean (checkExists := false) dep.module
     IO.println fname
 
 end Lean.Elab
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index c50b161f625e..e7a7322bf64a 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -794,8 +794,6 @@ partial def importModulesCore (imports : Array Import) : ImportStateM Unit := do
       continue
     modify fun s => { s with moduleNameSet := s.moduleNameSet.insert i.module }
     let mFile ← findOLean i.module
-    unless (← mFile.pathExists) do
-      throw <| IO.userError s!"object file '{mFile}' of module {i.module} does not exist"
     let (mod, region) ← readModuleData mFile
     importModulesCore mod.imports
     modify fun s => { s with
diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
index 2d6b48fde035..cbcbc2942797 100644
--- a/src/Lean/Util/Path.lean
+++ b/src/Lean/Util/Path.lean
@@ -40,25 +40,52 @@ where
   | Name.anonymous => base
   | Name.num _ _ => panic! "ill-formed import"
 
+variable (base : FilePath) (ext : String) in
+/--
+Checks whether a module of the given name and extension exists in `base`; this uses case-sensitive
+path comparisons regardless of underlying file system to ensure the check is consistent across
+platforms.
+-/
+partial def moduleExists : Name → IO Bool := go ext
+where go (ext : String)
+  | .mkStr parent str => do
+    -- Case-sensitive check for file with extension in top-level call, for directory recursively
+    let entryName := if ext.isEmpty then str else s!"{str}.{ext}"
+    unless (← go "" parent) do
+      return false
+    return (← (modToFilePath base parent "").readDir).any (·.fileName == entryName)
+  | .anonymous => base.pathExists
+  | .num .. => panic! "ill-formed import"
+
 /-- A `.olean' search path. -/
 abbrev SearchPath := System.SearchPath
 
 namespace SearchPath
 
+def findRoot (sp : SearchPath) (ext : String) (pkg : String) : IO (Option FilePath) := do
+  sp.findM? fun p => do
+    unless (← p.isDir) do  -- Lake may pass search roots that do not exist (yet)
+      return false
+    if (← (p / pkg).isDir) then
+      return (← p.readDir).any (·.fileName == pkg)
+    else
+      let fileName := s!"{pkg}.{ext}"
+      return (← p.readDir).any (·.fileName == fileName)
+
 /-- If the package of `mod` can be found in `sp`, return the path with extension
 `ext` (`lean` or `olean`) corresponding to `mod`. Otherwise, return `none`. Does
 not check whether the returned path exists. -/
 def findWithExt (sp : SearchPath) (ext : String) (mod : Name) : IO (Option FilePath) := do
   let pkg := mod.getRoot.toString (escape := false)
-  let root? ← sp.findM? fun p =>
-    (p / pkg).isDir <||> ((p / pkg).addExtension ext).pathExists
+  let root? ← findRoot sp ext pkg
   return root?.map (modToFilePath · mod ext)
 
 /-- Like `findWithExt`, but ensures the returned path exists. -/
 def findModuleWithExt (sp : SearchPath) (ext : String) (mod : Name) : IO (Option FilePath) := do
-  if let some path ← findWithExt sp ext mod then
-    if ← path.pathExists then
-      return some path
+  let pkg := mod.getRoot.toString (escape := false)
+  if let some root ← findRoot sp ext pkg then
+    if (← moduleExists root ext mod) then
+      return some <| modToFilePath root mod ext
   return none
 
 def findAllWithExt (sp : SearchPath) (ext : String) : IO (Array FilePath) := do
@@ -105,12 +132,20 @@ def initSearchPath (leanSysroot : FilePath) (sp : SearchPath := ∅) : IO Unit :
 private def initSearchPathInternal : IO Unit := do
   initSearchPath (← getBuildDir)
 
-partial def findOLean (mod : Name) : IO FilePath := do
+/--
+Returns the path of the .olean file for `mod`. Throws an error if no search path entry for `mod`
+could be located, or if `checkExists` is true and the resulting path does not exist.
+-/
+partial def findOLean (mod : Name) (checkExists := true) : IO FilePath := do
   let sp ← searchPathRef.get
-  if let some fname ← sp.findWithExt "olean" mod then
-    return fname
+  let pkg := mod.getRoot.toString (escape := false)
+  if let some root ← sp.findRoot "olean" pkg then
+    let path := modToFilePath root mod "olean"
+    if !checkExists || (← moduleExists root "olean" mod) then
+      return path
+    else
+      throw <| IO.userError s!"object file '{path}' of module {mod} does not exist"
   else
-    let pkg := FilePath.mk <| mod.getRoot.toString (escape := false)
     let mut msg := s!"unknown module prefix '{pkg}'
 
 No directory '{pkg}' or file '{pkg}.lean' in the search path entries:
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 66caa9a62a2c..38b01261e2a0 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -31,6 +31,9 @@ Recursively parse the Lean files of a module and its imports
 building an `Array` product of its direct local imports.
 -/
 def Module.recParseImports (mod : Module) : FetchM (Array Module) := do
+  -- Make sure we fail reading the file independently of the FS case sensitivity
+  unless (← Lean.moduleExists mod.lib.srcDir "lean" mod.name) do
+    error s!"module source file not found: {mod.leanFile}"
   let contents ← IO.FS.readFile mod.leanFile
   let imports ← Lean.parseImports' contents mod.leanFile.toString
   let mods ← imports.foldlM (init := OrdModuleSet.empty) fun set imp =>
diff --git a/tests/pkg/import-case/.gitignore b/tests/pkg/import-case/.gitignore
new file mode 100644
index 000000000000..bfb30ec8c762
--- /dev/null
+++ b/tests/pkg/import-case/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/tests/pkg/import-case/ImportCase.lean b/tests/pkg/import-case/ImportCase.lean
new file mode 100644
index 000000000000..83be2888b28f
--- /dev/null
+++ b/tests/pkg/import-case/ImportCase.lean
@@ -0,0 +1,2 @@
+-- should *not* be accepted on any platform
+import ImportCase.basic
diff --git a/tests/pkg/import-case/ImportCase/Basic.lean b/tests/pkg/import-case/ImportCase/Basic.lean
new file mode 100644
index 000000000000..e99d3a6f69f8
--- /dev/null
+++ b/tests/pkg/import-case/ImportCase/Basic.lean
@@ -0,0 +1 @@
+def hello := "world"
\ No newline at end of file
diff --git a/tests/pkg/import-case/lakefile.toml b/tests/pkg/import-case/lakefile.toml
new file mode 100644
index 000000000000..6254c1e2c2e6
--- /dev/null
+++ b/tests/pkg/import-case/lakefile.toml
@@ -0,0 +1,5 @@
+name = "«import-case»"
+defaultTargets = ["ImportCase"]
+
+[[lean_lib]]
+name = "ImportCase"
diff --git a/tests/pkg/import-case/test.sh b/tests/pkg/import-case/test.sh
new file mode 100755
index 000000000000..889a4fb42ce8
--- /dev/null
+++ b/tests/pkg/import-case/test.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+rm -rf .lake/build
+(lake build 2>&1 && exit 1 || true) | grep --color -F 'module source file not found'