diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean
index b1965b0ec5..b6310ba5c0 100644
--- a/src/Lean/Meta/Tactic/Injection.lean
+++ b/src/Lean/Meta/Tactic/Injection.lean
@@ -62,7 +62,7 @@ inductive InjectionResult where
   | solved
   | subgoal (mvarId : MVarId) (newEqs : Array FVarId) (remainingNames : List Name)
 
-private def heqToEq (mvarId : MVarId) (fvarId : FVarId) (tryToClear : Bool) : MetaM (FVarId × MVarId) :=
+def heqToEq (mvarId : MVarId) (fvarId : FVarId) (tryToClear : Bool) : MetaM (FVarId × MVarId) :=
   withMVarContext mvarId do
    let decl ← getLocalDecl fvarId
    let type ← whnf decl.type