diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
index fb3af291ab..6b6cc7b1c8 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/src/Lean/Meta/Injective.lean
@@ -139,13 +139,14 @@ private partial def andProjections (e : Expr) : MetaM (Array Expr) := do
       return acc.push e
   go e (← inferType e) #[]
 
-private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : MetaM Expr := do
+private def mkInjectiveEqTheoremValue (ctorVal : ConstructorVal) (targetType : Expr) : MetaM Expr := do
   forallTelescopeReducing targetType fun xs type => do
     let mvar ← mkFreshExprSyntheticOpaqueMVar type
     let [mvarId₁, mvarId₂] ← mvar.mvarId!.apply (mkConst ``Eq.propIntro)
-      | throwError "unexpected number of subgoals when proving injective theorem for constructor `{ctorName}`"
-    let (h, mvarId₁) ← mvarId₁.intro1
-    solveEqOfCtorEq ctorName mvarId₁ h
+      | throwError "unexpected number of subgoals when proving injective theorem for constructor `{ctorVal.name}`"
+    let injPrf := mkConst (mkInjectiveTheoremNameFor ctorVal.name) (ctorVal.levelParams.map mkLevelParam)
+    let injPrf := mkAppN injPrf xs
+    mvarId₁.assign injPrf
     let mut mvarId₂ := mvarId₂
     while true do
       let t ← mvarId₂.getType
@@ -158,7 +159,7 @@ private def mkInjectiveEqTheoremValue (ctorName : Name) (targetType : Expr) : Me
       | _ => pure ()
       let (h, mvarId₂') ← mvarId₂.intro1
       (_, mvarId₂) ← substEq mvarId₂' h
-    try mvarId₂.refl catch _ => throwError (injTheoremFailureHeader ctorName)
+    try mvarId₂.refl catch _ => throwError (injTheoremFailureHeader ctorVal.name)
     mkLambdaFVars xs mvar
 
 private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
@@ -167,7 +168,7 @@ private def mkInjectiveEqTheorem (ctorVal : ConstructorVal) : MetaM Unit := do
   let some type ← mkInjectiveEqTheoremType? ctorVal
     | return ()
   trace[Meta.injective] "type: {type}"
-  let value ← mkInjectiveEqTheoremValue ctorVal.name type
+  let value ← mkInjectiveEqTheoremValue ctorVal type
   addDecl <| Declaration.thmDecl {
     name
     levelParams := ctorVal.levelParams