From 184f2ed5977173e8ca56fe89fd565d73624817ad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 21 Jun 2023 20:27:44 -0700
Subject: [PATCH] chore: improve `isNonTrivialProof`

---
 src/Lean/Meta/AbstractNestedProofs.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean
index b7bc8688be..b76e65db62 100644
--- a/src/Lean/Meta/AbstractNestedProofs.lean
+++ b/src/Lean/Meta/AbstractNestedProofs.lean
@@ -8,11 +8,18 @@ import Lean.Meta.Closure
 namespace Lean.Meta
 namespace AbstractNestedProofs
 
+def getLambdaBody (e : Expr) : Expr :=
+  match e with
+  | .lam _ _ b _ => getLambdaBody b
+  | _ => e
+
 def isNonTrivialProof (e : Expr) : MetaM Bool := do
   if !(← isProof e) then
     pure false
   else
-    e.withApp fun f args =>
+    -- We consider proofs such as `fun x => f x a` as trivial.
+    -- For example, we don't want to abstract the body of `def rfl`
+    (getLambdaBody e).withApp fun f args =>
       pure $ !f.isAtomic || args.any fun arg => !arg.isAtomic
 
 structure Context where