diff --git a/theories/Tactics/Help.v b/theories/Tactics/Help.v
index b2e96396..eca4d6a4 100644
--- a/theories/Tactics/Help.v
+++ b/theories/Tactics/Help.v
@@ -26,6 +26,8 @@ Require Import Util.Goals.
 Require Import Util.Hypothesis.
 Require Import Util.MessagesToUser.
 
+Require Import Waterprove.
+
 Ltac2 Type exn ::= [ Inner ].
 
 Local Ltac2 create_forall_message (v_type: constr) :=
@@ -57,17 +59,14 @@ of_string " holds, then show a contradiction.
 Use ‘Assume that (...).’ to do the first step."].
 
 (**
-  Auxilliary tactic that checks if goal can be shown with minimal automation, i.e. only with core database.
+  Auxilliary tactic that checks if goal can be shown with automation
 *)
 Local Ltac2 solvable_by_core_auto () :=
-  let assertion_id := Fresh.in_goal @assert_goal in
+  let temp_id := Fresh.in_goal @temp in
   let goal := Control.goal () in
-  assert $goal as $assertion_id;
-  Control.focus 1 1 (fun () => 
-    let hint_databases := Some ((@core)::[]) in
-    Std.auto Std.Off (Some 1) [] hint_databases
-  );
-  clear $assertion_id.
+  assert $goal as $temp_id;
+  Control.focus 1 1 (fun () => waterprove 5 true Main);
+  clear $temp_id.
 
 (**
   Give a hint indicating a potential step to proving a given proposition [g].
@@ -106,7 +105,7 @@ Show one of the statements, use ‘It suffices to show that (...).’ with the d
     | not ?g => create_not_message g
     | False  => create_goal_wrapped_message ()
     | _ => 
-      match Control.case solvable_by_core_auto with
+      match Control.case (solvable_by_core_auto) with
         | Val _ => of_string "The goal can be shown immediately, use ‘We conclude that (...).’."
         | Err exn => Control.zero Inner
       end
@@ -137,4 +136,4 @@ Ltac2 print_goal_hint (g: constr option) :=
 (** * Help tactic
     Tries to give a hint how to proceed proving the current goal.
 *)
-Ltac2 Notation "Help" := print_goal_hint None.
+Ltac2 Notation "Help" := print_goal_hint None.
\ No newline at end of file