From f8e0fe7f3b77b0e5fe007c1c9f837c5b4971cbe5 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 1/4] 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 d4d5cef40826..da5ea4b13ec2 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

From 952b6b928f38fea4fcabc01da5a55d8ed7b98eea Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 10 Feb 2024 16:42:41 +0000
Subject: [PATCH 2/4] add test

---
 tests/lean/wrapped_injEq.lean              | 35 ++++++++++++++++++++++
 tests/lean/wrapped_injEq.lean.expected.out |  6 ++++
 2 files changed, 41 insertions(+)
 create mode 100644 tests/lean/wrapped_injEq.lean
 create mode 100644 tests/lean/wrapped_injEq.lean.expected.out

diff --git a/tests/lean/wrapped_injEq.lean b/tests/lean/wrapped_injEq.lean
new file mode 100644
index 000000000000..08fbbd637614
--- /dev/null
+++ b/tests/lean/wrapped_injEq.lean
@@ -0,0 +1,35 @@
+namespace Irreducible
+
+@[irreducible] def WrappedNat (_n : Nat) := Nat
+
+structure WithWrapped : Type :=
+(n : Nat)
+(m : WrappedNat n)
+
+#check WithWrapped.mk.injEq
+
+end Irreducible
+
+namespace Semireducible
+
+def WrappedNat (_n : Nat) := Nat
+
+structure WithWrapped : Type :=
+(n : Nat)
+(m : WrappedNat n)
+
+#check WithWrapped.mk.injEq
+
+end Semireducible
+
+namespace Reducible
+
+abbrev WrappedNat (_n : Nat) := Nat
+
+structure WithWrapped : Type :=
+(n : Nat)
+(m : WrappedNat n)
+
+#check WithWrapped.mk.injEq
+
+end Reducible
diff --git a/tests/lean/wrapped_injEq.lean.expected.out b/tests/lean/wrapped_injEq.lean.expected.out
new file mode 100644
index 000000000000..f8ae6c5cf1e8
--- /dev/null
+++ b/tests/lean/wrapped_injEq.lean.expected.out
@@ -0,0 +1,6 @@
+Irreducible.WithWrapped.mk.injEq (n : Nat) (m : WrappedNat n) (n : Nat) (m : WrappedNat n) :
+  ({ n := n, m := m } = { n := n, m := m }) = (n = n ∧ HEq m m)
+Semireducible.WithWrapped.mk.injEq (n : Nat) (m : WrappedNat n) (n : Nat) (m : WrappedNat n) :
+  ({ n := n, m := m } = { n := n, m := m }) = (n = n ∧ HEq m m)
+Reducible.WithWrapped.mk.injEq (n : Nat) (m : WrappedNat n) (n : Nat) (m : WrappedNat n) :
+  ({ n := n, m := m } = { n := n, m := m }) = (n = n ∧ m = m)

From 1689f507ae3dec4ba814dae4f6aed685935f9f8d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 10 Feb 2024 17:00:16 +0000
Subject: [PATCH 3/4] fix the error?

---
 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 da5ea4b13ec2..4cde984a5bf9 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/src/Lean/Meta/Injective.lean
@@ -82,7 +82,7 @@ private def throwInjectiveTheoremFailure {α} (ctorName : Name) (mvarId : MVarId
   throwError "{injTheoremFailureHeader ctorName}{indentD <| MessageData.ofGoal mvarId}"
 
 private def solveEqOfCtorEq (ctorName : Name) (mvarId : MVarId) (h : FVarId) : MetaM Unit := do
-  match (← injection mvarId h) with
+  match (withReducible <| ← injection mvarId h) with
   | InjectionResult.solved => unreachable!
   | InjectionResult.subgoal mvarId .. =>
     (←  mvarId.splitAnd).forM fun mvarId =>

From a0b2c14c12c882b4336b5495349186f80d47c8aa Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 10 Feb 2024 17:29:14 +0000
Subject: [PATCH 4/4] oh no

---
 src/library/constructions/no_confusion.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp
index ca206f374b47..b16ab2fd569f 100644
--- a/src/library/constructions/no_confusion.cpp
+++ b/src/library/constructions/no_confusion.cpp
@@ -101,6 +101,7 @@ static optional<environment> mk_no_confusion_type(environment const & env, name
                         expr rhs_type = lctx.get_type(rhs);
                         level l       = sort_level(type_checker(env, lctx).ensure_type(lhs_type));
                         expr h_type;
+                        // TODO: this should respect reducibility
                         if (type_checker(env, lctx).is_def_eq(lhs_type, rhs_type)) {
                             h_type = mk_app(mk_constant(get_eq_name(), levels(l)), lhs_type, lhs, rhs);
                         } else {