diff --git a/src/Lean/Compiler/Simp.lean b/src/Lean/Compiler/Simp.lean
index 0a469c18ed..462839ec67 100644
--- a/src/Lean/Compiler/Simp.lean
+++ b/src/Lean/Compiler/Simp.lean
@@ -276,7 +276,11 @@ Remark: `body` may have many loose bound variables, and the loose bound variable
 must be lifted by `n`.
 -/
 private def mkFlatLet (y : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool := false) : Expr :=
-  go value 0
+  match value with
+  | .letE binderName type value'@(.lam ..) (.bvar 0) nonDep =>
+    /- Easy case that is often generated by `inlineProjInst?` -/
+    .letE binderName type value' body nonDep
+  | _ => go value 0
 where
   go (value : Expr) (i : Nat) : Expr :=
     match value with