From bcde89b13118a8061f750f0f5213137bd73de188 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 19 Jun 2023 12:40:06 +0100
Subject: [PATCH] fix: respect type reducibility when generating injectivity
 lemmas

---
 src/Lean/Meta/Injective.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
index da56406f05a1b..e005a2bdb3778 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/src/Lean/Meta/Injective.lean
@@ -43,7 +43,7 @@ private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useE
       for arg1 in args1, arg2 in args2 do
         let arg1Type ← inferType arg1
         if !(← isProp arg1Type) && arg1 != arg2 then
-          eqs := eqs.push (← mkEqHEq arg1 arg2)
+          eqs := eqs.push (← withReducible <| mkEqHEq arg1 arg2)
       if let some andEqs := mkAnd? eqs then
         let result ← if useEq then
           mkEq eq andEqs