From b2a99e1b687bd947ea699abc590a80a36727c732 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 20 Aug 2022 17:12:51 -0700
Subject: [PATCH] chore: minor optimization at `mkFlatLet`

---
 src/Lean/Compiler/Simp.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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