fix: respect type reducibility when generating injectivity lemmas

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
@@ -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 =>

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 {

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

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)