refactor: remove use of liftCommandElabM from Coinductive (#13782)

This PR eliminates the use of `liftCommandElabM` from the coinductive
module.

Context: `liftCommandElabM` was decided to be deprecated in issue
#10674.

src/Lean/Elab/Coinductive.lean

@@ -411,10 +411,8 @@ private def mkCasesOnCoinductive (infos : Array InductiveVal) : MetaM Unit := do
                     (value := originalCasesOn)
                     (hints := .opaque)
             -- We apply the attribute so that the `cases` tactic can pick it up
-            liftCommandElabM
-              <| liftTermElabM
-                <| Term.applyAttributes
-                    casesOnName #[{name := `cases_eliminator}, {name := `elab_as_elim}]
+            Term.TermElabM.run' <| Term.applyAttributes
+              casesOnName #[{name := `cases_eliminator}, {name := `elab_as_elim}]
 
 /--
   Main entry point for elaborating mutual coinductive predicates. This function is called after